{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Language.Symantic.Typing.Type where

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

import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant

-- * Type 'Type'

-- | /Type of terms/.
--
-- * @cs@: /type constants/.
-- * @ki@: 'Kind' (/type of the type/).
-- * @h@: Haskell type projected onto.
--
-- * 'TyConst': /type constant/
-- * '(:$)': /type application/
-- * '(:~)': /type constraint constructor/
--
-- NOTE: when used, @h@ is a 'Proxy',
-- because @GADTs@ constructors cannot alter kinds.
-- Neither is it possible to assert that @(@'UnProxy'@ f :: * -> *)@,
-- and therefore @(@'UnProxy'@ f (@'UnProxy'@ x))@ cannot kind check;
-- however a type application of @f@ is needed in 'App' and 'Con',
-- so this is worked around with the introduction of the 'App' type family,
-- which handles the type application when @(@'UnProxy'@ f :: * -> *)@
-- is true from elsewhere, or stay abstract otherwise.
-- However, since type synonym family cannot be used within the pattern
-- of another type family, the kind of an abstract
-- @(@'App'@ f x)@ cannot be derived from @f@,
-- so this is worked around with the introduction of the @ki@ parameter.
data Type (cs::[*]) (ki::Kind) (h:: *) where
	TyConst
	 :: Const cs c
	 -> Type cs (Kind_of_Proxy c) c
	(:$)
	 :: Type cs (ki_x ':> ki) f
	 -> Type cs ki_x x
	 -> Type cs ki (App f x)
	(:~)
	 :: Con q x
	 => Type cs (ki_x ':> 'KiCon) q
	 -> Type cs ki_x x
	 -> Type cs 'KiCon (App q x)
	{-
	TyVar
	 :: SKind ki
	 -> SPeano v
	 -> Type cs ki v
	-}
infixl 5 :$
infixl 5 :~

-- ** Type family 'UnProxy'
-- | Useful to have 'App' and 'Con' type families working on all @a@.
type family UnProxy px :: k where
	UnProxy (Proxy h) = h

-- ** Type family 'App'
-- | Lift the Haskell /type application/ within a 'Proxy'.
type family App (f:: *) (a:: *) :: *
type instance App (Proxy (f:: ki_a -> ki_fa)) a = Proxy (f (UnProxy a))

-- ** Type family 'Con'
-- | Lift the Haskell /type constraint/ within a 'Proxy'.
type family Con (q:: *) (a:: *) :: Constraint
type instance Con (Proxy (q:: ki_a -> Constraint)) a = q (UnProxy a)

-- ** Type 'Type_of'
-- | Convenient wrapper when @t@ is statically known.
type Type_of cs t = Type cs (Kind_of t) (Proxy t)

kind_of :: Type cs ki h -> SKind ki
kind_of ty =
	case ty of
	 TyConst c -> kind_of_const c
	 f :$ _x -> case kind_of f of _ `SKiArrow` ki -> ki
	 q :~ _x -> case kind_of q of _ `SKiArrow` ki -> ki

eq_type
 :: Type cs ki_x x -> Type cs ki_y y
 -> Maybe (x :~: y)
eq_type (TyConst x) (TyConst y)
 | Just Refl <- testEquality x y
 = Just Refl
eq_type (xf :$ xx) (yf :$ yx)
 | Just Refl <- eq_type xf yf
 , Just Refl <- eq_type xx yx
 = Just Refl
eq_type (xq :~ xx) (yq :~ yx)
 | Just Refl <- eq_type xq yq
 , Just Refl <- eq_type xx yx
 = Just Refl
eq_type _ _ = Nothing

instance TestEquality (Type cs ki) where
	testEquality = eq_type

-- * Type 'EType'
-- | Existential for 'Type'.
data EType cs = forall ki h. EType (Type cs ki h)

instance Eq (EType cs) where
	EType x == EType y = isJust $ eq_type x y
instance Show_Const cs => Show (EType cs) where
	show (EType ty) = show_type ty

show_type :: Show_Const cs => Type cs ki_h h -> String
show_type (TyConst c) = show c
show_type ((:$) f@(:$){} a@(:$){}) = "(" ++ show_type f ++ ") (" ++ show_type a ++ ")"
show_type ((:$) f@(:$){} a) = "(" ++ show_type f ++ ") " ++ show_type a
show_type ((:$) f a@(:$){}) = show_type f ++ " (" ++ show_type a ++ ")"
show_type ((:$) f a) = show_type f ++ " " ++ show_type a
show_type ((:~) q a) = show_type q ++ " " ++ show_type a
-- show_type (TyVar v) = "t" ++ show (integral_from_peano v::Integer)

-- * Type 'Args'
data Args (cs::[*]) (args::[*]) where
	ArgZ :: Args cs '[]
	ArgS :: Type cs ki arg
	     -> Args cs args
	     -> Args cs (arg ': args)
infixr 5 `ArgS`

-- | Build the left spine of a 'Type'.
spine_of_type
 :: Type cs ki_h h
 -> (forall c as. Const cs c
               -> Args cs as -> ret) -> ret
spine_of_type (TyConst c)   k = k c ArgZ
spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
spine_of_type (q :~ a) k = spine_of_type q $ \c as -> k c (a `ArgS` as)

-- * Usual 'Type's

-- | The 'Bool' 'Type'
tyBool :: Inj_Const cs Bool => Type_of cs Bool
tyBool = TyConst inj_const

-- | The 'Eq' 'Type'
tyEq :: Inj_Const cs Eq => Type_of cs Eq
tyEq = TyConst inj_const

-- | The 'Int' 'Type'
tyInt :: Inj_Const cs Int => Type_of cs Int
tyInt = TyConst inj_const

-- | The 'IO'@ a@ 'Type'
tyIO :: Inj_Const cs IO => Type_of cs IO
tyIO = TyConst inj_const

-- | The 'Traversable'@ a@ 'Type'
tyTraversable :: Inj_Const cs Traversable => Type_of cs Traversable
tyTraversable = TyConst inj_const

-- | The 'Monad'@ a@ 'Type'
tyMonad :: Inj_Const cs Monad => Type_of cs Monad
tyMonad = TyConst inj_const

-- | The 'Int' 'Type'
tyFun :: Inj_Const cs (->) => Type_of cs (->)
tyFun = TyConst inj_const

-- | The function 'Type' @(\->) a b@
-- with an infix notation more readable.
(~>) :: forall cs a b. Inj_Const cs (->)
 => Type cs 'KiTerm (Proxy a)
 -> Type cs 'KiTerm (Proxy b)
 -> Type_of cs (a -> b)
(~>) a b = TyConst (inj_const::Const cs (Proxy (->))) :$ a :$ b
infixr 5 ~>