{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module TFHOE.Type.Common where

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

-- * Class 'Type_Eq'

-- | Test two types for equality,
-- returning an Haskell type-level proof
-- of the equality when it holds.
class Type_Eq ty where
	type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)

-- * Class 'Type_from'

class Type_Eq ty => Type_from raw ty where
	type_from
	 :: raw
	 -> (forall h. ty h -> Either Error_Type ret)
	 -> Either Error_Type ret

type Error_Type = String

-- * Class 'String_from_Type'

class String_from_Type ty where
	string_from_type :: ty h -> String

-- * Type 'Var'

-- | Join a name and a type;
-- used to handle lambda variables by name
-- (and not DeBruijn indices).
data Var ty h
 =   Var String (ty h)

-- * Type 'Context'

-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types of lambda variables in 'Expr_from'
-- or meta-terms of lambda variables in 'Repr_Host'.
data Context :: (* -> *) -> [*] -> * where
	Context_Empty :: Context item '[]
	Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
infixr 5 `Context_Next`

-- ** Type 'Type_End'

-- | Close an extensible type.
data Type_End h where
	Type_End :: Type_End ()

instance Type_Eq Type_End where
	type_eq Type_End Type_End = Just Refl
instance Eq (Type_End h) where
	_ == _ = True
instance String_from_Type Type_End where
	string_from_type _ = ""
instance Type_from raw Type_End where
	type_from _raw k = k Type_End

-- * Type 'Exists_Type'

-- | Existential data type to wrap an indexed type.
data Exists_Type ty
 = forall h. Exists_Type (ty h)
instance -- Eq
 Type_Eq ty =>
 Eq (Exists_Type ty) where
	Exists_Type xh == Exists_Type yh =
		isJust $ type_eq xh yh
instance -- Show
 String_from_Type ty =>
 Show (Exists_Type ty) where
	show (Exists_Type ty) = string_from_type ty

-- * Type 'Exists_Type_and_Repr'

data Exists_Type_and_Repr ty repr
 =   forall h.
     Exists_Type_and_Repr (ty h) (repr h)