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 Data.Proxy
   7 import Data.Type.Equality
   8 import qualified Data.Kind as K
   9
  10 import Language.Symantic.Grammar
  11
  12 -- * Type 'Kind'
  13 -- | Singleton for kind types.
  14 data Kind src k where
  15         KiType       :: src -> Kind src K.Type
  16         KiConstraint :: src -> Kind src K.Constraint
  17         KiFun        :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
  18 infixr 5 `KiFun`
  19
  20 type instance SourceOf (Kind src k) = src
  21 instance Source src => Sourced (Kind src k) where
  22         sourceOf (KiType       src) = src
  23         sourceOf (KiConstraint src) = src
  24         sourceOf (KiFun src _a _b)  = src
  25
  26         setSource (KiType       _loc) src = KiType src
  27         setSource (KiConstraint _loc) src = KiConstraint src
  28         setSource (KiFun _loc a b)    src = KiFun src a b
  29
  30 instance Show (Kind src k) where
  31         show KiType{}         = "*"
  32         show KiConstraint{}   = "Constraint"
  33         show (KiFun _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
  34 instance TestEquality (Kind src) where
  35         testEquality = eqKi
  36
  37 eqKi :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
  38 eqKi KiType{} KiType{} = Just Refl
  39 eqKi KiConstraint{} KiConstraint{} = Just Refl
  40 eqKi (KiFun _xs xa xb) (KiFun _ys ya yb)
  41  | Just Refl <- eqKi xa ya
  42  , Just Refl <- eqKi xb yb
  43  = Just Refl
  44 eqKi _ _ = Nothing
  45
  46 -- * Type 'K'
  47 type K (t::kt) = kt
  48
  49 -- * Class 'KindOf'
  50 -- | Return the 'Kind' of something.
  51 class KindOf (a::kt -> K.Type) where
  52         kindOf :: a t -> Kind (SourceOf (a t)) kt
  53
  54 -- * Type 'Inj_Kind'
  55 -- | Implicit 'Kind'.
  56 --
  57 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  58 -- makes it fail to properly build an implicit 'Kind',
  59 -- this can however be worked around by having the class instances
  60 -- work on a data type 'Ty' instead of 'Data.K.Type',
  61 -- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.
  62 class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where
  63 instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k
  64
  65 inj_Kind ::
  66  forall k src.
  67  Source src =>
  68  Inj_Kind k =>
  69  Kind src k
  70 inj_Kind = inj_KindP (Proxy @(Ty_of_Type k)) (noSource @src)
  71
  72 -- ** Type 'Inj_KindP'
  73 class Inj_KindP k where
  74         inj_KindP :: Proxy k -> src -> Kind src (Type_of_Ty k)
  75 instance Inj_KindP K.Constraint where
  76         inj_KindP _ = KiConstraint
  77 instance Inj_KindP Ty where
  78         inj_KindP _ = KiType
  79 instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where
  80         inj_KindP _ src =
  81                 KiFun src
  82                  (inj_KindP (Proxy @a) src)
  83                  (inj_KindP (Proxy @b) src)
  84
  85 -- ** Type 'Ty'
  86 -- | FIXME: workaround to be removed when
  87 -- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  88 -- will be fixed.
  89 data Ty
  90
  91 -- ** Type family 'Ty_of_Type'
  92 -- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
  93 -- this notably disables the expansion of 'Ty_of_Type'@ Any@.
  94 type family Ty_of_Type (t::K.Type) :: K.Type
  95 type instance Ty_of_Type K.Type       = Ty
  96 type instance Ty_of_Type K.Constraint = K.Constraint
  97 type instance Ty_of_Type (a -> b)     = Ty_of_Type a -> Ty_of_Type b
  98
  99 -- ** Type family 'Type_of_Ty'
 100 -- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
 101 -- this notably disables the expansion of 'Type_of_Ty'@ Any@.
 102 type family Type_of_Ty (t::K.Type) :: K.Type
 103 type instance Type_of_Ty Ty           = K.Type
 104 type instance Type_of_Ty K.Constraint = K.Constraint
 105 type instance Type_of_Ty (a -> b)     = Type_of_Ty a -> Type_of_Ty b
 106
 107 -- * Type 'KindK'
 108 -- | Existential for 'Kind'.
 109 data KindK src = forall k. KindK (Kind src k)
 110 instance Eq (KindK src) where
 111         KindK x == KindK y
 112          | Just _ <- eqKi x y = True
 113         _x == _y = False
 114 instance Show (KindK src) where
 115         show (KindK x) = show x
 116
 117 -- * Type 'Con_Kind'
 118 data Con_Kind src
 119  =   Con_Kind_Eq    (KindK src) (KindK src)
 120  |   Con_Kind_Arrow (KindK src)
 121  deriving (Eq, Show)
 122
 123 when_EqKind
 124  :: Inj_Error (Con_Kind src) err
 125  => Kind src x
 126  -> Kind src y
 127  -> ((x :~: y) -> Either err ret) -> Either err ret
 128 when_EqKind x y k =
 129         case x `eqKi` y of
 130          Just Refl -> k Refl
 131          Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)
 132
 133 when_KiFun ::
 134  Inj_Error (Con_Kind src) err =>
 135  Inj_Source (KindK src) src =>
 136  Kind src x ->
 137  (forall a b. (x :~: (a -> b)) ->
 138               Kind src a ->
 139               Kind src b ->
 140               Either err ret) ->
 141  Either err ret
 142 when_KiFun x k =
 143         case x of
 144          KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
 145          _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)