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