symantic/Language/Symantic/Typing/Kind.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 module Language.Symantic.Typing.Kind where
   6
   7 import Data.Type.Equality (TestEquality(..), (:~:)(..))
   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 = eqKind
  36
  37 eqKind :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
  38 eqKind KiType{} KiType{} = Just Refl
  39 eqKind KiConstraint{} KiConstraint{} = Just Refl
  40 eqKind (KiFun _xs xa xb) (KiFun _ys ya yb)
  41  | Just Refl <- eqKind xa ya
  42  , Just Refl <- eqKind xb yb
  43  = Just Refl
  44 eqKind _ _ = 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 @(Ty_of_Type k) (noSource @src)
  71
  72 -- ** Type 'Inj_KindP'
  73 class Inj_KindP k where
  74         inj_KindP :: 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 = KiFun src (inj_KindP @a src) (inj_KindP @b src)
  81
  82 -- ** Type 'Ty'
  83 -- | FIXME: workaround to be removed when
  84 -- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  85 -- will be fixed.
  86 data Ty
  87
  88 -- ** Type family 'Ty_of_Type'
  89 -- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
  90 -- this notably disables the expansion of 'Ty_of_Type'@ Any@.
  91 type family Ty_of_Type (t::K.Type) :: K.Type
  92 type instance Ty_of_Type K.Type       = Ty
  93 type instance Ty_of_Type K.Constraint = K.Constraint
  94 type instance Ty_of_Type (a -> b)     = Ty_of_Type a -> Ty_of_Type b
  95
  96 -- ** Type family 'Type_of_Ty'
  97 -- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
  98 -- this notably disables the expansion of 'Type_of_Ty'@ Any@.
  99 type family Type_of_Ty (t::K.Type) :: K.Type
 100 type instance Type_of_Ty Ty           = K.Type
 101 type instance Type_of_Ty K.Constraint = K.Constraint
 102 type instance Type_of_Ty (a -> b)     = Type_of_Ty a -> Type_of_Ty b
 103
 104 -- * Type 'KindK'
 105 -- | Existential for 'Kind'.
 106 data KindK src = forall k. KindK (Kind src k)
 107 instance Eq (KindK src) where
 108         KindK x == KindK y
 109          | Just _ <- eqKind x y = True
 110         _x == _y = False
 111 instance Show (KindK src) where
 112         show (KindK x) = show x
 113
 114 -- * Type 'Con_Kind'
 115 data Con_Kind src
 116  =   Con_Kind_Eq    (KindK src) (KindK src)
 117  |   Con_Kind_Arrow (KindK src)
 118  deriving (Eq, Show)
 119
 120 when_EqKind
 121  :: Inj_Error (Con_Kind src) err
 122  => Kind src x
 123  -> Kind src y
 124  -> ((x :~: y) -> Either err ret) -> Either err ret
 125 when_EqKind x y k =
 126         case x `eqKind` y of
 127          Just Refl -> k Refl
 128          Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)
 129
 130 when_KiFun ::
 131  Inj_Error (Con_Kind src) err =>
 132  Inj_Source (KindK src) src =>
 133  Kind src x ->
 134  (forall a b. (x :~: (a -> b)) ->
 135               Kind src a ->
 136               Kind src b ->
 137               Either err ret) ->
 138  Either err ret
 139 when_KiFun x k =
 140         case x of
 141          KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
 142          _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)