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

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

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 'Type_Type2'
data Type_Type2 px (root:: * -> *) h where
	Type_Type2
	 :: (Constraint2_of px) a b
	 => px -> root a -> root b
	 -> Type_Type2 px root ((Host2_of px) a b)
class Constraint2_Empty a b
instance Constraint2_Empty a b

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

instance -- Eq_Type
 Eq_Type root =>
 Eq_Type (Type_Type2 (Proxy h2) root) where
	eq_type
	 (Type_Type2 _ arg1 res1)
	 (Type_Type2 _ arg2 res2)
	 | Just Refl <- arg1 `eq_type` arg2
	 , Just Refl <- res1 `eq_type` res2
	 = Just Refl
	eq_type _ _ = Nothing
instance -- Eq_Type
 Eq_Type root =>
 Eq_Type (Type_Type2 EPeano root) where
	eq_type (Type_Type2 p1 arg1 res1)
	        (Type_Type2 p2 arg2 res2)
	 | p1 == p2
	 , Just Refl <- arg1 `eq_type` arg2
	 , Just Refl <- res1 `eq_type` res2
	 = Just Refl
	eq_type _ _ = Nothing
instance -- Eq
 Eq_Type root =>
 Eq (Type_Type2 (Proxy h2) root h) where
	x == y = isJust $ x `eq_type` y
instance -- Eq
 Eq_Type root =>
 Eq (Type_Type2 EPeano root h) where
	x == y = isJust $ x `eq_type` y
instance -- Show
 ( String_from_Type root
 , String_from_Type (Type_Type2 px root)
 ) => Show (Type_Type2 px root h) where
	show = string_from_type
instance Constraint_Type Eq  (Type_Type2 px root)
instance Constraint_Type Ord (Type_Type2 px root)
instance Unlift_Type1 (Type_Type2 px)  -- FIXME: should be doable
instance Eq_Type1 (Type_Type2 px root) -- FIXME: should be doable

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

-- ** Type 'Constraint2_of'
type family Constraint2_of px :: (* -> * -> Constraint)