Comments only: replace ":=:" by "~" (notation for equality predicates)
[ghc.git] / compiler / types / Unify.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module Unify ( 
7         -- Matching of types: 
8         --      the "tc" prefix indicates that matching always
9         --      respects newtypes (rather than looking through them)
10         tcMatchTy, tcMatchTys, tcMatchTyX, 
11         ruleMatchTyX, tcMatchPreds, MatchEnv(..),
12         
13         dataConCannotMatch,
14
15         -- GADT type refinement
16         Refinement, emptyRefinement, isEmptyRefinement, 
17         matchRefine, refineType, refinePred, refineResType,
18
19         -- side-effect free unification
20         tcUnifyTys, BindFlag(..)
21
22    ) where
23
24 #include "HsVersions.h"
25
26 import Var
27 import VarEnv
28 import VarSet
29 import Type
30 import Coercion
31 import TyCon
32 import DataCon
33 import TypeRep
34 import Outputable
35 import ErrUtils
36 import Util
37 import Maybes
38 import UniqFM
39 import FastString
40 \end{code}
41
42
43 %************************************************************************
44 %*                                                                      *
45                 Matching
46 %*                                                                      *
47 %************************************************************************
48
49
50 Matching is much tricker than you might think.
51
52 1. The substitution we generate binds the *template type variables*
53    which are given to us explicitly.
54
55 2. We want to match in the presence of foralls; 
56         e.g     (forall a. t1) ~ (forall b. t2)
57
58    That is what the RnEnv2 is for; it does the alpha-renaming
59    that makes it as if a and b were the same variable.
60    Initialising the RnEnv2, so that it can generate a fresh
61    binder when necessary, entails knowing the free variables of
62    both types.
63
64 3. We must be careful not to bind a template type variable to a
65    locally bound variable.  E.g.
66         (forall a. x) ~ (forall b. b)
67    where x is the template type variable.  Then we do not want to
68    bind x to a/b!  This is a kind of occurs check.
69    The necessary locals accumulate in the RnEnv2.
70
71
72 \begin{code}
73 data MatchEnv
74   = ME  { me_tmpls :: VarSet    -- Template tyvars
75         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
76         }                       --   In-scope set includes template tyvars
77
78 tcMatchTy :: TyVarSet           -- Template tyvars
79           -> Type               -- Template
80           -> Type               -- Target
81           -> Maybe TvSubst      -- One-shot; in principle the template
82                                 -- variables could be free in the target
83
84 tcMatchTy tmpls ty1 ty2
85   = case match menv emptyTvSubstEnv ty1 ty2 of
86         Just subst_env -> Just (TvSubst in_scope subst_env)
87         Nothing        -> Nothing
88   where
89     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
90     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
91         -- We're assuming that all the interesting 
92         -- tyvars in tys1 are in tmpls
93
94 tcMatchTys :: TyVarSet          -- Template tyvars
95            -> [Type]            -- Template
96            -> [Type]            -- Target
97            -> Maybe TvSubst     -- One-shot; in principle the template
98                                 -- variables could be free in the target
99
100 tcMatchTys tmpls tys1 tys2
101   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
102         Just subst_env -> Just (TvSubst in_scope subst_env)
103         Nothing        -> Nothing
104   where
105     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
106     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
107         -- We're assuming that all the interesting 
108         -- tyvars in tys1 are in tmpls
109
110 -- This is similar, but extends a substitution
111 tcMatchTyX :: TyVarSet          -- Template tyvars
112            -> TvSubst           -- Substitution to extend
113            -> Type              -- Template
114            -> Type              -- Target
115            -> Maybe TvSubst
116 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
117   = case match menv subst_env ty1 ty2 of
118         Just subst_env -> Just (TvSubst in_scope subst_env)
119         Nothing        -> Nothing
120   where
121     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
122
123 tcMatchPreds
124         :: [TyVar]                      -- Bind these
125         -> [PredType] -> [PredType]
126         -> Maybe TvSubstEnv
127 tcMatchPreds tmpls ps1 ps2
128   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
129   where
130     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
131     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
132
133 -- This one is called from the expression matcher, which already has a MatchEnv in hand
134 ruleMatchTyX :: MatchEnv 
135          -> TvSubstEnv          -- Substitution to extend
136          -> Type                -- Template
137          -> Type                -- Target
138          -> Maybe TvSubstEnv
139
140 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
141 \end{code}
142
143 Now the internals of matching
144
145 \begin{code}
146 match :: MatchEnv       -- For the most part this is pushed downwards
147       -> TvSubstEnv     -- Substitution so far:
148                         --   Domain is subset of template tyvars
149                         --   Free vars of range is subset of 
150                         --      in-scope set of the RnEnv2
151       -> Type -> Type   -- Template and target respectively
152       -> Maybe TvSubstEnv
153 -- This matcher works on core types; that is, it ignores PredTypes
154 -- Watch out if newtypes become transparent agin!
155 --      this matcher must respect newtypes
156
157 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
158                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
159
160 match menv subst (TyVarTy tv1) ty2
161   | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
162   = if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
163         -- ty1 has no locally-bound variables, hence nukeRnEnvL
164         -- Note tcEqType...we are doing source-type matching here
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 tv1 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   = match menv' subst ty1 ty2
185   where         -- Use the magic of rnBndr2 to go under the binders
186     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
187
188 match menv subst (PredTy p1) (PredTy p2) 
189   = match_pred menv subst p1 p2
190 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
191   | tc1 == tc2 = match_tys menv subst tys1 tys2
192 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
193   = do { subst' <- match menv subst ty1a ty2a
194        ; match menv subst' ty1b ty2b }
195 match menv subst (AppTy ty1a ty1b) ty2
196   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
197         -- 'repSplit' used because the tcView stuff is done above
198   = do { subst' <- match menv subst ty1a ty2a
199        ; match menv subst' ty1b ty2b }
200
201 match _ _ _ _
202   = Nothing
203
204 --------------
205 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
206 -- Match the kind of the template tyvar with the kind of Type
207 -- Note [Matching kinds]
208 match_kind menv subst tv ty
209   | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
210                           (ty3,ty4) = coercionKind ty
211                     ; subst1 <- match menv subst ty1 ty3
212                     ; match menv subst1 ty2 ty4 }
213   | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
214                  then Just subst
215                  else Nothing
216
217 -- Note [Matching kinds]
218 -- ~~~~~~~~~~~~~~~~~~~~~
219 -- For ordinary type variables, we don't want (m a) to match (n b) 
220 -- if say (a::*) and (b::*->*).  This is just a yes/no issue. 
221 --
222 -- For coercion kinds matters are more complicated.  If we have a 
223 -- coercion template variable co::a~[b], where a,b are presumably also
224 -- template type variables, then we must match co's kind against the 
225 -- kind of the actual argument, so as to give bindings to a,b.  
226 --
227 -- In fact I have no example in mind that *requires* this kind-matching
228 -- to instantiate template type variables, but it seems like the right
229 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
230
231 --------------
232 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
233 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
234
235 --------------
236 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
237            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
238 match_list _  subst []         []         = Just subst
239 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
240                                                 ; match_list fn subst' tys1 tys2 }
241 match_list _  _     _          _          = Nothing
242
243 --------------
244 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
245 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
246   | c1 == c2 = match_tys menv subst tys1 tys2
247 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
248   | n1 == n2 = match menv subst t1 t2
249 match_pred _    _     _ _ = Nothing
250 \end{code}
251
252
253 %************************************************************************
254 %*                                                                      *
255                 GADTs
256 %*                                                                      *
257 %************************************************************************
258
259 Note [Pruning dead case alternatives]
260 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
261 Consider        data T a where
262                    T1 :: T Int
263                    T2 :: T a
264
265                 newtype X = MkX Int
266                 newtype Y = MkY Char
267
268                 type family F a
269                 type instance F Bool = Int
270
271 Now consider    case x of { T1 -> e1; T2 -> e2 }
272
273 The question before the house is this: if I know something about the type
274 of x, can I prune away the T1 alternative?
275
276 Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
277         Answer = YES (clearly)
278
279 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
280 to 'Bool', in which case x::T Int, so
281         ANSWER = NO (clearly)
282
283 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom) 
284 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
285 gives a coercion
286         CoX :: X ~ Int
287 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
288 of type (T X) constructed with T1.  Hence
289         ANSWER = NO (surprisingly)
290
291 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
292 mechanism uses a cast, just as above, to move from one dictionary to another,
293 in effect giving the programmer access to CoX.
294
295 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
296 non-bottom value of type (T Y) using T1.  That's because we can get
297 from Y to Char, but not to Int.
298
299
300 Here's a related question.      data Eq a b where EQ :: Eq a a
301 Consider
302         case x of { EQ -> ... }
303
304 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
305
306 What about x::Eq Int a, in a context where we have evidence that a~Char.
307 Then again the alternative is dead.   
308
309
310                         Summary
311
312 We are really doing a test for unsatisfiability of the type
313 constraints implied by the match. And that is clearly, in general, a
314 hard thing to do.  
315
316 However, since we are simply dropping dead code, a conservative test
317 suffices.  There is a continuum of tests, ranging from easy to hard, that
318 drop more and more dead code.
319
320 For now we implement a very simple test: type variables match
321 anything, type functions (incl newtypes) match anything, and only
322 distinct data types fail to match.  We can elaborate later.
323
324 \begin{code}
325 dataConCannotMatch :: [Type] -> DataCon -> Bool
326 -- Returns True iff the data con *definitely cannot* match a 
327 --                  scrutinee of type (T tys)
328 --                  where T is the type constructor for the data con
329 --
330 dataConCannotMatch tys con
331   | null eq_spec      = False   -- Common
332   | all isTyVarTy tys = False   -- Also common
333   | otherwise
334   = cant_match_s (map (substTyVar subst . fst) eq_spec)
335                  (map snd eq_spec)
336   where
337     dc_tvs  = dataConUnivTyVars con
338     eq_spec = dataConEqSpec con
339     subst   = zipTopTvSubst dc_tvs tys
340
341     cant_match_s :: [Type] -> [Type] -> Bool
342     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
343                              or (zipWith cant_match tys1 tys2)
344
345     cant_match :: Type -> Type -> Bool
346     cant_match t1 t2
347         | Just t1' <- coreView t1 = cant_match t1' t2
348         | Just t2' <- coreView t2 = cant_match t1 t2'
349
350     cant_match (FunTy a1 r1) (FunTy a2 r2)
351         = cant_match a1 a2 || cant_match r1 r2
352
353     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
354         | isDataTyCon tc1 && isDataTyCon tc2
355         = tc1 /= tc2 || cant_match_s tys1 tys2
356
357     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
358     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
359         -- tc can't be FunTyCon by invariant
360
361     cant_match (AppTy f1 a1) ty2
362         | Just (f2, a2) <- repSplitAppTy_maybe ty2
363         = cant_match f1 f2 || cant_match a1 a2
364     cant_match ty1 (AppTy f2 a2)
365         | Just (f1, a1) <- repSplitAppTy_maybe ty1
366         = cant_match f1 f2 || cant_match a1 a2
367
368     cant_match _ _ = False      -- Safe!
369
370 -- Things we could add;
371 --      foralls
372 --      look through newtypes
373 --      take account of tyvar bindings (EQ example above)
374 \end{code}
375
376
377 %************************************************************************
378 %*                                                                      *
379                 What a refinement is
380 %*                                                                      *
381 %************************************************************************
382
383 \begin{code}
384 data Refinement = Reft InScopeSet InternalReft 
385
386 type InternalReft = TyVarEnv (Coercion, Type)
387 -- INVARIANT:   a->(co,ty)   then   co :: (a~ty)
388 -- Not necessarily idemopotent
389
390 instance Outputable Refinement where
391   ppr (Reft _in_scope env)
392     = ptext (sLit "Refinement") <+>
393         braces (ppr env)
394
395 emptyRefinement :: Refinement
396 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
397
398 isEmptyRefinement :: Refinement -> Bool
399 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
400
401 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
402 -- Apply the refinement to the type.
403 -- If (refineType r ty) = (co, ty')
404 -- Then co :: ty~ty'
405 -- Nothing => the refinement does nothing to this type
406 refineType (Reft in_scope env) ty
407   | not (isEmptyVarEnv env),            -- Common case
408     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
409   = Just (substTy co_subst ty, substTy tv_subst ty)
410   | otherwise
411   = Nothing     -- The type doesn't mention any refined type variables
412   where
413     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
414     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
415  
416 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
417 refinePred (Reft in_scope env) pred
418   | not (isEmptyVarEnv env),            -- Common case
419     any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
420   = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
421   | otherwise
422   = Nothing     -- The type doesn't mention any refined type variables
423   where
424     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
425     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
426  
427 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
428 -- Like refineType, but returns the 'sym' coercion
429 -- If (refineResType r ty) = (co, ty')
430 -- Then co :: ty'~ty
431 refineResType reft ty
432   = case refineType reft ty of
433       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
434       Nothing        -> Nothing
435 \end{code}
436
437
438 %************************************************************************
439 %*                                                                      *
440                 Simple generation of a type refinement
441 %*                                                                      *
442 %************************************************************************
443
444 \begin{code}
445 matchRefine :: [TyVar] -> [Coercion] -> Refinement
446 \end{code}
447
448 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
449 is a specialisation of ty1, produce a type refinement that maps the variables
450 of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
451
452   matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
453     = { right (left (right co)) :: a ~ c
454       , right (right co)        :: b ~ Maybe d
455       }
456
457 Precondition: The rhs types must indeed be a specialisation of the lhs types;
458   i.e., some free variables of the lhs are replaced with either distinct free 
459   variables or proper type terms to obtain the rhs.  (We don't perform full
460   unification or type matching here!)
461
462 NB: matchRefine does *not* expand the type synonyms.
463
464 \begin{code}
465 matchRefine in_scope_tvs cos 
466   = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
467   where
468     in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
469         -- NB: in_scope_tvs include both coercion variables
470         --     *and* the tyvars in their kinds
471
472     refineOne co = refine co ty1 ty2
473       where
474         (ty1, ty2) = coercionKind co
475
476     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
477     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
478     refine _  (PredTy _) (PredTy _)               = 
479       error "Unify.matchRefine: PredTy"
480     refine co (FunTy arg res) (FunTy arg' res')   =
481       refine (mkRightCoercion (mkLeftCoercion co)) arg arg' 
482       `plusVarEnv` 
483       refine (mkRightCoercion co) res res'
484     refine co (AppTy fun arg) (AppTy fun' arg')   = 
485       refine (mkLeftCoercion co) fun fun' 
486       `plusVarEnv`
487       refine (mkRightCoercion co) arg arg'
488     refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
489       refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
490     refine _ _ _ = error "RcGadt.matchRefine: mismatch"
491
492     refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
493     refineArgs co tys tys' = 
494       fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
495       where
496         refineArg (ty, ty') (reft, coWrapper) 
497           = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, 
498              mkLeftCoercion . coWrapper)
499 \end{code}
500
501
502 %************************************************************************
503 %*                                                                      *
504                 Unification
505 %*                                                                      *
506 %************************************************************************
507
508 \begin{code}
509 tcUnifyTys :: (TyVar -> BindFlag)
510            -> [Type] -> [Type]
511            -> Maybe TvSubst     -- A regular one-shot substitution
512 -- The two types may have common type variables, and indeed do so in the
513 -- second call to tcUnifyTys in FunDeps.checkClsFD
514 --
515 tcUnifyTys bind_fn tys1 tys2
516   = maybeErrToMaybe $ initUM bind_fn $
517     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
518
519         -- Find the fixed point of the resulting non-idempotent substitution
520         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
521               tv_env   = fixTvSubstEnv in_scope subst
522
523         ; return (mkTvSubst in_scope tv_env) }
524   where
525     tvs1 = tyVarsOfTypes tys1
526     tvs2 = tyVarsOfTypes tys2
527
528 ----------------------------
529 -- XXX Can we do this more nicely, by exploiting laziness?
530 -- Or avoid needing it in the first place?
531 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
532 fixTvSubstEnv in_scope env = f env
533   where
534     f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
535           in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
536              then e
537              else f e'
538
539 \end{code}
540
541
542 %************************************************************************
543 %*                                                                      *
544                 The workhorse
545 %*                                                                      *
546 %************************************************************************
547
548 \begin{code}
549 unify :: TvSubstEnv     -- An existing substitution to extend
550       -> Type -> Type   -- Types to be unified, and witness of their equality
551       -> UM TvSubstEnv          -- Just the extended substitution, 
552                                 -- Nothing if unification failed
553 -- We do not require the incoming substitution to be idempotent,
554 -- nor guarantee that the outgoing one is.  That's fixed up by
555 -- the wrappers.
556
557 -- Respects newtypes, PredTypes
558
559 -- in unify, any NewTcApps/Preds should be taken at face value
560 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
561 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
562
563 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
564 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
565
566 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
567
568 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) 
569   | tyc1 == tyc2 = unify_tys subst tys1 tys2
570
571 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
572   = do  { subst' <- unify subst ty1a ty2a
573         ; unify subst' ty1b ty2b }
574
575         -- Applications need a bit of care!
576         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
577         -- NB: we've already dealt with type variables and Notes,
578         -- so if one type is an App the other one jolly well better be too
579 unify subst (AppTy ty1a ty1b) ty2
580   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
581   = do  { subst' <- unify subst ty1a ty2a
582         ; unify subst' ty1b ty2b }
583
584 unify subst ty1 (AppTy ty2a ty2b)
585   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
586   = do  { subst' <- unify subst ty1a ty2a
587         ; unify subst' ty1b ty2b }
588
589 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
590         -- ForAlls??
591
592 ------------------------------
593 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
594 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
595   | c1 == c2 = unify_tys subst tys1 tys2
596 unify_pred subst (IParam n1 t1) (IParam n2 t2)
597   | n1 == n2 = unify subst t1 t2
598 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
599  
600 ------------------------------
601 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
602 unify_tys subst xs ys = unifyList subst xs ys
603
604 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
605 unifyList subst orig_xs orig_ys
606   = go subst orig_xs orig_ys
607   where
608     go subst []     []     = return subst
609     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
610                                 ; go subst' xs ys }
611     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
612
613 ---------------------------------
614 uVar :: TvSubstEnv      -- An existing substitution to extend
615      -> TyVar           -- Type variable to be unified
616      -> Type            -- with this type
617      -> UM TvSubstEnv
618
619 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
620 --      if swap=False   (tv1~ty)
621 --      if swap=True    (ty~tv1)
622
623 uVar subst tv1 ty
624  = -- Check to see whether tv1 is refined by the substitution
625    case (lookupVarEnv subst tv1) of
626      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
627      Nothing  -> uUnrefined subst       -- No, continue
628                             tv1 ty ty
629
630 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
631            -> TyVar               -- Type variable to be unified
632            -> Type                -- with this type
633            -> Type                -- (version w/ expanded synonyms)
634            -> UM TvSubstEnv
635
636 -- We know that tv1 isn't refined
637
638 uUnrefined subst tv1 ty2 ty2'
639   | Just ty2'' <- tcView ty2'
640   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
641                 -- This is essential, in case we have
642                 --      type Foo a = a
643                 -- and then unify a ~ Foo a
644
645 uUnrefined subst tv1 ty2 (TyVarTy tv2)
646   | tv1 == tv2          -- Same type variable
647   = return subst
648
649     -- Check to see whether tv2 is refined
650   | Just ty' <- lookupVarEnv subst tv2
651   = uUnrefined subst tv1 ty' ty'
652
653   -- So both are unrefined; next, see if the kinds force the direction
654   | eqKind k1 k2        -- Can update either; so check the bind-flags
655   = do  { b1 <- tvBindFlag tv1
656         ; b2 <- tvBindFlag tv2
657         ; case (b1,b2) of
658             (BindMe, _)          -> bind tv1 ty2
659             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
660             (Skolem, _)          -> bind tv2 ty1
661         }
662
663   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
664   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
665
666   | otherwise = failWith (kindMisMatch tv1 ty2)
667   where
668     ty1 = TyVarTy tv1
669     k1 = tyVarKind tv1
670     k2 = tyVarKind tv2
671     bind tv ty = return $ extendVarEnv subst tv ty
672
673 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
674   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
675   = failWith (occursCheck tv1 ty2)      -- Occurs check
676   | not (k2 `isSubKind` k1)
677   = failWith (kindMisMatch tv1 ty2)     -- Kind check
678   | otherwise
679   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
680   where
681     k1 = tyVarKind tv1
682     k2 = typeKind ty2'
683
684 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
685 -- Apply the non-idempotent substitution to a set of type variables,
686 -- remembering that the substitution isn't necessarily idempotent
687 substTvSet subst tvs
688   = foldVarSet (unionVarSet . get) emptyVarSet tvs
689   where
690     get tv = case lookupVarEnv subst tv of
691                Nothing -> unitVarSet tv
692                Just ty -> substTvSet subst (tyVarsOfType ty)
693
694 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
695 bindTv subst tv ty      -- ty is not a type variable
696   = do  { b <- tvBindFlag tv
697         ; case b of
698             Skolem -> failWith (misMatch (TyVarTy tv) ty)
699             BindMe -> return $ extendVarEnv subst tv ty
700         }
701 \end{code}
702
703 %************************************************************************
704 %*                                                                      *
705                 Binding decisions
706 %*                                                                      *
707 %************************************************************************
708
709 \begin{code}
710 data BindFlag 
711   = BindMe      -- A regular type variable
712
713   | Skolem      -- This type variable is a skolem constant
714                 -- Don't bind it; it only matches itself
715 \end{code}
716
717
718 %************************************************************************
719 %*                                                                      *
720                 Unification monad
721 %*                                                                      *
722 %************************************************************************
723
724 \begin{code}
725 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
726                          -> MaybeErr Message a }
727
728 instance Monad UM where
729   return a = UM (\_tvs -> Succeeded a)
730   fail s   = UM (\_tvs -> Failed (text s))
731   m >>= k  = UM (\tvs -> case unUM m tvs of
732                            Failed err -> Failed err
733                            Succeeded v  -> unUM (k v) tvs)
734
735 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
736 initUM badtvs um = unUM um badtvs
737
738 tvBindFlag :: TyVar -> UM BindFlag
739 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
740
741 failWith :: Message -> UM a
742 failWith msg = UM (\_tv_fn -> Failed msg)
743
744 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
745 maybeErrToMaybe (Succeeded a) = Just a
746 maybeErrToMaybe (Failed _)    = Nothing
747 \end{code}
748
749
750 %************************************************************************
751 %*                                                                      *
752                 Error reporting
753         We go to a lot more trouble to tidy the types
754         in TcUnify.  Maybe we'll end up having to do that
755         here too, but I'll leave it for now.
756 %*                                                                      *
757 %************************************************************************
758
759 \begin{code}
760 misMatch :: Type -> Type -> SDoc
761 misMatch t1 t2
762   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> 
763     ptext (sLit "and") <+> quotes (ppr t2)
764
765 lengthMisMatch :: [Type] -> [Type] -> SDoc
766 lengthMisMatch tys1 tys2
767   = sep [ptext (sLit "Can't match unequal length lists"), 
768          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
769
770 kindMisMatch :: TyVar -> Type -> SDoc
771 kindMisMatch tv1 t2
772   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
773             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
774           ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
775                 ptext (sLit "with") <+> quotes (ppr t2)]
776
777 occursCheck :: TyVar -> Type -> SDoc
778 occursCheck tv ty
779   = hang (ptext (sLit "Can't construct the infinite type"))
780        2 (ppr tv <+> equals <+> ppr ty)
781 \end{code}