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 import Language.Symantic.Parsing
  13
  14 -- * Type 'Kind'
  15 -- | Singleton for kind types.
  16 data Kind src k where
  17         KiType       :: src -> Kind src Kind.Type
  18         KiConstraint :: src -> Kind src Constraint
  19         KiArrow      :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
  20 infixr 5 `KiArrow`
  21
  22 instance Source src => Sourced (Kind src k) where
  23         type Source_of (Kind src k) = src
  24
  25         source_of (KiType       src)  = src
  26         source_of (KiConstraint src)  = src
  27         source_of (KiArrow src _a _b) = src
  28
  29         source_is (KiType       _loc) src = KiType src
  30         source_is (KiConstraint _loc) src = KiConstraint src
  31         source_is (KiArrow _loc a b)  src = KiArrow src a b
  32
  33 instance Show (Kind src k) where
  34         show KiType{}           = "*"
  35         show KiConstraint{}     = "Constraint"
  36         show (KiArrow _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
  37 instance TestEquality (Kind src) where
  38         testEquality = eqKi
  39
  40 eqKi :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
  41 eqKi KiType{} KiType{} = Just Refl
  42 eqKi KiConstraint{} KiConstraint{} = Just Refl
  43 eqKi (KiArrow _xs xa xb) (KiArrow _ys ya yb)
  44  | Just Refl <- eqKi xa ya
  45  , Just Refl <- eqKi xb yb
  46  = Just Refl
  47 eqKi _ _ = Nothing
  48
  49 -- * Type 'Inj_Kind'
  50 -- | Implicit 'Kind'.
  51 --
  52 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  53 -- makes it fail to properly build an implicit 'Kind',
  54 -- this can however be worked around by having the class instances
  55 -- work on a data type 'Ty' instead of 'Data.Kind.Type',
  56 -- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.
  57 class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where
  58         inj_Kind :: Source src => Kind src k
  59         inj_Kind = inj_KindP (Proxy @(Ty_of_Type k)) sourceLess
  60 instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k
  61
  62 -- ** Type 'Inj_KindP'
  63 class Inj_KindP k where
  64         inj_KindP :: Proxy k -> src -> Kind src (Type_of_Ty k)
  65 instance Inj_KindP Constraint where
  66         inj_KindP _ = KiConstraint
  67 instance Inj_KindP Ty where
  68         inj_KindP _ = KiType
  69 instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where
  70         inj_KindP _ src =
  71                 KiArrow src
  72                  (inj_KindP (Proxy @a) src)
  73                  (inj_KindP (Proxy @b) src)
  74
  75 -- ** Type 'Ty'
  76 -- | FIXME: to be removed when
  77 -- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  78 -- will be fixed.
  79 data Ty
  80
  81 -- ** Type family 'Ty_of_Type'
  82 type family   Ty_of_Type (typ::Kind.Type) :: Kind.Type
  83 type instance Ty_of_Type Kind.Type  = Ty
  84 type instance Ty_of_Type Constraint = Constraint
  85 type instance Ty_of_Type (a -> b)   = Ty_of_Type a -> Ty_of_Type b
  86
  87 -- ** Type family 'Type_of_Ty'
  88 type family   Type_of_Ty (typ::Kind.Type) :: Kind.Type
  89 type instance Type_of_Ty Ty         = Kind.Type
  90 type instance Type_of_Ty Constraint = Constraint
  91 type instance Type_of_Ty (a -> b)   = Type_of_Ty a -> Type_of_Ty b
  92
  93 -- * Type 'EKind'
  94 -- | Existential for 'Kind'.
  95 data EKind src = forall k. EKind (Kind src k)
  96 instance Eq (EKind src) where
  97         EKind x == EKind y
  98          | Just _ <- eqKi x y = True
  99         _x == _y = False
 100 instance Show (EKind src) where
 101         show (EKind x) = show x
 102
 103 -- * Class 'Inj_Error'
 104 class Inj_Error a b where
 105         inj_Error :: a -> b
 106 instance Inj_Error err e => Inj_Error err (Either e a) where
 107         inj_Error = Left . inj_Error
 108
 109 lift_Error
 110  :: forall e0 err e1 a.
 111  ( Inj_Error e0 e1
 112  , Inj_Error e1 err
 113  ) => Proxy e1 -> Either e0 a -> Either err a
 114 lift_Error _e1 (Right a) = Right a
 115 lift_Error _e1 (Left e)  = Left $ inj_Error @e1 @err $ inj_Error @e0 @e1 e
 116
 117 -- * Type 'Con_Kind'
 118 data Con_Kind src
 119  =   Con_Kind_Eq    (EKind src) (EKind src)
 120  |   Con_Kind_Arrow (EKind src)
 121  deriving (Eq, Show)
 122
 123 if_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 if_EqKind x y k =
 129         case x `eqKi` y of
 130          Just Refl -> k Refl
 131          Nothing -> Left $ inj_Error $ Con_Kind_Eq (EKind x) (EKind y)
 132
 133 if_KiArrow
 134  :: ( Inj_Error (Con_Kind src) err
 135     , Inj_Source (EKind src) src )
 136  => Kind src x
 137  -> (forall a b. (x :~: (a -> b)) -> Kind src a -> Kind src b -> Either err ret)
 138  -> Either err ret
 139 if_KiArrow x k =
 140         case x of
 141          KiArrow _src a b -> k Refl (a `source` EKind x) (b `source` EKind x)
 142          _ -> Left $ inj_Error $ Con_Kind_Arrow (EKind x)
 143
 144 -- * Type family 'KindOf'
 145 type family   KindOf (x::k) :: Kind.Type
 146 type instance KindOf (x::Constraint) = Constraint
 147 type instance KindOf (x::Kind.Type)  = Kind.Type
 148 type instance KindOf (x::a -> b)     = KindOf (Any::a) -> KindOf (Any::b)
 149
 150 {-
 151 import Debug.Trace (trace)
 152
 153 dbg :: Show a => [Char] -> a -> a
 154 dbg msg x = trace (msg ++ " = " ++ show x) x
 155 -}