symantic/Language/Symantic/Typing/Kind.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE UndecidableInstances #-}
   4 module Language.Symantic.Typing.Kind where
   5
   6 import qualified Data.Kind as Kind
   7 import Data.Proxy
   8 import Data.Type.Equality
   9 import GHC.Exts (Constraint)
  10 import GHC.Prim (Any)
  11
  12 -- * Type 'SKind'
  13 -- | Singleton for kind types.
  14 data SKind k where
  15         SKiType       :: SKind Kind.Type
  16         SKiConstraint :: SKind Constraint
  17         SKiArrow      :: SKind ka -> SKind kb -> SKind (ka -> kb)
  18 infixr 5 `SKiArrow`
  19
  20 instance Show (SKind k) where
  21         show SKiType = "*"
  22         show SKiConstraint  = "Constraint"
  23         show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
  24 instance TestEquality SKind where
  25         testEquality = eq_SKind
  26
  27 eq_SKind :: SKind x -> SKind y -> Maybe (x:~:y)
  28 eq_SKind SKiType SKiType = Just Refl
  29 eq_SKind SKiConstraint SKiConstraint = Just Refl
  30 eq_SKind (SKiArrow xa xb) (SKiArrow ya yb)
  31  | Just Refl <- eq_SKind xa ya
  32  , Just Refl <- eq_SKind xb yb
  33  = Just Refl
  34 eq_SKind _ _ = Nothing
  35
  36 -- * Type 'IKind'
  37 -- | Implicit 'SKind'.
  38 --
  39 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  40 -- makes it fail to properly build an implicit 'SKind',
  41 -- this can however be worked around by having the class instances
  42 -- work on a data type 'Ty' instead of 'Data.Kind.Type',
  43 -- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'IKindP'.
  44 class (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k where
  45         kind :: SKind k
  46         kind = kindP (Proxy @(Ty_of_Type k))
  47 instance (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k
  48
  49 -- ** Type 'IKindP'
  50 class IKindP k where
  51         kindP :: Proxy k -> SKind (Type_of_Ty k)
  52 instance IKindP Constraint where
  53         kindP _ = SKiConstraint
  54 instance IKindP Ty where
  55         kindP _ = SKiType
  56 instance (IKindP a, IKindP b) => IKindP (a -> b) where
  57         kindP _ = kindP (Proxy @a) `SKiArrow` kindP (Proxy @b)
  58
  59 -- ** Type 'Ty'
  60 -- | FIXME: to be removed when
  61 -- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  62 -- will be fixed.
  63 data Ty
  64
  65 -- ** Type family 'Ty_of_Type'
  66 type family   Ty_of_Type (typ::Kind.Type) :: Kind.Type
  67 type instance Ty_of_Type Kind.Type  = Ty
  68 type instance Ty_of_Type Constraint = Constraint
  69 type instance Ty_of_Type (a -> b)   = Ty_of_Type a -> Ty_of_Type b
  70
  71 -- ** Type family 'Type_of_Ty'
  72 type family   Type_of_Ty (typ::Kind.Type) :: Kind.Type
  73 type instance Type_of_Ty Ty         = Kind.Type
  74 type instance Type_of_Ty Constraint = Constraint
  75 type instance Type_of_Ty (a -> b)   = Type_of_Ty a -> Type_of_Ty b
  76
  77 -- * Type 'EKind'
  78 -- | Existential for 'Kind'.
  79 data EKind = forall k. EKind (SKind k)
  80 instance Eq EKind where
  81         EKind x == EKind y
  82          | Just _ <- eq_SKind x y = True
  83         _x == _y = False
  84 instance Show EKind where
  85         show (EKind x) = show x
  86
  87 -- * Type family 'Kind_Of'
  88 type family   Kind_Of (x::k) :: Kind.Type
  89 type instance Kind_Of (x::Constraint) = Constraint
  90 type instance Kind_Of (x::Kind.Type)  = Kind.Type
  91 type instance Kind_Of (x::a -> b)     = Kind_Of (Any::a) -> Kind_Of (Any::b)
  92
  93 {-
  94 instance Show (x :~~: y) where
  95         show _ = "HRefl"
  96
  97 type family Eq_KindF (x::kx) (y::ky) :: Bool where
  98         Eq_KindF (x::k) (y::k) = 'True
  99         Eq_KindF x y = 'False
 100
 101 type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
 102 class Eq_KindB (b::Bool) (x::kx) (y::ky) where
 103         eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
 104 instance Eq_KindB 'False x y where
 105         eq_kindB _b _x _y = Nothing
 106 instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
 107         eq_kindB _b _x _y = Just HRefl
 108 instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
 109         eq_kindB _b _x _y = Just HRefl
 110 instance
 111  ( Eq_Kind (Any::k0) (Any::k2)
 112  , Eq_Kind (Any::k1) (Any::k3)
 113  ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
 114         eq_kindB _b _x _y
 115          | Just HRefl <- eq_kind (Proxy @(Any::k0)) (Proxy @(Any::k2))
 116          , Just HRefl <- eq_kind (Proxy @(Any::k1)) (Proxy @(Any::k3))
 117          = Just HRefl
 118         eq_kindB _b _x _y = Nothing
 119
 120 eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
 121 eq_kind = eq_kindB (Proxy @(Eq_KindF x y))
 122 -}