]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Kind.hs
Fix cabal-version warning.
[haskell/symantic.git] / 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 => Sourceable (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 'KindInj'
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 'KindP'.Inj
62 class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k where
63 instance (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k
64
65 kindInj ::
66 forall k src.
67 Source src =>
68 KindInj k =>
69 Kind src k
70 kindInj = kindInjP @(Ty_of_Type k) (noSource @src)
71
72 -- ** Type 'KindInjP'
73 class KindInjP k where
74 kindInjP :: src -> Kind src (Type_of_Ty k)
75 instance KindInjP K.Constraint where
76 kindInjP = KiConstraint
77 instance KindInjP Ty where
78 kindInjP = KiType
79 instance (KindInjP a, KindInjP b) => KindInjP (a -> b) where
80 kindInjP src = KiFun src (kindInjP @a src) (kindInjP @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 :: ErrorInj (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 $ errorInj $ Con_Kind_Eq (KindK x) (KindK y)
129
130 when_KiFun ::
131 ErrorInj (Con_Kind src) err =>
132 SourceInj (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 `withSource` KindK x) (b `withSource` KindK x)
142 _ -> Left $ errorInj $ Con_Kind_Arrow (KindK x)