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

import Data.Type.Equality (TestEquality(..), (:~:)(..))
import qualified Data.Kind as K

import Language.Symantic.Grammar

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

type instance SourceOf (Kind src k) = src
instance Source src => Sourceable (Kind src k) where
	sourceOf (KiType       src) = src
	sourceOf (KiConstraint src) = src
	sourceOf (KiFun src _a _b)  = src
	
	setSource (KiType       _loc) src = KiType src
	setSource (KiConstraint _loc) src = KiConstraint src
	setSource (KiFun _loc a b)    src = KiFun src a b

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

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

-- * Type 'K'
type K (t::kt) = kt

-- * Class 'KindOf'
-- | Return the 'Kind' of something.
class KindOf (a::kt -> K.Type) where
	kindOf :: a t -> Kind (SourceOf (a t)) kt

-- * Type 'KindInj'
-- | 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.K.Type',
-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'KindP'.Inj
class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k where
instance (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k

kindInj ::
 forall k src.
 Source src =>
 KindInj k =>
 Kind src k
kindInj = kindInjP @(Ty_of_Type k) (noSource @src)

-- ** Type 'KindInjP'
class KindInjP k where
	kindInjP :: src -> Kind src (Type_of_Ty k)
instance KindInjP K.Constraint where
	kindInjP = KiConstraint
instance KindInjP Ty where
	kindInjP = KiType
instance (KindInjP a, KindInjP b) => KindInjP (a -> b) where
	kindInjP src = KiFun src (kindInjP @a src) (kindInjP @b src)

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

-- ** Type family 'Ty_of_Type'
-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
-- this notably disables the expansion of 'Ty_of_Type'@ Any@.
type family Ty_of_Type (t::K.Type) :: K.Type
type instance Ty_of_Type K.Type       = Ty
type instance Ty_of_Type K.Constraint = K.Constraint
type instance Ty_of_Type (a -> b)     = Ty_of_Type a -> Ty_of_Type b

-- ** Type family 'Type_of_Ty'
-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
-- this notably disables the expansion of 'Type_of_Ty'@ Any@.
type family Type_of_Ty (t::K.Type) :: K.Type
type instance Type_of_Ty Ty           = K.Type
type instance Type_of_Ty K.Constraint = K.Constraint
type instance Type_of_Ty (a -> b)     = Type_of_Ty a -> Type_of_Ty b

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

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

when_EqKind
 :: ErrorInj (Con_Kind src) err
 => Kind src x
 -> Kind src y
 -> ((x :~: y) -> Either err ret) -> Either err ret
when_EqKind x y k =
	case x `eqKind` y of
	 Just Refl -> k Refl
	 Nothing -> Left $ errorInj $ Con_Kind_Eq (KindK x) (KindK y)

when_KiFun ::
 ErrorInj (Con_Kind src) err =>
 SourceInj (KindK src) src =>
 Kind src x ->
 (forall a b. (x :~: (a -> b)) ->
              Kind src a ->
              Kind src b ->
              Either err ret) ->
 Either err ret
when_KiFun x k =
	case x of
	 KiFun _src a b -> k Refl (a `withSource` KindK x) (b `withSource` KindK x)
	 _ -> Left $ errorInj $ Con_Kind_Arrow (KindK x)