]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Unify.hs
Improve dynamic insertion of terms (via CtxTy or Modules).
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Unify.hs
1 {-# LANGUAGE ExistentialQuantification #-}
2 {-# LANGUAGE TypeInType #-}
3 {-# LANGUAGE UndecidableInstances #-}
4 {-# LANGUAGE ViewPatterns #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 module Language.Symantic.Typing.Unify where
7
8 import Data.Map.Strict (Map)
9 import Data.Semigroup (Semigroup(..))
10 import Unsafe.Coerce (unsafeCoerce)
11 import qualified Data.Map.Strict as Map
12
13 import Language.Symantic.Grammar
14 import Language.Symantic.Typing.Variable
15 import Language.Symantic.Typing.Kind
16 import Language.Symantic.Typing.Type
17 import Language.Symantic.Typing.Show ()
18
19 -- * Type 'Subst'
20 -- | /Type variable substitution/.
21 --
22 -- WARNING: a 'Subst' MUST be without loops, and fully expanded.
23 newtype Subst src vs
24 = Subst (Map IndexVar (VT src vs))
25 deriving instance Source src => Show (Subst src vs)
26 instance Semigroup (Subst src vs) where
27 (<>) = unionSubst
28 instance Monoid (Subst src vs) where
29 mempty = Subst Map.empty
30 mappend = (<>)
31
32 -- | Unify two 'Subst's.
33 --
34 -- NOTE: the union is left-biased: in case of duplicate 'Var's,
35 -- it keeps the one from the first 'Subst' given.
36 --
37 -- NOTE: the first 'Subst' given is applied to the second (with 'subst'),
38 -- this way each 'Var' directly maps to an expanded 'Type',
39 -- so that, when using the resulting 'Subst',
40 -- there is no need to apply it multiple times
41 -- until there is no more substitution to be done.
42 unionSubst :: Subst src vs -> Subst src vs -> Subst src vs
43 unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) <$> y)
44
45 -- * Type 'VT'
46 -- | A 'Var' and a 'Type' existentialized over their type index.
47 data VT src vs = forall t. VT (Var src vs t) (Type src vs t)
48 deriving instance Source src => Show (VT src vs)
49
50 insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs
51 insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s
52
53 lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v)
54 lookupSubst v (Subst s)
55 | Just (VT v' t) <- Map.lookup (indexVar v) s
56 , Just HRefl <- v `eqVarKi` v'
57 = Just t
58 lookupSubst _v _m = Nothing
59
60 -- * Class 'Substable'
61 class Substable a where
62 -- | Like 'substVar', but without the /occurence check/.
63 substVarUnsafe ::
64 src ~ SourceOf a =>
65 vs ~ VarsOf a =>
66 Var src vs v -> Type src vs v -> a -> a
67 -- | Substitute all the 'Var's which have a match in given 'Subst'.
68 subst ::
69 src ~ SourceOf a =>
70 vs ~ VarsOf a =>
71 Subst src vs -> a -> a
72 instance Substable (Type src vs t) where
73 substVarUnsafe _v _r t@TyConst{} = t
74 substVarUnsafe v r (TyApp src f a) =
75 TyApp src
76 (substVarUnsafe v r f)
77 (substVarUnsafe v r a)
78 substVarUnsafe v r t@(TyVar _src _n vt) =
79 case v `eqVarKi` vt of
80 Just HRefl -> r
81 Nothing -> t
82 substVarUnsafe v r (TyFam src len fam as) =
83 TyFam src len fam $ substVarUnsafe v r as
84
85 subst _s t@TyConst{} = t
86 subst s (TyApp src f a) = TyApp src (subst s f) (subst s a)
87 subst (Subst s) t@(TyVar _src _n v) =
88 case indexVar v `Map.lookup` s of
89 Nothing -> t
90 Just (VT vr r) ->
91 case v `eqVarKi` vr of
92 Nothing -> error "[BUG] subst: kind mismatch"
93 Just HRefl -> r
94 subst s (TyFam src len fam as) = TyFam src len fam $ subst s as
95 instance Substable (Types src vs ts) where
96 substVarUnsafe _v _r TypesZ = TypesZ
97 substVarUnsafe v r (TypesS t ts) =
98 substVarUnsafe v r t `TypesS`
99 substVarUnsafe v r ts
100 subst _s TypesZ = TypesZ
101 subst s (TypesS t ts) = subst s t `TypesS` subst s ts
102
103 -- | Substitute the given 'Var' by the given 'Type',
104 -- returning 'Nothing' if this 'Type' contains
105 -- the 'Var' (occurence check).
106 substVar ::
107 src ~ SourceOf a =>
108 vs ~ VarsOf a =>
109 Source src => VarOccursIn a => Substable a =>
110 Var src vs v -> Type src vs v -> a -> Maybe a
111 substVar v r t =
112 if v `varOccursIn` r
113 then Nothing -- NOTE: occurence check
114 else Just $ substVarUnsafe v r t
115
116 -- ** Type 'Error_Unify'
117 -- | Reasons why two 'Type's cannot be unified.
118 data Error_Unify src
119 = Error_Unify_Var_loop IndexVar (TypeVT src)
120 -- ^ /occurence check/: a 'Var' is unified with a 'Type'
121 -- which contains this same 'Var'.
122 | Error_Unify_Const_mismatch (TypeVT src) (TypeVT src)
123 -- ^ Two 'TyConst's should be the same, but are different.
124 | Error_Unify_Kind_mismatch (KindK src) (KindK src)
125 -- ^ Two 'Kind's should be the same, but are different.
126 | Error_Unify_Kind (Con_Kind src)
127 -- ^ Two 'Kind's mismatch.
128 | Error_Unify_mismatch (TypeVT src) (TypeVT src)
129 -- ^ Cannot unify those two 'Type's.
130
131 deriving instance Source src => Eq (Error_Unify src)
132 deriving instance Source src => Show (Error_Unify src)
133
134 instance Inj_Error (Error_Unify src) (Error_Unify src) where
135 inj_Error = id
136 instance Inj_Error (Con_Kind src) (Error_Unify src) where
137 inj_Error = Error_Unify_Kind
138
139 -- | Return the left spine of a 'Type':
140 -- the root 'Type' and its 'Type' parameters,
141 -- from the left to the right.
142 spineTy ::
143 forall src vs t.
144 Source src =>
145 Inj_Source (TypeVT src) src =>
146 Type src vs t ->
147 (TypeT src vs, [TypeT src vs])
148 spineTy typ = go [] typ
149 where
150 go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
151 go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
152 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
153 = go ctx t -- NOTE: skip the constraint @q@.
154 go ctx (TyApp _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f
155 go ctx t = (TypeT (t `source` TypeVT typ), ctx)
156
157 {-
158 spineTy
159 :: Type src ctx ss cs (t::k)
160 -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
161 -> ret
162 spineTy = go TypesZ
163 where
164 go :: Types src ctx ss cs hs
165 -> Type src ctx ss cs (t::k)
166 -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
167 -> ret
168 go ctx (TyApp _src f a) k = go (a `TypesS` ctx) f k
169 go ctx (Term x _te) k = go ctx x k
170 go ctx (TyAny x) k = go ctx x k
171 go ctx t k = k t ctx
172 -}
173
174 -- | Return the /most general unification/ of two 'Type's, when it exists.
175 unifyType ::
176 forall ki (x::ki) (y::ki) vs src.
177 Inj_Source (TypeVT src) src =>
178 Inj_Error (Con_Kind src) (Error_Unify src) =>
179 Subst src vs ->
180 Type src vs (x::ki) ->
181 Type src vs (y::ki) ->
182 Either (Error_Unify src) (Subst src vs)
183 unifyType vs x y =
184 let k = kindOfType x in
185 case (spineTy x, spineTy y) of
186 ((TypeT hx, px), (TypeT hy, py)) ->
187 case (hx, hy) of
188 (TyVar _ _n vx, _) | Just Refl <- k `eqKind` kindOfVar vx -> goVar vs vx y
189 (_, TyVar _ _n vy) | Just Refl <- k `eqKind` kindOfVar vy -> goVar vs vy x
190 (TyConst _sx _lx cx, TyConst _sy _ly cy)
191 | Just HRefl <- cx `eqConstKi` cy -> goList vs px py
192 | otherwise -> Left $ Error_Unify_Const_mismatch (TypeVT hx) (TypeVT hy)
193 _ ->
194 case (x, y) of
195 (TyApp _ fx ax, TyApp _ fy ay) ->
196 goList vs
197 [TypeT fx, TypeT ax]
198 [TypeT fy, TypeT ay]
199 _ -> Left $ Error_Unify_mismatch (TypeVT x) (TypeVT y)
200 where
201 goVar ::
202 forall k (a::k) (b::k) vs'.
203 Subst src vs' -> Var src vs' a -> Type src vs' b ->
204 Either (Error_Unify src) (Subst src vs')
205 goVar vs' va b =
206 case va `lookupSubst` vs' of
207 Just a -> unifyType vs' b a
208 Nothing ->
209 case vs' `subst` b of
210 TyVar _src _kb vb | Just HRefl <- va `eqVarKi` vb -> Right vs'
211 b' | va `varOccursIn` b' -> Left $ Error_Unify_Var_loop (indexVar va) (TypeVT b')
212 | Refl :: a :~: b <- unsafeCoerce Refl ->
213 Right $ insertSubst va b' mempty <> vs'
214 goList ::
215 forall vs'.
216 Subst src vs' -> [TypeT src vs'] -> [TypeT src vs'] ->
217 Either (Error_Unify src) (Subst src vs')
218 goList vs' [] [] = Right vs'
219 goList vs' (TypeT a:as) (TypeT b:bs) =
220 when_EqKind (kindOfType a) (kindOfType b) $ \Refl ->
221 unifyType vs' a b >>= \vs'' -> goList vs'' as bs
222 goList _vs _a _b = error "[BUG] unifyType: kinds mismatch"