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