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