]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Kind.hs
Add some Eq and Show instances.
[haskell/symantic.git] / 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 = 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 (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 _ <- eqKind 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 `eqKind` 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)