Updated documentation; changed "group" to "branched" in type families
[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         ApartResult(..), 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 NotApart, which means a substitution can be found between
381    them,
382
383    Example: (Either a Int) and (Either Bool b) are NotApart, 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 NotApart 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 \begin{code}
437 -- See Note [Unification and apartness]
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 --
444 tcUnifyTys bind_fn tys1 tys2
445   | NotApart subst <- tcApartTys bind_fn tys1 tys2
446   = Just subst
447   | otherwise
448   = Nothing
449
450 data ApartResult = NotApart TvSubst   -- the subst that unifies the types
451                  | MaybeApart
452                  | SurelyApart
453
454 tcApartTys :: (TyVar -> BindFlag)
455            -> [Type] -> [Type]
456            -> ApartResult
457 tcApartTys bind_fn tys1 tys2
458   = initUM bind_fn $
459     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
460
461         -- Find the fixed point of the resulting non-idempotent substitution
462         ; return (niFixTvSubst subst) }
463 \end{code}
464
465
466 %************************************************************************
467 %*                                                                      *
468                 Non-idempotent substitution
469 %*                                                                      *
470 %************************************************************************
471
472 Note [Non-idempotent substitution]
473 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
474 During unification we use a TvSubstEnv that is
475   (a) non-idempotent
476   (b) loop-free; ie repeatedly applying it yields a fixed point
477
478 \begin{code}
479 niFixTvSubst :: TvSubstEnv -> TvSubst
480 -- Find the idempotent fixed point of the non-idempotent substitution
481 -- ToDo: use laziness instead of iteration?
482 niFixTvSubst env = f env
483   where
484     f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
485         | otherwise    = subst
486         where
487           range_tvs    = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
488           subst        = mkTvSubst (mkInScopeSet range_tvs) e 
489           not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
490           in_domain tv = tv `elemVarEnv` e
491
492 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
493 -- Apply the non-idempotent substitution to a set of type variables,
494 -- remembering that the substitution isn't necessarily idempotent
495 -- This is used in the occurs check, before extending the substitution
496 niSubstTvSet subst tvs
497   = foldVarSet (unionVarSet . get) emptyVarSet tvs
498   where
499     get tv = case lookupVarEnv subst tv of
500                Nothing -> unitVarSet tv
501                Just ty -> niSubstTvSet subst (tyVarsOfType ty)
502 \end{code}
503
504 %************************************************************************
505 %*                                                                      *
506                 The workhorse
507 %*                                                                      *
508 %************************************************************************
509
510 \begin{code}
511 unify :: TvSubstEnv     -- An existing substitution to extend
512       -> Type -> Type   -- Types to be unified, and witness of their equality
513       -> UM TvSubstEnv          -- Just the extended substitution, 
514                                 -- Nothing if unification failed
515 -- We do not require the incoming substitution to be idempotent,
516 -- nor guarantee that the outgoing one is.  That's fixed up by
517 -- the wrappers.
518
519 -- Respects newtypes, PredTypes
520
521 -- in unify, any NewTcApps/Preds should be taken at face value
522 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
523 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
524
525 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
526 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
527
528 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) 
529   | tyc1 == tyc2                                   = unify_tys subst tys1 tys2
530   | isSynFamilyTyCon tyc1 || isSynFamilyTyCon tyc2 = maybeApart
531
532 -- See Note [Unifying with type families]
533 unify _ (TyConApp tyc _) _
534   | isSynFamilyTyCon tyc = maybeApart
535 unify _ _ (TyConApp tyc _)
536   | isSynFamilyTyCon tyc = maybeApart
537
538 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
539   = do  { subst' <- unify subst ty1a ty2a
540         ; unify subst' ty1b ty2b }
541
542         -- Applications need a bit of care!
543         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
544         -- NB: we've already dealt with type variables and Notes,
545         -- so if one type is an App the other one jolly well better be too
546 unify subst (AppTy ty1a ty1b) ty2
547   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
548   = do  { subst' <- unify subst ty1a ty2a
549         ; unify subst' ty1b ty2b }
550
551 unify subst ty1 (AppTy ty2a ty2b)
552   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
553   = do  { subst' <- unify subst ty1a ty2a
554         ; unify subst' ty1b ty2b }
555
556 unify subst (LitTy x) (LitTy y) | x == y = return subst
557
558 unify _ _ _ = surelyApart
559         -- ForAlls??
560
561 ------------------------------
562 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
563 unify_tys subst xs ys = unifyList subst xs ys
564
565 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
566 unifyList subst orig_xs orig_ys
567   = go subst orig_xs orig_ys
568   where
569     go subst []     []     = return subst
570     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
571                                 ; go subst' xs ys }
572     go _ _ _ = surelyApart
573
574 ---------------------------------
575 uVar :: TvSubstEnv      -- An existing substitution to extend
576      -> TyVar           -- Type variable to be unified
577      -> Type            -- with this type
578      -> UM TvSubstEnv
579
580 uVar subst tv1 ty
581  = -- Check to see whether tv1 is refined by the substitution
582    case (lookupVarEnv subst tv1) of
583      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
584      Nothing  -> uUnrefined subst       -- No, continue
585                             tv1 ty ty
586
587 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
588            -> TyVar               -- Type variable to be unified
589            -> Type                -- with this type
590            -> Type                -- (version w/ expanded synonyms)
591            -> UM TvSubstEnv
592
593 -- We know that tv1 isn't refined
594
595 uUnrefined subst tv1 ty2 ty2'
596   | Just ty2'' <- tcView ty2'
597   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
598                 -- This is essential, in case we have
599                 --      type Foo a = a
600                 -- and then unify a ~ Foo a
601
602 uUnrefined subst tv1 ty2 (TyVarTy tv2)
603   | tv1 == tv2          -- Same type variable
604   = return subst
605
606     -- Check to see whether tv2 is refined
607   | Just ty' <- lookupVarEnv subst tv2
608   = uUnrefined subst tv1 ty' ty'
609
610   | otherwise
611
612   = do {   -- So both are unrefined; unify the kinds
613        ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)
614
615            -- And then bind one or the other, 
616            -- depending on which is bindable
617            -- NB: unlike TcUnify we do not have an elaborate sub-kinding 
618            --     story.  That is relevant only during type inference, and
619            --     (I very much hope) is not relevant here.
620        ; b1 <- tvBindFlag tv1
621        ; b2 <- tvBindFlag tv2
622        ; let ty1 = TyVarTy tv1
623        ; case (b1, b2) of
624            (Skolem, Skolem) -> maybeApart  -- See Note [Apartness with skolems]
625            (BindMe, _)      -> return (extendVarEnv subst' tv1 ty2)
626            (_, BindMe)      -> return (extendVarEnv subst' tv2 ty1) }
627
628 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
629   | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
630   = surelyApart                         -- Occurs check
631   | otherwise
632   = do { subst' <- unify subst k1 k2
633        ; bindTv subst' tv1 ty2 }        -- Bind tyvar to the synonym if poss
634   where
635     k1 = tyVarKind tv1
636     k2 = typeKind ty2'
637
638 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
639 bindTv subst tv ty      -- ty is not a type variable
640   = do  { b <- tvBindFlag tv
641         ; case b of
642             Skolem -> maybeApart  -- See Note [Apartness with skolems]
643             BindMe -> return $ extendVarEnv subst tv ty
644         }
645 \end{code}
646
647 %************************************************************************
648 %*                                                                      *
649                 Binding decisions
650 %*                                                                      *
651 %************************************************************************
652
653 \begin{code}
654 data BindFlag 
655   = BindMe      -- A regular type variable
656
657   | Skolem      -- This type variable is a skolem constant
658                 -- Don't bind it; it only matches itself
659 \end{code}
660
661
662 %************************************************************************
663 %*                                                                      *
664                 Unification monad
665 %*                                                                      *
666 %************************************************************************
667
668 \begin{code}
669 data UnifFailure = UFMaybeApart
670                  | UFSurelyApart
671
672 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
673                          -> Either UnifFailure a }
674
675 instance Monad UM where
676   return a = UM (\_tvs -> Right a)
677   fail _   = UM (\_tvs -> Left UFSurelyApart) -- failed pattern match
678   m >>= k  = UM (\tvs -> case unUM m tvs of
679                            Right v -> unUM (k v) tvs
680                            Left f  -> Left f)
681
682 initUM :: (TyVar -> BindFlag) -> UM TvSubst -> ApartResult
683 initUM badtvs um
684   = case unUM um badtvs of
685       Right subst        -> NotApart subst
686       Left UFMaybeApart  -> MaybeApart
687       Left UFSurelyApart -> SurelyApart
688     
689 tvBindFlag :: TyVar -> UM BindFlag
690 tvBindFlag tv = UM (\tv_fn -> Right (tv_fn tv))
691
692 maybeApart :: UM a
693 maybeApart = UM (\_tv_fn -> Left UFMaybeApart)
694
695 surelyApart :: UM a
696 surelyApart = UM (\_tv_fn -> Left UFSurelyApart)
697 \end{code}
698