{-# 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)

-- * Type 'SKind'
-- | Singleton for kind types.
data SKind k where
	SKiType       :: SKind Kind.Type
	SKiConstraint :: SKind Constraint
	SKiArrow      :: SKind ka -> SKind kb -> SKind (ka -> kb)
infixr 5 `SKiArrow`

instance Show (SKind k) where
	show SKiType = "*"
	show SKiConstraint  = "Constraint"
	show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
instance TestEquality SKind where
	testEquality = eq_SKind

eq_SKind :: SKind x -> SKind y -> Maybe (x:~:y)
eq_SKind SKiType SKiType = Just Refl
eq_SKind SKiConstraint SKiConstraint = Just Refl
eq_SKind (SKiArrow xa xb) (SKiArrow ya yb)
 | Just Refl <- eq_SKind xa ya
 , Just Refl <- eq_SKind xb yb
 = Just Refl
eq_SKind _ _ = Nothing

-- * Type 'IKind'
-- | Implicit 'SKind'.
--
-- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
-- makes it fail to properly build an implicit 'SKind',
-- 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 :: SKind k
	kind = kindP (Proxy @(Ty_of_Type k))
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 -> SKind (Type_of_Ty k)
instance IKindP Constraint where
	kindP _ = SKiConstraint
instance IKindP Ty where
	kindP _ = SKiType
instance (IKindP a, IKindP b) => IKindP (a -> b) where
	kindP _ = kindP (Proxy @a) `SKiArrow` kindP (Proxy @b)

-- ** 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 = forall k. EKind (SKind k)
instance Eq EKind where
	EKind x == EKind y
	 | Just _ <- eq_SKind x y = True
	_x == _y = False
instance Show EKind where
	show (EKind x) = show x

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

{-
instance Show (x :~~: y) where
	show _ = "HRefl"

type family Eq_KindF (x::kx) (y::ky) :: Bool where
	Eq_KindF (x::k) (y::k) = 'True
	Eq_KindF x y = 'False

type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
class Eq_KindB (b::Bool) (x::kx) (y::ky) where
	eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
instance Eq_KindB 'False x y where
	eq_kindB _b _x _y = Nothing
instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
	eq_kindB _b _x _y = Just HRefl
instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
	eq_kindB _b _x _y = Just HRefl
instance
 ( Eq_Kind (Any::k0) (Any::k2)
 , Eq_Kind (Any::k1) (Any::k3)
 ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
	eq_kindB _b _x _y
	 | Just HRefl <- eq_kind (Proxy @(Any::k0)) (Proxy @(Any::k2))
	 , Just HRefl <- eq_kind (Proxy @(Any::k1)) (Proxy @(Any::k3))
	 = Just HRefl
	eq_kindB _b _x _y = Nothing

eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
eq_kind = eq_kindB (Proxy @(Eq_KindF x y))
-}