Refactor the TyVarTy case of 'match'. No change in behaviour.
[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 :: [CoVar] -> 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 co_vars 
466   = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
467   where
468     in_scope = foldr extend emptyInScopeSet co_vars
469
470         -- For each co_var, add it *and* the tyvars it mentions, to in_scope
471     extend co_var in_scope
472       = extendInScopeSetSet in_scope $
473           extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
474
475     refineOne co_var = refine (TyVarTy co_var) ty1 ty2
476       where
477         (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
478
479     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
480     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
481     refine _  (PredTy _) (PredTy _)               = 
482       error "Unify.matchRefine: PredTy"
483     refine co (FunTy arg res) (FunTy arg' res')   =
484       refine (mkRightCoercion (mkLeftCoercion co)) arg arg' 
485       `plusVarEnv` 
486       refine (mkRightCoercion co) res res'
487     refine co (AppTy fun arg) (AppTy fun' arg')   = 
488       refine (mkLeftCoercion co) fun fun' 
489       `plusVarEnv`
490       refine (mkRightCoercion co) arg arg'
491     refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
492       refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
493     refine _ _ _ = error "RcGadt.matchRefine: mismatch"
494
495     refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
496     refineArgs co tys tys' = 
497       fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
498       where
499         refineArg (ty, ty') (reft, coWrapper) 
500           = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, 
501              mkLeftCoercion . coWrapper)
502 \end{code}
503
504
505 %************************************************************************
506 %*                                                                      *
507                 Unification
508 %*                                                                      *
509 %************************************************************************
510
511 \begin{code}
512 tcUnifyTys :: (TyVar -> BindFlag)
513            -> [Type] -> [Type]
514            -> Maybe TvSubst     -- A regular one-shot substitution
515 -- The two types may have common type variables, and indeed do so in the
516 -- second call to tcUnifyTys in FunDeps.checkClsFD
517 --
518 tcUnifyTys bind_fn tys1 tys2
519   = maybeErrToMaybe $ initUM bind_fn $
520     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
521
522         -- Find the fixed point of the resulting non-idempotent substitution
523         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
524               tv_env   = fixTvSubstEnv in_scope subst
525
526         ; return (mkTvSubst in_scope tv_env) }
527   where
528     tvs1 = tyVarsOfTypes tys1
529     tvs2 = tyVarsOfTypes tys2
530
531 ----------------------------
532 -- XXX Can we do this more nicely, by exploiting laziness?
533 -- Or avoid needing it in the first place?
534 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
535 fixTvSubstEnv in_scope env = f env
536   where
537     f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
538           in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
539              then e
540              else f e'
541
542 \end{code}
543
544
545 %************************************************************************
546 %*                                                                      *
547                 The workhorse
548 %*                                                                      *
549 %************************************************************************
550
551 \begin{code}
552 unify :: TvSubstEnv     -- An existing substitution to extend
553       -> Type -> Type   -- Types to be unified, and witness of their equality
554       -> UM TvSubstEnv          -- Just the extended substitution, 
555                                 -- Nothing if unification failed
556 -- We do not require the incoming substitution to be idempotent,
557 -- nor guarantee that the outgoing one is.  That's fixed up by
558 -- the wrappers.
559
560 -- Respects newtypes, PredTypes
561
562 -- in unify, any NewTcApps/Preds should be taken at face value
563 unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
564 unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
565
566 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
567 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
568
569 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
570
571 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) 
572   | tyc1 == tyc2 = unify_tys subst tys1 tys2
573
574 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
575   = do  { subst' <- unify subst ty1a ty2a
576         ; unify subst' ty1b ty2b }
577
578         -- Applications need a bit of care!
579         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
580         -- NB: we've already dealt with type variables and Notes,
581         -- so if one type is an App the other one jolly well better be too
582 unify subst (AppTy ty1a ty1b) ty2
583   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
584   = do  { subst' <- unify subst ty1a ty2a
585         ; unify subst' ty1b ty2b }
586
587 unify subst ty1 (AppTy ty2a ty2b)
588   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
589   = do  { subst' <- unify subst ty1a ty2a
590         ; unify subst' ty1b ty2b }
591
592 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
593         -- ForAlls??
594
595 ------------------------------
596 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
597 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
598   | c1 == c2 = unify_tys subst tys1 tys2
599 unify_pred subst (IParam n1 t1) (IParam n2 t2)
600   | n1 == n2 = unify subst t1 t2
601 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
602  
603 ------------------------------
604 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
605 unify_tys subst xs ys = unifyList subst xs ys
606
607 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
608 unifyList subst orig_xs orig_ys
609   = go subst orig_xs orig_ys
610   where
611     go subst []     []     = return subst
612     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
613                                 ; go subst' xs ys }
614     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
615
616 ---------------------------------
617 uVar :: TvSubstEnv      -- An existing substitution to extend
618      -> TyVar           -- Type variable to be unified
619      -> Type            -- with this type
620      -> UM TvSubstEnv
621
622 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
623 --      if swap=False   (tv1:=:ty)
624 --      if swap=True    (ty:=:tv1)
625
626 uVar subst tv1 ty
627  = -- Check to see whether tv1 is refined by the substitution
628    case (lookupVarEnv subst tv1) of
629      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
630      Nothing  -> uUnrefined subst       -- No, continue
631                             tv1 ty ty
632
633 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
634            -> TyVar               -- Type variable to be unified
635            -> Type                -- with this type
636            -> Type                -- (version w/ expanded synonyms)
637            -> UM TvSubstEnv
638
639 -- We know that tv1 isn't refined
640
641 uUnrefined subst tv1 ty2 ty2'
642   | Just ty2'' <- tcView ty2'
643   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
644                 -- This is essential, in case we have
645                 --      type Foo a = a
646                 -- and then unify a :=: Foo a
647
648 uUnrefined subst tv1 ty2 (TyVarTy tv2)
649   | tv1 == tv2          -- Same type variable
650   = return subst
651
652     -- Check to see whether tv2 is refined
653   | Just ty' <- lookupVarEnv subst tv2
654   = uUnrefined subst tv1 ty' ty'
655
656   -- So both are unrefined; next, see if the kinds force the direction
657   | eqKind k1 k2        -- Can update either; so check the bind-flags
658   = do  { b1 <- tvBindFlag tv1
659         ; b2 <- tvBindFlag tv2
660         ; case (b1,b2) of
661             (BindMe, _)          -> bind tv1 ty2
662
663             (AvoidMe, BindMe)    -> bind tv2 ty1
664             (AvoidMe, _)         -> bind tv1 ty2
665
666             (WildCard, WildCard) -> return subst
667             (WildCard, Skolem)   -> return subst
668             (WildCard, _)        -> bind tv2 ty1
669
670             (Skolem, WildCard)   -> return subst
671             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
672             (Skolem, _)          -> bind tv2 ty1
673         }
674
675   | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
676   | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
677
678   | otherwise = failWith (kindMisMatch tv1 ty2)
679   where
680     ty1 = TyVarTy tv1
681     k1 = tyVarKind tv1
682     k2 = tyVarKind tv2
683     bind tv ty = return $ extendVarEnv subst tv ty
684
685 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
686   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
687   = failWith (occursCheck tv1 ty2)      -- Occurs check
688   | not (k2 `isSubKind` k1)
689   = failWith (kindMisMatch tv1 ty2)     -- Kind check
690   | otherwise
691   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
692   where
693     k1 = tyVarKind tv1
694     k2 = typeKind ty2'
695
696 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
697 -- Apply the non-idempotent substitution to a set of type variables,
698 -- remembering that the substitution isn't necessarily idempotent
699 substTvSet subst tvs
700   = foldVarSet (unionVarSet . get) emptyVarSet tvs
701   where
702     get tv = case lookupVarEnv subst tv of
703                Nothing -> unitVarSet tv
704                Just ty -> substTvSet subst (tyVarsOfType ty)
705
706 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
707 bindTv subst tv ty      -- ty is not a type variable
708   = do  { b <- tvBindFlag tv
709         ; case b of
710             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
711             WildCard -> return subst
712             _other   -> return $ extendVarEnv subst tv ty
713         }
714 \end{code}
715
716 %************************************************************************
717 %*                                                                      *
718                 Unification monad
719 %*                                                                      *
720 %************************************************************************
721
722 \begin{code}
723 data BindFlag 
724   = BindMe      -- A regular type variable
725   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
726
727   | Skolem      -- This type variable is a skolem constant
728                 -- Don't bind it; it only matches itself
729
730   | WildCard    -- This type variable matches anything,
731                 -- and does not affect the substitution
732
733 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
734                          -> MaybeErr Message a }
735
736 instance Monad UM where
737   return a = UM (\_tvs -> Succeeded a)
738   fail s   = UM (\_tvs -> Failed (text s))
739   m >>= k  = UM (\tvs -> case unUM m tvs of
740                            Failed err -> Failed err
741                            Succeeded v  -> unUM (k v) tvs)
742
743 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
744 initUM badtvs um = unUM um badtvs
745
746 tvBindFlag :: TyVar -> UM BindFlag
747 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
748
749 failWith :: Message -> UM a
750 failWith msg = UM (\_tv_fn -> Failed msg)
751
752 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
753 maybeErrToMaybe (Succeeded a) = Just a
754 maybeErrToMaybe (Failed _)    = Nothing
755 \end{code}
756
757
758 %************************************************************************
759 %*                                                                      *
760                 Error reporting
761         We go to a lot more trouble to tidy the types
762         in TcUnify.  Maybe we'll end up having to do that
763         here too, but I'll leave it for now.
764 %*                                                                      *
765 %************************************************************************
766
767 \begin{code}
768 misMatch :: Type -> Type -> SDoc
769 misMatch t1 t2
770   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
771     ptext SLIT("and") <+> quotes (ppr t2)
772
773 lengthMisMatch :: [Type] -> [Type] -> SDoc
774 lengthMisMatch tys1 tys2
775   = sep [ptext SLIT("Can't match unequal length lists"), 
776          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
777
778 kindMisMatch :: TyVar -> Type -> SDoc
779 kindMisMatch tv1 t2
780   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
781             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
782           ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
783                 ptext SLIT("with") <+> quotes (ppr t2)]
784
785 occursCheck :: TyVar -> Type -> SDoc
786 occursCheck tv ty
787   = hang (ptext SLIT("Can't construct the infinite type"))
788        2 (ppr tv <+> equals <+> ppr ty)
789 \end{code}