{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Type.Type2 where

import Data.Maybe (isJust)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Lib.Data.Peano
-- import Language.Symantic.Lib.Data.Bool
import Language.Symantic.Type.Root
-- import Language.Symantic.Type.Alt
import Language.Symantic.Type.Error
import Language.Symantic.Type.Type0
-- import Language.Symantic.Type.Type1

-- * Type 'Type2'
-- | A type of kind @(* -> * -> *)@.
data Type2 px (root:: * -> *) h where
	Type2 :: px -> root a -> root b
	      -> Type2 px root ((Host2_of px) a b)

type instance Root_of_Type      (Type2 px root) = root
type instance Error_of_Type ast (Type2 px root) = No_Error_Type

instance -- Type0_Eq
 Type0_Eq root =>
 Type0_Eq (Type2 (Proxy h2) root) where
	type0_eq
	 (Type2 _ arg1 res1)
	 (Type2 _ arg2 res2)
	 | Just Refl <- arg1 `type0_eq` arg2
	 , Just Refl <- res1 `type0_eq` res2
	 = Just Refl
	type0_eq _ _ = Nothing
instance -- Type0_Eq
 Type0_Eq root =>
 Type0_Eq (Type2 EPeano root) where
	type0_eq (Type2 p1 arg1 res1)
	        (Type2 p2 arg2 res2)
	 | p1 == p2
	 , Just Refl <- arg1 `type0_eq` arg2
	 , Just Refl <- res1 `type0_eq` res2
	 = Just Refl
	type0_eq _ _ = Nothing
instance -- Eq
 Type0_Eq root =>
 Eq (Type2 (Proxy h2) root h) where
	x == y = isJust $ x `type0_eq` y
instance -- Eq
 Type0_Eq root =>
 Eq (Type2 EPeano root h) where
	x == y = isJust $ x `type0_eq` y
instance -- Show
 ( String_from_Type root
 , String_from_Type (Type2 px root)
 ) => Show (Type2 px root h) where
	show = string_from_type

-- | Inject a 'Type2' within a root type.
type2
 :: forall root h2 a b.
 Type_Root_Lift (Type2 (Proxy h2)) root
 => root a -> root b -> root (h2 a b)
type2 a b = type_root_lift $ Type2 (Proxy::Proxy h2) a b

-- ** Type 'Host2_of'
type family Host2_of px :: * -> * -> *
type instance Host2_of (Proxy h2) = h2