{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Kind where

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

import Language.Symantic.Parsing

-- * Type 'Kind'
-- | Singleton for kind types.
data Kind src k where
	KiType       :: src -> Kind src Kind.Type
	KiConstraint :: src -> Kind src Constraint
	KiArrow      :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
infixr 5 `KiArrow`

instance Source src => Sourced (Kind src k) where
	type Source_of (Kind src k) = src
	
	source_of (KiType       src)  = src
	source_of (KiConstraint src)  = src
	source_of (KiArrow src _a _b) = src
	
	source_is (KiType       _loc) src = KiType src
	source_is (KiConstraint _loc) src = KiConstraint src
	source_is (KiArrow _loc a b)  src = KiArrow src a b

instance Show (Kind src k) where
	show KiType{}           = "*"
	show KiConstraint{}     = "Constraint"
	show (KiArrow _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
instance TestEquality (Kind src) where
	testEquality = eqKi

eqKi :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
eqKi KiType{} KiType{} = Just Refl
eqKi KiConstraint{} KiConstraint{} = Just Refl
eqKi (KiArrow _xs xa xb) (KiArrow _ys ya yb)
 | Just Refl <- eqKi xa ya
 , Just Refl <- eqKi xb yb
 = Just Refl
eqKi _ _ = Nothing

-- * Type 'IKind'
-- | Implicit 'Kind'.
--
-- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
-- makes it fail to properly build an implicit 'Kind',
-- this can however be worked around by having the class instances
-- work on a data type 'Ty' instead of 'Data.Kind.Type',
-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'IKindP'.
class (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k where
	kind :: Source src => Kind src k
	kind = kindP (Proxy @(Ty_of_Type k)) sourceLess
instance (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k

-- ** Type 'IKindP'
class IKindP k where
	kindP :: Proxy k -> src -> Kind src (Type_of_Ty k)
instance IKindP Constraint where
	kindP _ = KiConstraint
instance IKindP Ty where
	kindP _ = KiType
instance (IKindP a, IKindP b) => IKindP (a -> b) where
	kindP _ src =
		KiArrow src
		 (kindP (Proxy @a) src)
		 (kindP (Proxy @b) src)

-- ** Type 'Ty'
-- | FIXME: to be removed when
-- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
-- will be fixed.
data Ty

-- ** Type family 'Ty_of_Type'
type family   Ty_of_Type (typ::Kind.Type) :: Kind.Type
type instance Ty_of_Type Kind.Type  = Ty
type instance Ty_of_Type Constraint = Constraint
type instance Ty_of_Type (a -> b)   = Ty_of_Type a -> Ty_of_Type b

-- ** Type family 'Type_of_Ty'
type family   Type_of_Ty (typ::Kind.Type) :: Kind.Type
type instance Type_of_Ty Ty         = Kind.Type
type instance Type_of_Ty Constraint = Constraint
type instance Type_of_Ty (a -> b)   = Type_of_Ty a -> Type_of_Ty b

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

-- * Class 'Inj_Error'
class Inj_Error a b where
	inj_Error :: a -> b
instance Inj_Error err e => Inj_Error err (Either e a) where
	inj_Error = Left . inj_Error

lift_Error
 :: forall e0 err e1 a.
 ( Inj_Error e0 e1
 , Inj_Error e1 err
 ) => Proxy e1 -> Either e0 a -> Either err a
lift_Error _e1 (Right a) = Right a
lift_Error _e1 (Left e)  = Left $ inj_Error @e1 @err $ inj_Error @e0 @e1 e

-- * Type 'Con_Kind'
data Con_Kind src
 =   Con_Kind_Eq    (EKind src) (EKind src)
 |   Con_Kind_Arrow (EKind src)
 deriving (Eq, Show)

if_EqKind
 :: Inj_Error (Con_Kind src) err
 => Kind src x
 -> Kind src y
 -> ((x :~: y) -> Either err ret) -> Either err ret
if_EqKind x y k =
	case x `eqKi` y of
	 Just Refl -> k Refl
	 Nothing -> Left $ inj_Error $ Con_Kind_Eq (EKind x) (EKind y)

if_KiArrow
 :: ( Inj_Error (Con_Kind src) err
    , Inj_Source (EKind src) src )
 => Kind src x
 -> (forall a b. (x :~: (a -> b)) -> Kind src a -> Kind src b -> Either err ret)
 -> Either err ret
if_KiArrow x k =
	case x of
	 KiArrow _src a b -> k Refl (a `source` EKind x) (b `source` EKind x)
	 _ -> Left $ inj_Error $ Con_Kind_Arrow (EKind x)

-- * Type family 'KindOf'
type family   KindOf (x::k) :: Kind.Type
type instance KindOf (x::Constraint) = Constraint
type instance KindOf (x::Kind.Type)  = Kind.Type
type instance KindOf (x::a -> b)     = KindOf (Any::a) -> KindOf (Any::b)