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