unlit compiler/types/ modules
[ghc.git] / compiler / types / Unify.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP #-}
4
5 module Unify (
6 -- Matching of types:
7 -- the "tc" prefix indicates that matching always
8 -- respects newtypes (rather than looking through them)
9 tcMatchTy, tcMatchTys, tcMatchTyX,
10 ruleMatchTyX, tcMatchPreds,
11
12 MatchEnv(..), matchList,
13
14 typesCantMatch,
15
16 -- Side-effect free unification
17 tcUnifyTy, tcUnifyTys, BindFlag(..),
18
19 UnifyResultM(..), UnifyResult, tcUnifyTysFG
20
21 ) where
22
23 #include "HsVersions.h"
24
25 import Var
26 import VarEnv
27 import VarSet
28 import Kind
29 import Type
30 import TyCon
31 import TypeRep
32 import Util
33
34 import Control.Monad (liftM, ap)
35 #if __GLASGOW_HASKELL__ < 709
36 import Control.Applicative (Applicative(..))
37 #endif
38
39 {-
40 ************************************************************************
41 * *
42 Matching
43 * *
44 ************************************************************************
45
46
47 Matching is much tricker than you might think.
48
49 1. The substitution we generate binds the *template type variables*
50 which are given to us explicitly.
51
52 2. We want to match in the presence of foralls;
53 e.g (forall a. t1) ~ (forall b. t2)
54
55 That is what the RnEnv2 is for; it does the alpha-renaming
56 that makes it as if a and b were the same variable.
57 Initialising the RnEnv2, so that it can generate a fresh
58 binder when necessary, entails knowing the free variables of
59 both types.
60
61 3. We must be careful not to bind a template type variable to a
62 locally bound variable. E.g.
63 (forall a. x) ~ (forall b. b)
64 where x is the template type variable. Then we do not want to
65 bind x to a/b! This is a kind of occurs check.
66 The necessary locals accumulate in the RnEnv2.
67 -}
68
69 data MatchEnv
70 = ME { me_tmpls :: VarSet -- Template variables
71 , me_env :: RnEnv2 -- Renaming envt for nested foralls
72 } -- In-scope set includes template variables
73 -- Nota Bene: MatchEnv isn't specific to Types. It is used
74 -- for matching terms and coercions as well as types
75
76 tcMatchTy :: TyVarSet -- Template tyvars
77 -> Type -- Template
78 -> Type -- Target
79 -> Maybe TvSubst -- One-shot; in principle the template
80 -- variables could be free in the target
81
82 tcMatchTy tmpls ty1 ty2
83 = case match menv emptyTvSubstEnv ty1 ty2 of
84 Just subst_env -> Just (TvSubst in_scope subst_env)
85 Nothing -> Nothing
86 where
87 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
88 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
89 -- We're assuming that all the interesting
90 -- tyvars in tys1 are in tmpls
91
92 tcMatchTys :: TyVarSet -- Template tyvars
93 -> [Type] -- Template
94 -> [Type] -- Target
95 -> Maybe TvSubst -- One-shot; in principle the template
96 -- variables could be free in the target
97
98 tcMatchTys tmpls tys1 tys2
99 = case match_tys menv emptyTvSubstEnv tys1 tys2 of
100 Just subst_env -> Just (TvSubst in_scope subst_env)
101 Nothing -> Nothing
102 where
103 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
104 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
105 -- We're assuming that all the interesting
106 -- tyvars in tys1 are in tmpls
107
108 -- This is similar, but extends a substitution
109 tcMatchTyX :: TyVarSet -- Template tyvars
110 -> TvSubst -- Substitution to extend
111 -> Type -- Template
112 -> Type -- Target
113 -> Maybe TvSubst
114 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
115 = case match menv subst_env ty1 ty2 of
116 Just subst_env -> Just (TvSubst in_scope subst_env)
117 Nothing -> Nothing
118 where
119 menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
120
121 tcMatchPreds
122 :: [TyVar] -- Bind these
123 -> [PredType] -> [PredType]
124 -> Maybe TvSubstEnv
125 tcMatchPreds tmpls ps1 ps2
126 = matchList (match menv) emptyTvSubstEnv ps1 ps2
127 where
128 menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
129 in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2)
130
131 -- This one is called from the expression matcher, which already has a MatchEnv in hand
132 ruleMatchTyX :: MatchEnv
133 -> TvSubstEnv -- Substitution to extend
134 -> Type -- Template
135 -> Type -- Target
136 -> Maybe TvSubstEnv
137
138 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
139
140 -- Now the internals of matching
141
142 match :: MatchEnv -- For the most part this is pushed downwards
143 -> TvSubstEnv -- Substitution so far:
144 -- Domain is subset of template tyvars
145 -- Free vars of range is subset of
146 -- in-scope set of the RnEnv2
147 -> Type -> Type -- Template and target respectively
148 -> Maybe TvSubstEnv
149
150 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
151 | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
152
153 match menv subst (TyVarTy tv1) ty2
154 | Just ty1' <- lookupVarEnv subst tv1' -- tv1' is already bound
155 = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
156 -- ty1 has no locally-bound variables, hence nukeRnEnvL
157 then Just subst
158 else Nothing -- ty2 doesn't match
159
160 | tv1' `elemVarSet` me_tmpls menv
161 = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
162 then Nothing -- Occurs check
163 else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
164 -- Note [Matching kinds]
165 ; return (extendVarEnv subst1 tv1' ty2) }
166
167 | otherwise -- tv1 is not a template tyvar
168 = case ty2 of
169 TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
170 _ -> Nothing
171 where
172 rn_env = me_env menv
173 tv1' = rnOccL rn_env tv1
174
175 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
176 = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2)
177 ; match menv' subst' ty1 ty2 }
178 where -- Use the magic of rnBndr2 to go under the binders
179 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
180
181 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
182 | tc1 == tc2 = match_tys menv subst tys1 tys2
183 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
184 = do { subst' <- match menv subst ty1a ty2a
185 ; match menv subst' ty1b ty2b }
186 match menv subst (AppTy ty1a ty1b) ty2
187 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
188 -- 'repSplit' used because the tcView stuff is done above
189 = do { subst' <- match menv subst ty1a ty2a
190 ; match menv subst' ty1b ty2b }
191
192 match _ subst (LitTy x) (LitTy y) | x == y = return subst
193
194 match _ _ _ _
195 = Nothing
196
197
198
199 --------------
200 match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
201 -- Match the kind of the template tyvar with the kind of Type
202 -- Note [Matching kinds]
203 match_kind menv subst k1 k2
204 | k2 `isSubKind` k1
205 = return subst
206
207 | otherwise
208 = match menv subst k1 k2
209
210 -- Note [Matching kinds]
211 -- ~~~~~~~~~~~~~~~~~~~~~
212 -- For ordinary type variables, we don't want (m a) to match (n b)
213 -- if say (a::*) and (b::*->*). This is just a yes/no issue.
214 --
215 -- For coercion kinds matters are more complicated. If we have a
216 -- coercion template variable co::a~[b], where a,b are presumably also
217 -- template type variables, then we must match co's kind against the
218 -- kind of the actual argument, so as to give bindings to a,b.
219 --
220 -- In fact I have no example in mind that *requires* this kind-matching
221 -- to instantiate template type variables, but it seems like the right
222 -- thing to do. C.f. Note [Matching variable types] in Rules.lhs
223
224 --------------
225 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
226 match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
227
228 --------------
229 matchList :: (env -> a -> b -> Maybe env)
230 -> env -> [a] -> [b] -> Maybe env
231 matchList _ subst [] [] = Just subst
232 matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
233 ; matchList fn subst' as bs }
234 matchList _ _ _ _ = Nothing
235
236 {-
237 ************************************************************************
238 * *
239 GADTs
240 * *
241 ************************************************************************
242
243 Note [Pruning dead case alternatives]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 Consider data T a where
246 T1 :: T Int
247 T2 :: T a
248
249 newtype X = MkX Int
250 newtype Y = MkY Char
251
252 type family F a
253 type instance F Bool = Int
254
255 Now consider case x of { T1 -> e1; T2 -> e2 }
256
257 The question before the house is this: if I know something about the type
258 of x, can I prune away the T1 alternative?
259
260 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
261 Answer = YES we can prune the T1 branch (clearly)
262
263 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
264 to 'Bool', in which case x::T Int, so
265 ANSWER = NO (clearly)
266
267 Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom)
268 value of type (T X) using T1. But *in FC* it's quite possible. The newtype
269 gives a coercion
270 CoX :: X ~ Int
271 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
272 of type (T X) constructed with T1. Hence
273 ANSWER = NO we can't prune the T1 branch (surprisingly)
274
275 Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving
276 mechanism uses a cast, just as above, to move from one dictionary to another,
277 in effect giving the programmer access to CoX.
278
279 Finally, suppose x::T Y. Then *even in FC* we can't construct a
280 non-bottom value of type (T Y) using T1. That's because we can get
281 from Y to Char, but not to Int.
282
283
284 Here's a related question. data Eq a b where EQ :: Eq a a
285 Consider
286 case x of { EQ -> ... }
287
288 Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
289
290 What about x::Eq Int a, in a context where we have evidence that a~Char.
291 Then again the alternative is dead.
292
293
294 Summary
295
296 We are really doing a test for unsatisfiability of the type
297 constraints implied by the match. And that is clearly, in general, a
298 hard thing to do.
299
300 However, since we are simply dropping dead code, a conservative test
301 suffices. There is a continuum of tests, ranging from easy to hard, that
302 drop more and more dead code.
303
304 For now we implement a very simple test: type variables match
305 anything, type functions (incl newtypes) match anything, and only
306 distinct data types fail to match. We can elaborate later.
307 -}
308
309 typesCantMatch :: [(Type,Type)] -> Bool
310 typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
311 where
312 cant_match :: Type -> Type -> Bool
313 cant_match t1 t2
314 | Just t1' <- coreView t1 = cant_match t1' t2
315 | Just t2' <- coreView t2 = cant_match t1 t2'
316
317 cant_match (FunTy a1 r1) (FunTy a2 r2)
318 = cant_match a1 a2 || cant_match r1 r2
319
320 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
321 | isDistinctTyCon tc1 && isDistinctTyCon tc2
322 = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
323
324 cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc
325 cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc
326 -- tc can't be FunTyCon by invariant
327
328 cant_match (AppTy f1 a1) ty2
329 | Just (f2, a2) <- repSplitAppTy_maybe ty2
330 = cant_match f1 f2 || cant_match a1 a2
331 cant_match ty1 (AppTy f2 a2)
332 | Just (f1, a1) <- repSplitAppTy_maybe ty1
333 = cant_match f1 f2 || cant_match a1 a2
334
335 cant_match (LitTy x) (LitTy y) = x /= y
336
337 cant_match _ _ = False -- Safe!
338
339 -- Things we could add;
340 -- foralls
341 -- look through newtypes
342 -- take account of tyvar bindings (EQ example above)
343
344 {-
345 ************************************************************************
346 * *
347 Unification
348 * *
349 ************************************************************************
350
351 Note [Fine-grained unification]
352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
353 Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
354 no substitution to finite types makes these match. But, a substitution to
355 *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
356 Why do we care? Consider these two type family instances:
357
358 type instance F x x = Int
359 type instance F [y] y = Bool
360
361 If we also have
362
363 type instance Looper = [Looper]
364
365 then the instances potentially overlap. The solution is to use unification
366 over infinite terms. This is possible (see [1] for lots of gory details), but
367 a full algorithm is a little more power than we need. Instead, we make a
368 conservative approximation and just omit the occurs check.
369
370 [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
371
372 tcUnifyTys considers an occurs-check problem as the same as general unification
373 failure.
374
375 tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
376 failure ("MaybeApart"), or general failure ("SurelyApart").
377
378 See also Trac #8162.
379
380 It's worth noting that unification in the presence of infinite types is not
381 complete. This means that, sometimes, a closed type family does not reduce
382 when it should. See test case indexed-types/should_fail/Overlap15 for an
383 example.
384
385 Note [The substitution in MaybeApart]
386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
387 The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
388 Because consider unifying these:
389
390 (a, a, Int) ~ (b, [b], Bool)
391
392 If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
393 apply the subst we have so far and discover that we need [b |-> [b]]. Because
394 this fails the occurs check, we say that the types are MaybeApart (see above
395 Note [Fine-grained unification]). But, we can't stop there! Because if we
396 continue, we discover that Int is SurelyApart from Bool, and therefore the
397 types are apart. This has practical consequences for the ability for closed
398 type family applications to reduce. See test case
399 indexed-types/should_compile/Overlap14.
400
401 Note [Unifying with skolems]
402 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
403 If we discover that two types unify if and only if a skolem variable is
404 substituted, we can't properly unify the types. But, that skolem variable
405 may later be instantiated with a unifyable type. So, we return maybeApart
406 in these cases.
407
408 Note [Lists of different lengths are MaybeApart]
409 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
410 It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
411 lengths. The place where we know this can happen is from compatibleBranches in
412 FamInstEnv, when checking data family instances. Data family instances may be
413 eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
414
415 We wish to say that
416
417 D :: * -> * -> *
418 axDF1 :: D Int ~ DFInst1
419 axDF2 :: D Int Bool ~ DFInst2
420
421 overlap. If we conclude that lists of different lengths are SurelyApart, then
422 it will look like these do *not* overlap, causing disaster. See Trac #9371.
423
424 In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
425 which can't tell the difference between MaybeApart and SurelyApart, so those
426 usages won't notice this design choice.
427 -}
428
429 tcUnifyTy :: Type -> Type -- All tyvars are bindable
430 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
431 -- Simple unification of two types; all type variables are bindable
432 tcUnifyTy ty1 ty2
433 = case initUM (const BindMe) (unify emptyTvSubstEnv ty1 ty2) of
434 Unifiable subst_env -> Just (niFixTvSubst subst_env)
435 _other -> Nothing
436
437 -----------------
438 tcUnifyTys :: (TyVar -> BindFlag)
439 -> [Type] -> [Type]
440 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
441 -- The two types may have common type variables, and indeed do so in the
442 -- second call to tcUnifyTys in FunDeps.checkClsFD
443 tcUnifyTys bind_fn tys1 tys2
444 = case tcUnifyTysFG bind_fn tys1 tys2 of
445 Unifiable subst -> Just subst
446 _ -> Nothing
447
448 -- This type does double-duty. It is used in the UM (unifier monad) and to
449 -- return the final result. See Note [Fine-grained unification]
450 type UnifyResult = UnifyResultM TvSubst
451 data UnifyResultM a = Unifiable a -- the subst that unifies the types
452 | MaybeApart a -- the subst has as much as we know
453 -- it must be part of an most general unifier
454 -- See Note [The substitution in MaybeApart]
455 | SurelyApart
456
457 -- See Note [Fine-grained unification]
458 tcUnifyTysFG :: (TyVar -> BindFlag)
459 -> [Type] -> [Type]
460 -> UnifyResult
461 tcUnifyTysFG bind_fn tys1 tys2
462 = initUM bind_fn $
463 do { subst <- unifyList emptyTvSubstEnv tys1 tys2
464
465 -- Find the fixed point of the resulting non-idempotent substitution
466 ; return (niFixTvSubst subst) }
467
468 {-
469 ************************************************************************
470 * *
471 Non-idempotent substitution
472 * *
473 ************************************************************************
474
475 Note [Non-idempotent substitution]
476 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
477 During unification we use a TvSubstEnv that is
478 (a) non-idempotent
479 (b) loop-free; ie repeatedly applying it yields a fixed point
480
481 Note [Finding the substitution fixpoint]
482 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
483 Finding the fixpoint of a non-idempotent substitution arising from a
484 unification is harder than it looks, because of kinds. Consider
485 T k (H k (f:k)) ~ T * (g:*)
486 If we unify, we get the substitution
487 [ k -> *
488 , g -> H k (f:k) ]
489 To make it idempotent we don't want to get just
490 [ k -> *
491 , g -> H * (f:k) ]
492 We also want to substitute inside f's kind, to get
493 [ k -> *
494 , g -> H k (f:*) ]
495 If we don't do this, we may apply the substitition to something,
496 and get an ill-formed type, i.e. one where typeKind will fail.
497 This happened, for example, in Trac #9106.
498
499 This is the reason for extending env with [f:k -> f:*], in the
500 definition of env' in niFixTvSubst
501 -}
502
503 niFixTvSubst :: TvSubstEnv -> TvSubst
504 -- Find the idempotent fixed point of the non-idempotent substitution
505 -- See Note [Finding the substitution fixpoint]
506 -- ToDo: use laziness instead of iteration?
507 niFixTvSubst env = f env
508 where
509 f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
510 | otherwise = subst
511 where
512 not_fixpoint = foldVarSet ((||) . in_domain) False all_range_tvs
513 in_domain tv = tv `elemVarEnv` env
514
515 range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
516 all_range_tvs = closeOverKinds range_tvs
517 subst = mkTvSubst (mkInScopeSet all_range_tvs) env
518
519 -- env' extends env by replacing any free type with
520 -- that same tyvar with a substituted kind
521 -- See note [Finding the substitution fixpoint]
522 env' = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
523 substTy subst $ tyVarKind rtv)
524 | rtv <- varSetElems range_tvs
525 , not (in_domain rtv) ]
526 subst' = mkTvSubst (mkInScopeSet all_range_tvs) env'
527
528 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
529 -- Apply the non-idempotent substitution to a set of type variables,
530 -- remembering that the substitution isn't necessarily idempotent
531 -- This is used in the occurs check, before extending the substitution
532 niSubstTvSet subst tvs
533 = foldVarSet (unionVarSet . get) emptyVarSet tvs
534 where
535 get tv = case lookupVarEnv subst tv of
536 Nothing -> unitVarSet tv
537 Just ty -> niSubstTvSet subst (tyVarsOfType ty)
538
539 {-
540 ************************************************************************
541 * *
542 The workhorse
543 * *
544 ************************************************************************
545 -}
546
547 unify :: TvSubstEnv -- An existing substitution to extend
548 -> Type -> Type -- Types to be unified, and witness of their equality
549 -> UM TvSubstEnv -- Just the extended substitution,
550 -- Nothing if unification failed
551 -- We do not require the incoming substitution to be idempotent,
552 -- nor guarantee that the outgoing one is. That's fixed up by
553 -- the wrappers.
554
555 -- Respects newtypes, PredTypes
556
557 -- in unify, any NewTcApps/Preds should be taken at face value
558 unify subst (TyVarTy tv1) ty2 = uVar subst tv1 ty2
559 unify subst ty1 (TyVarTy tv2) = uVar subst tv2 ty1
560
561 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
562 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
563
564 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
565 | tyc1 == tyc2
566 = unify_tys subst tys1 tys2
567
568 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
569 = do { subst' <- unify subst ty1a ty2a
570 ; unify subst' ty1b ty2b }
571
572 -- Applications need a bit of care!
573 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
574 -- NB: we've already dealt with type variables and Notes,
575 -- so if one type is an App the other one jolly well better be too
576 unify subst (AppTy ty1a ty1b) ty2
577 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
578 = do { subst' <- unify subst ty1a ty2a
579 ; unify subst' ty1b ty2b }
580
581 unify subst ty1 (AppTy ty2a ty2b)
582 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
583 = do { subst' <- unify subst ty1a ty2a
584 ; unify subst' ty1b ty2b }
585
586 unify subst (LitTy x) (LitTy y) | x == y = return subst
587
588 unify _ _ _ = surelyApart
589 -- ForAlls??
590
591 ------------------------------
592 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
593 unify_tys subst xs ys = unifyList subst xs ys
594
595 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
596 unifyList subst orig_xs orig_ys
597 = go subst orig_xs orig_ys
598 where
599 go subst [] [] = return subst
600 go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
601 ; go subst' xs ys }
602 go subst _ _ = maybeApart subst -- See Note [Lists of different lengths are MaybeApart]
603
604 ---------------------------------
605 uVar :: TvSubstEnv -- An existing substitution to extend
606 -> TyVar -- Type variable to be unified
607 -> Type -- with this type
608 -> UM TvSubstEnv
609
610 uVar subst tv1 ty
611 = -- Check to see whether tv1 is refined by the substitution
612 case (lookupVarEnv subst tv1) of
613 Just ty' -> unify subst ty' ty -- Yes, call back into unify'
614 Nothing -> uUnrefined subst -- No, continue
615 tv1 ty ty
616
617 uUnrefined :: TvSubstEnv -- An existing substitution to extend
618 -> TyVar -- Type variable to be unified
619 -> Type -- with this type
620 -> Type -- (version w/ expanded synonyms)
621 -> UM TvSubstEnv
622
623 -- We know that tv1 isn't refined
624
625 uUnrefined subst tv1 ty2 ty2'
626 | Just ty2'' <- tcView ty2'
627 = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
628 -- This is essential, in case we have
629 -- type Foo a = a
630 -- and then unify a ~ Foo a
631
632 uUnrefined subst tv1 ty2 (TyVarTy tv2)
633 | tv1 == tv2 -- Same type variable
634 = return subst
635
636 -- Check to see whether tv2 is refined
637 | Just ty' <- lookupVarEnv subst tv2
638 = uUnrefined subst tv1 ty' ty'
639
640 | otherwise
641
642 = do { -- So both are unrefined; unify the kinds
643 ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)
644
645 -- And then bind one or the other,
646 -- depending on which is bindable
647 -- NB: unlike TcUnify we do not have an elaborate sub-kinding
648 -- story. That is relevant only during type inference, and
649 -- (I very much hope) is not relevant here.
650 ; b1 <- tvBindFlag tv1
651 ; b2 <- tvBindFlag tv2
652 ; let ty1 = TyVarTy tv1
653 ; case (b1, b2) of
654 (Skolem, Skolem) -> maybeApart subst' -- See Note [Unification with skolems]
655 (BindMe, _) -> return (extendVarEnv subst' tv1 ty2)
656 (_, BindMe) -> return (extendVarEnv subst' tv2 ty1) }
657
658 uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
659 | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
660 = maybeApart subst -- Occurs check
661 -- See Note [Fine-grained unification]
662 | otherwise
663 = do { subst' <- unify subst k1 k2
664 -- Note [Kinds Containing Only Literals]
665 ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss
666 where
667 k1 = tyVarKind tv1
668 k2 = typeKind ty2'
669
670 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
671 bindTv subst tv ty -- ty is not a type variable
672 = do { b <- tvBindFlag tv
673 ; case b of
674 Skolem -> maybeApart subst -- See Note [Unification with skolems]
675 BindMe -> return $ extendVarEnv subst tv ty
676 }
677
678 {-
679 ************************************************************************
680 * *
681 Binding decisions
682 * *
683 ************************************************************************
684 -}
685
686 data BindFlag
687 = BindMe -- A regular type variable
688
689 | Skolem -- This type variable is a skolem constant
690 -- Don't bind it; it only matches itself
691
692 {-
693 ************************************************************************
694 * *
695 Unification monad
696 * *
697 ************************************************************************
698 -}
699
700 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
701 -> UnifyResultM a }
702
703 instance Functor UM where
704 fmap = liftM
705
706 instance Applicative UM where
707 pure = return
708 (<*>) = ap
709
710 instance Monad UM where
711 return a = UM (\_tvs -> Unifiable a)
712 fail _ = UM (\_tvs -> SurelyApart) -- failed pattern match
713 m >>= k = UM (\tvs -> case unUM m tvs of
714 Unifiable v -> unUM (k v) tvs
715 MaybeApart v ->
716 case unUM (k v) tvs of
717 Unifiable v' -> MaybeApart v'
718 other -> other
719 SurelyApart -> SurelyApart)
720
721 initUM :: (TyVar -> BindFlag) -> UM a -> UnifyResultM a
722 initUM badtvs um = unUM um badtvs
723
724 tvBindFlag :: TyVar -> UM BindFlag
725 tvBindFlag tv = UM (\tv_fn -> Unifiable (tv_fn tv))
726
727 maybeApart :: TvSubstEnv -> UM TvSubstEnv
728 maybeApart subst = UM (\_tv_fn -> MaybeApart subst)
729
730 surelyApart :: UM a
731 surelyApart = UM (\_tv_fn -> SurelyApart)