{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- {-# LANGUAGE TypeInType #-}
module Language.Symantic.Typing.Kind where

import Data.Proxy
import Data.Type.Equality
import GHC.Exts (Constraint)
import GHC.Prim (Any)

-- * Type 'Kind'
-- | /Type of types/.
data Kind
 =   KiTerm -- ^ \*
 |   KiCon -- ^ 'Constraint'
 |   (:>) Kind Kind -- ^ \->
infixr 0 :>

-- * Type family 'Kind_of'
-- | To be completed on need, according to the /type constants/ used.
type family   Kind_of (x::k) :: Kind
type instance Kind_of (x::k0 -> k1)   = Kind_of (Any::k0) ':> Kind_of (Any::k1)
type instance Kind_of (x::Constraint) = 'KiCon
type instance Kind_of (x:: *)         = 'KiTerm

-- ** Type family 'Kind_of_UnProxy'
type family Kind_of_UnProxy (x:: *) :: Kind where
	Kind_of_UnProxy (Proxy x) = Kind_of x

-- * Type 'EKind'
-- | Existential for 'Kind'.
data EKind = forall k. EKind (SKind k)
instance Eq EKind where
	EKind x == EKind y
	 | Just _ <- testEquality x y = True
	_x == _y = False
instance Show EKind where
	show (EKind x) = show x

-- * Type 'SKind'
-- | Singleton for 'Kind'.
data SKind (k::Kind) where
	SKiTerm  :: SKind 'KiTerm
	SKiCon   :: SKind 'KiCon
	SKiArrow :: SKind a -> SKind b -> SKind (a ':> b)
instance TestEquality SKind where
	testEquality SKiTerm SKiTerm = Just Refl
	testEquality SKiCon SKiCon = Just Refl
	testEquality (SKiArrow xa xb) (SKiArrow ya yb)
	 | Just Refl <- testEquality xa ya
	 , Just Refl <- testEquality xb yb
	 = Just Refl
	testEquality _ _ = Nothing
instance Show (SKind k) where
	show SKiTerm = "*"
	show SKiCon  = "Constraint"
	show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"

-- * Type 'IKind'
-- | Implicit for 'Kind'.
class IKind (k::Kind) where
	kind :: SKind k
instance IKind 'KiTerm where
	kind = SKiTerm
instance IKind 'KiCon where
	kind = SKiCon
instance (IKind a, IKind b) => IKind (a ':> b) where
	kind = kind `SKiArrow` kind