Fix #10493.
[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.hs
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 ~R Int
284 So (T CoX)_R :: T X ~R 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 NB: typesCantMatch is subtly different than the apartness checks
322 elsewhere in this module. It reasons over *representational* equality
323 (saying that a newtype is not distinct from its representation) whereas
324 the checks in, say, tcUnifyTysFG are about *nominal* equality. tcUnifyTysFG
325 also assumes that its inputs are type-family-free, whereas no such assumption
326 is in play here.
327 -}
328
329 typesCantMatch :: [(Type,Type)] -> Bool
330 typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
331 where
332 cant_match :: Type -> Type -> Bool
333 cant_match t1 t2
334 | Just t1' <- coreView t1 = cant_match t1' t2
335 | Just t2' <- coreView t2 = cant_match t1 t2'
336
337 cant_match (FunTy a1 r1) (FunTy a2 r2)
338 = cant_match a1 a2 || cant_match r1 r2
339
340 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
341 | isDistinctTyCon tc1 && isDistinctTyCon tc2
342 = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
343
344 cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc
345 cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc
346 -- tc can't be FunTyCon by invariant
347
348 cant_match (AppTy f1 a1) ty2
349 | Just (f2, a2) <- repSplitAppTy_maybe ty2
350 = cant_match f1 f2 || cant_match a1 a2
351 cant_match ty1 (AppTy f2 a2)
352 | Just (f1, a1) <- repSplitAppTy_maybe ty1
353 = cant_match f1 f2 || cant_match a1 a2
354
355 cant_match (LitTy x) (LitTy y) = x /= y
356
357 cant_match _ _ = False -- Safe!
358
359 -- Things we could add;
360 -- foralls
361 -- look through newtypes
362 -- take account of tyvar bindings (EQ example above)
363
364 {-
365 ************************************************************************
366 * *
367 Unification
368 * *
369 ************************************************************************
370
371 Note [Fine-grained unification]
372 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
373 Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
374 no substitution to finite types makes these match. But, a substitution to
375 *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
376 Why do we care? Consider these two type family instances:
377
378 type instance F x x = Int
379 type instance F [y] y = Bool
380
381 If we also have
382
383 type instance Looper = [Looper]
384
385 then the instances potentially overlap. The solution is to use unification
386 over infinite terms. This is possible (see [1] for lots of gory details), but
387 a full algorithm is a little more power than we need. Instead, we make a
388 conservative approximation and just omit the occurs check.
389
390 [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
391
392 tcUnifyTys considers an occurs-check problem as the same as general unification
393 failure.
394
395 tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
396 failure ("MaybeApart"), or general failure ("SurelyApart").
397
398 See also Trac #8162.
399
400 It's worth noting that unification in the presence of infinite types is not
401 complete. This means that, sometimes, a closed type family does not reduce
402 when it should. See test case indexed-types/should_fail/Overlap15 for an
403 example.
404
405 Note [The substitution in MaybeApart]
406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
408 Because consider unifying these:
409
410 (a, a, Int) ~ (b, [b], Bool)
411
412 If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
413 apply the subst we have so far and discover that we need [b |-> [b]]. Because
414 this fails the occurs check, we say that the types are MaybeApart (see above
415 Note [Fine-grained unification]). But, we can't stop there! Because if we
416 continue, we discover that Int is SurelyApart from Bool, and therefore the
417 types are apart. This has practical consequences for the ability for closed
418 type family applications to reduce. See test case
419 indexed-types/should_compile/Overlap14.
420
421 Note [Unifying with skolems]
422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
423 If we discover that two types unify if and only if a skolem variable is
424 substituted, we can't properly unify the types. But, that skolem variable
425 may later be instantiated with a unifyable type. So, we return maybeApart
426 in these cases.
427
428 Note [Lists of different lengths are MaybeApart]
429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
431 lengths. The place where we know this can happen is from compatibleBranches in
432 FamInstEnv, when checking data family instances. Data family instances may be
433 eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
434
435 We wish to say that
436
437 D :: * -> * -> *
438 axDF1 :: D Int ~ DFInst1
439 axDF2 :: D Int Bool ~ DFInst2
440
441 overlap. If we conclude that lists of different lengths are SurelyApart, then
442 it will look like these do *not* overlap, causing disaster. See Trac #9371.
443
444 In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
445 which can't tell the difference between MaybeApart and SurelyApart, so those
446 usages won't notice this design choice.
447 -}
448
449 tcUnifyTy :: Type -> Type -- All tyvars are bindable
450 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
451 -- Simple unification of two types; all type variables are bindable
452 tcUnifyTy ty1 ty2
453 = case initUM (const BindMe) (unify emptyTvSubstEnv ty1 ty2) of
454 Unifiable subst_env -> Just (niFixTvSubst subst_env)
455 _other -> Nothing
456
457 -----------------
458 tcUnifyTys :: (TyVar -> BindFlag)
459 -> [Type] -> [Type]
460 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
461 -- The two types may have common type variables, and indeed do so in the
462 -- second call to tcUnifyTys in FunDeps.checkClsFD
463 tcUnifyTys bind_fn tys1 tys2
464 = case tcUnifyTysFG bind_fn tys1 tys2 of
465 Unifiable subst -> Just subst
466 _ -> Nothing
467
468 -- This type does double-duty. It is used in the UM (unifier monad) and to
469 -- return the final result. See Note [Fine-grained unification]
470 type UnifyResult = UnifyResultM TvSubst
471 data UnifyResultM a = Unifiable a -- the subst that unifies the types
472 | MaybeApart a -- the subst has as much as we know
473 -- it must be part of an most general unifier
474 -- See Note [The substitution in MaybeApart]
475 | SurelyApart
476
477 -- See Note [Fine-grained unification]
478 tcUnifyTysFG :: (TyVar -> BindFlag)
479 -> [Type] -> [Type]
480 -> UnifyResult
481 tcUnifyTysFG bind_fn tys1 tys2
482 = initUM bind_fn $
483 do { subst <- unifyList emptyTvSubstEnv tys1 tys2
484
485 -- Find the fixed point of the resulting non-idempotent substitution
486 ; return (niFixTvSubst subst) }
487
488 {-
489 ************************************************************************
490 * *
491 Non-idempotent substitution
492 * *
493 ************************************************************************
494
495 Note [Non-idempotent substitution]
496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
497 During unification we use a TvSubstEnv that is
498 (a) non-idempotent
499 (b) loop-free; ie repeatedly applying it yields a fixed point
500
501 Note [Finding the substitution fixpoint]
502 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
503 Finding the fixpoint of a non-idempotent substitution arising from a
504 unification is harder than it looks, because of kinds. Consider
505 T k (H k (f:k)) ~ T * (g:*)
506 If we unify, we get the substitution
507 [ k -> *
508 , g -> H k (f:k) ]
509 To make it idempotent we don't want to get just
510 [ k -> *
511 , g -> H * (f:k) ]
512 We also want to substitute inside f's kind, to get
513 [ k -> *
514 , g -> H k (f:*) ]
515 If we don't do this, we may apply the substitition to something,
516 and get an ill-formed type, i.e. one where typeKind will fail.
517 This happened, for example, in Trac #9106.
518
519 This is the reason for extending env with [f:k -> f:*], in the
520 definition of env' in niFixTvSubst
521 -}
522
523 niFixTvSubst :: TvSubstEnv -> TvSubst
524 -- Find the idempotent fixed point of the non-idempotent substitution
525 -- See Note [Finding the substitution fixpoint]
526 -- ToDo: use laziness instead of iteration?
527 niFixTvSubst env = f env
528 where
529 f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
530 | otherwise = subst
531 where
532 not_fixpoint = foldVarSet ((||) . in_domain) False all_range_tvs
533 in_domain tv = tv `elemVarEnv` env
534
535 range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
536 all_range_tvs = closeOverKinds range_tvs
537 subst = mkTvSubst (mkInScopeSet all_range_tvs) env
538
539 -- env' extends env by replacing any free type with
540 -- that same tyvar with a substituted kind
541 -- See note [Finding the substitution fixpoint]
542 env' = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
543 substTy subst $ tyVarKind rtv)
544 | rtv <- varSetElems range_tvs
545 , not (in_domain rtv) ]
546 subst' = mkTvSubst (mkInScopeSet all_range_tvs) env'
547
548 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
549 -- Apply the non-idempotent substitution to a set of type variables,
550 -- remembering that the substitution isn't necessarily idempotent
551 -- This is used in the occurs check, before extending the substitution
552 niSubstTvSet subst tvs
553 = foldVarSet (unionVarSet . get) emptyVarSet tvs
554 where
555 get tv = case lookupVarEnv subst tv of
556 Nothing -> unitVarSet tv
557 Just ty -> niSubstTvSet subst (tyVarsOfType ty)
558
559 {-
560 ************************************************************************
561 * *
562 The workhorse
563 * *
564 ************************************************************************
565 -}
566
567 unify :: TvSubstEnv -- An existing substitution to extend
568 -> Type -> Type -- Types to be unified, and witness of their equality
569 -> UM TvSubstEnv -- Just the extended substitution,
570 -- Nothing if unification failed
571 -- We do not require the incoming substitution to be idempotent,
572 -- nor guarantee that the outgoing one is. That's fixed up by
573 -- the wrappers.
574
575 -- Respects newtypes, PredTypes
576
577 -- in unify, any NewTcApps/Preds should be taken at face value
578 unify subst (TyVarTy tv1) ty2 = uVar subst tv1 ty2
579 unify subst ty1 (TyVarTy tv2) = uVar subst tv2 ty1
580
581 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
582 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
583
584 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
585 | tyc1 == tyc2
586 = unify_tys subst tys1 tys2
587
588 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
589 = do { subst' <- unify subst ty1a ty2a
590 ; unify subst' ty1b ty2b }
591
592 -- Applications need a bit of care!
593 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
594 -- NB: we've already dealt with type variables and Notes,
595 -- so if one type is an App the other one jolly well better be too
596 unify subst (AppTy ty1a ty1b) ty2
597 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
598 = do { subst' <- unify subst ty1a ty2a
599 ; unify subst' ty1b ty2b }
600
601 unify subst ty1 (AppTy ty2a ty2b)
602 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
603 = do { subst' <- unify subst ty1a ty2a
604 ; unify subst' ty1b ty2b }
605
606 unify subst (LitTy x) (LitTy y) | x == y = return subst
607
608 unify _ _ _ = surelyApart
609 -- ForAlls??
610
611 ------------------------------
612 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
613 unify_tys subst xs ys = unifyList subst xs ys
614
615 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
616 unifyList subst orig_xs orig_ys
617 = go subst orig_xs orig_ys
618 where
619 go subst [] [] = return subst
620 go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
621 ; go subst' xs ys }
622 go subst _ _ = maybeApart subst -- See Note [Lists of different lengths are MaybeApart]
623
624 ---------------------------------
625 uVar :: TvSubstEnv -- An existing substitution to extend
626 -> TyVar -- Type variable to be unified
627 -> Type -- with this type
628 -> UM TvSubstEnv
629
630 uVar subst tv1 ty
631 = -- Check to see whether tv1 is refined by the substitution
632 case (lookupVarEnv subst tv1) of
633 Just ty' -> unify subst ty' ty -- Yes, call back into unify'
634 Nothing -> uUnrefined subst -- No, continue
635 tv1 ty ty
636
637 uUnrefined :: TvSubstEnv -- An existing substitution to extend
638 -> TyVar -- Type variable to be unified
639 -> Type -- with this type
640 -> Type -- (version w/ expanded synonyms)
641 -> UM TvSubstEnv
642
643 -- We know that tv1 isn't refined
644
645 uUnrefined subst tv1 ty2 ty2'
646 | Just ty2'' <- tcView ty2'
647 = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
648 -- This is essential, in case we have
649 -- type Foo a = a
650 -- and then unify a ~ Foo a
651
652 uUnrefined subst tv1 ty2 (TyVarTy tv2)
653 | tv1 == tv2 -- Same type variable
654 = return subst
655
656 -- Check to see whether tv2 is refined
657 | Just ty' <- lookupVarEnv subst tv2
658 = uUnrefined subst tv1 ty' ty'
659
660 | otherwise
661
662 = do { -- So both are unrefined; unify the kinds
663 ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)
664
665 -- And then bind one or the other,
666 -- depending on which is bindable
667 -- NB: unlike TcUnify we do not have an elaborate sub-kinding
668 -- story. That is relevant only during type inference, and
669 -- (I very much hope) is not relevant here.
670 ; b1 <- tvBindFlag tv1
671 ; b2 <- tvBindFlag tv2
672 ; let ty1 = TyVarTy tv1
673 ; case (b1, b2) of
674 (Skolem, Skolem) -> maybeApart subst' -- See Note [Unification with skolems]
675 (BindMe, _) -> return (extendVarEnv subst' tv1 ty2)
676 (_, BindMe) -> return (extendVarEnv subst' tv2 ty1) }
677
678 uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
679 | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
680 = maybeApart subst -- Occurs check
681 -- See Note [Fine-grained unification]
682 | otherwise
683 = do { subst' <- unify subst k1 k2
684 -- Note [Kinds Containing Only Literals]
685 ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss
686 where
687 k1 = tyVarKind tv1
688 k2 = typeKind ty2'
689
690 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
691 bindTv subst tv ty -- ty is not a type variable
692 = do { b <- tvBindFlag tv
693 ; case b of
694 Skolem -> maybeApart subst -- See Note [Unification with skolems]
695 BindMe -> return $ extendVarEnv subst tv ty
696 }
697
698 {-
699 ************************************************************************
700 * *
701 Binding decisions
702 * *
703 ************************************************************************
704 -}
705
706 data BindFlag
707 = BindMe -- A regular type variable
708
709 | Skolem -- This type variable is a skolem constant
710 -- Don't bind it; it only matches itself
711
712 {-
713 ************************************************************************
714 * *
715 Unification monad
716 * *
717 ************************************************************************
718 -}
719
720 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
721 -> UnifyResultM a }
722
723 instance Functor UM where
724 fmap = liftM
725
726 instance Applicative UM where
727 pure = return
728 (<*>) = ap
729
730 instance Monad UM where
731 return a = UM (\_tvs -> Unifiable a)
732 fail _ = UM (\_tvs -> SurelyApart) -- failed pattern match
733 m >>= k = UM (\tvs -> case unUM m tvs of
734 Unifiable v -> unUM (k v) tvs
735 MaybeApart v ->
736 case unUM (k v) tvs of
737 Unifiable v' -> MaybeApart v'
738 other -> other
739 SurelyApart -> SurelyApart)
740
741 initUM :: (TyVar -> BindFlag) -> UM a -> UnifyResultM a
742 initUM badtvs um = unUM um badtvs
743
744 tvBindFlag :: TyVar -> UM BindFlag
745 tvBindFlag tv = UM (\tv_fn -> Unifiable (tv_fn tv))
746
747 maybeApart :: TvSubstEnv -> UM TvSubstEnv
748 maybeApart subst = UM (\_tv_fn -> MaybeApart subst)
749
750 surelyApart :: UM a
751 surelyApart = UM (\_tv_fn -> SurelyApart)