Implememt -fdefer-type-errors (Trac #5624)
[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    ) where
29
30 #include "HsVersions.h"
31
32 import Var
33 import VarEnv
34 import VarSet
35 import Kind
36 import Type
37 import TyCon
38 import TypeRep
39 import Outputable
40 import ErrUtils
41 import Util
42 import Maybes
43 import FastString
44 \end{code}
45
46
47 %************************************************************************
48 %*                                                                      *
49                 Matching
50 %*                                                                      *
51 %************************************************************************
52
53
54 Matching is much tricker than you might think.
55
56 1. The substitution we generate binds the *template type variables*
57    which are given to us explicitly.
58
59 2. We want to match in the presence of foralls; 
60         e.g     (forall a. t1) ~ (forall b. t2)
61
62    That is what the RnEnv2 is for; it does the alpha-renaming
63    that makes it as if a and b were the same variable.
64    Initialising the RnEnv2, so that it can generate a fresh
65    binder when necessary, entails knowing the free variables of
66    both types.
67
68 3. We must be careful not to bind a template type variable to a
69    locally bound variable.  E.g.
70         (forall a. x) ~ (forall b. b)
71    where x is the template type variable.  Then we do not want to
72    bind x to a/b!  This is a kind of occurs check.
73    The necessary locals accumulate in the RnEnv2.
74
75
76 \begin{code}
77 data MatchEnv
78   = ME  { me_tmpls :: VarSet    -- Template variables
79         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
80         }                       --   In-scope set includes template variables
81     -- Nota Bene: MatchEnv isn't specific to Types.  It is used
82     --            for matching terms and coercions as well as types
83
84 tcMatchTy :: TyVarSet           -- Template tyvars
85           -> Type               -- Template
86           -> Type               -- Target
87           -> Maybe TvSubst      -- One-shot; in principle the template
88                                 -- variables could be free in the target
89
90 tcMatchTy tmpls ty1 ty2
91   = case match menv emptyTvSubstEnv ty1 ty2 of
92         Just subst_env -> Just (TvSubst in_scope subst_env)
93         Nothing        -> Nothing
94   where
95     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
96     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
97         -- We're assuming that all the interesting 
98         -- tyvars in tys1 are in tmpls
99
100 tcMatchTys :: TyVarSet          -- Template tyvars
101            -> [Type]            -- Template
102            -> [Type]            -- Target
103            -> Maybe TvSubst     -- One-shot; in principle the template
104                                 -- variables could be free in the target
105
106 tcMatchTys tmpls tys1 tys2
107   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
108         Just subst_env -> Just (TvSubst in_scope subst_env)
109         Nothing        -> Nothing
110   where
111     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
112     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
113         -- We're assuming that all the interesting 
114         -- tyvars in tys1 are in tmpls
115
116 -- This is similar, but extends a substitution
117 tcMatchTyX :: TyVarSet          -- Template tyvars
118            -> TvSubst           -- Substitution to extend
119            -> Type              -- Template
120            -> Type              -- Target
121            -> Maybe TvSubst
122 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
123   = case match menv subst_env ty1 ty2 of
124         Just subst_env -> Just (TvSubst in_scope subst_env)
125         Nothing        -> Nothing
126   where
127     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
128
129 tcMatchPreds
130         :: [TyVar]                      -- Bind these
131         -> [PredType] -> [PredType]
132         -> Maybe TvSubstEnv
133 tcMatchPreds tmpls ps1 ps2
134   = matchList (match menv) emptyTvSubstEnv ps1 ps2
135   where
136     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
137     in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2)
138
139 -- This one is called from the expression matcher, which already has a MatchEnv in hand
140 ruleMatchTyX :: MatchEnv 
141          -> TvSubstEnv          -- Substitution to extend
142          -> Type                -- Template
143          -> Type                -- Target
144          -> Maybe TvSubstEnv
145
146 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
147 \end{code}
148
149 Now the internals of matching
150
151 \begin{code}
152 match :: MatchEnv       -- For the most part this is pushed downwards
153       -> TvSubstEnv     -- Substitution so far:
154                         --   Domain is subset of template tyvars
155                         --   Free vars of range is subset of 
156                         --      in-scope set of the RnEnv2
157       -> Type -> Type   -- Template and target respectively
158       -> Maybe TvSubstEnv
159 -- This matcher works on core types; that is, it ignores PredTypes
160 -- Watch out if newtypes become transparent agin!
161 --      this matcher must respect newtypes
162
163 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
164                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
165
166 match menv subst (TyVarTy tv1) ty2
167   | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
168   = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
169         -- ty1 has no locally-bound variables, hence nukeRnEnvL
170     then Just subst
171     else Nothing        -- ty2 doesn't match
172
173   | tv1' `elemVarSet` me_tmpls menv
174   = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
175     then Nothing        -- Occurs check
176     else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
177                         -- Note [Matching kinds]
178             ; return (extendVarEnv subst1 tv1' ty2) }
179
180    | otherwise  -- tv1 is not a template tyvar
181    = case ty2 of
182         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
183         _                                       -> Nothing
184   where
185     rn_env = me_env menv
186     tv1' = rnOccL rn_env tv1
187
188 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
189   = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2)
190        ; match menv' subst' ty1 ty2 }
191   where         -- Use the magic of rnBndr2 to go under the binders
192     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
193
194 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
195   | tc1 == tc2 = match_tys menv subst tys1 tys2
196 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
197   = do { subst' <- match menv subst ty1a ty2a
198        ; match menv subst' ty1b ty2b }
199 match menv subst (AppTy ty1a ty1b) ty2
200   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
201         -- 'repSplit' used because the tcView stuff is done above
202   = do { subst' <- match menv subst ty1a ty2a
203        ; match menv subst' ty1b ty2b }
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 _ _ = False      -- Safe!
346
347 -- Things we could add;
348 --      foralls
349 --      look through newtypes
350 --      take account of tyvar bindings (EQ example above)
351 \end{code}
352
353
354 %************************************************************************
355 %*                                                                      *
356              Unification
357 %*                                                                      *
358 %************************************************************************
359
360 \begin{code}
361 tcUnifyTys :: (TyVar -> BindFlag)
362            -> [Type] -> [Type]
363            -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
364 -- The two types may have common type variables, and indeed do so in the
365 -- second call to tcUnifyTys in FunDeps.checkClsFD
366 --
367 tcUnifyTys bind_fn tys1 tys2
368   = maybeErrToMaybe $ initUM bind_fn $
369     do { subst <- unifyList emptyTvSubstEnv tys1 tys2
370
371         -- Find the fixed point of the resulting non-idempotent substitution
372         ; return (niFixTvSubst subst) }
373 \end{code}
374
375
376 %************************************************************************
377 %*                                                                      *
378                 Non-idempotent substitution
379 %*                                                                      *
380 %************************************************************************
381
382 Note [Non-idempotent substitution]
383 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
384 During unification we use a TvSubstEnv that is
385   (a) non-idempotent
386   (b) loop-free; ie repeatedly applying it yields a fixed point
387
388 \begin{code}
389 niFixTvSubst :: TvSubstEnv -> TvSubst
390 -- Find the idempotent fixed point of the non-idempotent substitution
391 -- ToDo: use laziness instead of iteration?
392 niFixTvSubst env = f env
393   where
394     f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
395         | otherwise    = subst
396         where
397           range_tvs    = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
398           subst        = mkTvSubst (mkInScopeSet range_tvs) e 
399           not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
400           in_domain tv = tv `elemVarEnv` e
401
402 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
403 -- Apply the non-idempotent substitution to a set of type variables,
404 -- remembering that the substitution isn't necessarily idempotent
405 -- This is used in the occurs check, before extending the substitution
406 niSubstTvSet subst tvs
407   = foldVarSet (unionVarSet . get) emptyVarSet tvs
408   where
409     get tv = case lookupVarEnv subst tv of
410                Nothing -> unitVarSet tv
411                Just ty -> niSubstTvSet subst (tyVarsOfType ty)
412 \end{code}
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 (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) 
439   | tyc1 == tyc2 = unify_tys subst tys1 tys2
440
441 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
442   = do  { subst' <- unify subst ty1a ty2a
443         ; unify subst' ty1b ty2b }
444
445         -- Applications need a bit of care!
446         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
447         -- NB: we've already dealt with type variables and Notes,
448         -- so if one type is an App the other one jolly well better be too
449 unify subst (AppTy ty1a ty1b) ty2
450   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
451   = do  { subst' <- unify subst ty1a ty2a
452         ; unify subst' ty1b ty2b }
453
454 unify subst ty1 (AppTy ty2a ty2b)
455   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
456   = do  { subst' <- unify subst ty1a ty2a
457         ; unify subst' ty1b ty2b }
458
459 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
460         -- ForAlls??
461
462 ------------------------------
463 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
464 unify_tys subst xs ys = unifyList subst xs ys
465
466 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
467 unifyList subst orig_xs orig_ys
468   = go subst orig_xs orig_ys
469   where
470     go subst []     []     = return subst
471     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
472                                 ; go subst' xs ys }
473     go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
474
475 ---------------------------------
476 uVar :: TvSubstEnv      -- An existing substitution to extend
477      -> TyVar           -- Type variable to be unified
478      -> Type            -- with this type
479      -> UM TvSubstEnv
480
481 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
482 --      if swap=False   (tv1~ty)
483 --      if swap=True    (ty~tv1)
484
485 uVar subst tv1 ty
486  = -- Check to see whether tv1 is refined by the substitution
487    case (lookupVarEnv subst tv1) of
488      Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
489      Nothing  -> uUnrefined subst       -- No, continue
490                             tv1 ty ty
491
492 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
493            -> TyVar               -- Type variable to be unified
494            -> Type                -- with this type
495            -> Type                -- (version w/ expanded synonyms)
496            -> UM TvSubstEnv
497
498 -- We know that tv1 isn't refined
499
500 uUnrefined subst tv1 ty2 ty2'
501   | Just ty2'' <- tcView ty2'
502   = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
503                 -- This is essential, in case we have
504                 --      type Foo a = a
505                 -- and then unify a ~ Foo a
506
507 uUnrefined subst tv1 ty2 (TyVarTy tv2)
508   | tv1 == tv2          -- Same type variable
509   = return subst
510
511     -- Check to see whether tv2 is refined
512   | Just ty' <- lookupVarEnv subst tv2
513   = uUnrefined subst tv1 ty' ty'
514
515   | otherwise
516   -- So both are unrefined; next, see if the kinds force the direction
517   = case (k1_sub_k2, k2_sub_k1) of
518         (True,  True)  -> choose subst
519         (True,  False) -> bindTv subst tv2 ty1
520         (False, True)  -> bindTv subst tv1 ty2
521         (False, False) -> do
522             { subst' <- unify subst k1 k2
523             ; choose subst' }
524   where subst_kind = mkTvSubst (mkInScopeSet (tyVarsOfTypes [k1,k2])) subst
525         k1 = substTy subst_kind (tyVarKind tv1)
526         k2 = substTy subst_kind (tyVarKind tv2)
527         k1_sub_k2 = k1 `isSubKind` k2
528         k2_sub_k1 = k2 `isSubKind` k1
529         ty1 = TyVarTy tv1
530         bind subst tv ty = return $ extendVarEnv subst tv ty
531         choose subst = do
532              { b1 <- tvBindFlag tv1
533              ; b2 <- tvBindFlag tv2
534              ; case (b1, b2) of
535                  (BindMe, _)         -> bind subst tv1 ty2
536                  (Skolem, Skolem)    -> failWith (misMatch ty1 ty2)
537                  (Skolem, _)         -> bind subst tv2 ty1 }
538
539 uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
540   | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
541   = failWith (occursCheck tv1 ty2)      -- Occurs check
542   | not (k2 `isSubKind` k1)
543   = failWith (kindMisMatch tv1 ty2)     -- Kind check
544   | otherwise
545   = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
546   where
547     k1 = tyVarKind tv1
548     k2 = typeKind ty2'
549
550 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
551 bindTv subst tv ty      -- ty is not a type variable
552   = do  { b <- tvBindFlag tv
553         ; case b of
554             Skolem -> failWith (misMatch (TyVarTy tv) ty)
555             BindMe -> return $ extendVarEnv subst tv ty
556         }
557 \end{code}
558
559 %************************************************************************
560 %*                                                                      *
561                 Binding decisions
562 %*                                                                      *
563 %************************************************************************
564
565 \begin{code}
566 data BindFlag 
567   = BindMe      -- A regular type variable
568
569   | Skolem      -- This type variable is a skolem constant
570                 -- Don't bind it; it only matches itself
571 \end{code}
572
573
574 %************************************************************************
575 %*                                                                      *
576                 Unification monad
577 %*                                                                      *
578 %************************************************************************
579
580 \begin{code}
581 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
582                          -> MaybeErr MsgDoc a }
583
584 instance Monad UM where
585   return a = UM (\_tvs -> Succeeded a)
586   fail s   = UM (\_tvs -> Failed (text s))
587   m >>= k  = UM (\tvs -> case unUM m tvs of
588                            Failed err -> Failed err
589                            Succeeded v  -> unUM (k v) tvs)
590
591 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr MsgDoc a
592 initUM badtvs um = unUM um badtvs
593
594 tvBindFlag :: TyVar -> UM BindFlag
595 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
596
597 failWith :: MsgDoc -> UM a
598 failWith msg = UM (\_tv_fn -> Failed msg)
599
600 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
601 maybeErrToMaybe (Succeeded a) = Just a
602 maybeErrToMaybe (Failed _)    = Nothing
603 \end{code}
604
605
606 %************************************************************************
607 %*                                                                      *
608                 Error reporting
609         We go to a lot more trouble to tidy the types
610         in TcUnify.  Maybe we'll end up having to do that
611         here too, but I'll leave it for now.
612 %*                                                                      *
613 %************************************************************************
614
615 \begin{code}
616 misMatch :: Type -> Type -> SDoc
617 misMatch t1 t2
618   = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> 
619     ptext (sLit "and") <+> quotes (ppr t2)
620
621 lengthMisMatch :: [Type] -> [Type] -> SDoc
622 lengthMisMatch tys1 tys2
623   = sep [ptext (sLit "Can't match unequal length lists"), 
624          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
625
626 kindMisMatch :: TyVar -> Type -> SDoc
627 kindMisMatch tv1 t2
628   = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
629             ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
630           ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
631                 ptext (sLit "with") <+> quotes (ppr t2)]
632
633 occursCheck :: TyVar -> Type -> SDoc
634 occursCheck tv ty
635   = hang (ptext (sLit "Can't construct the infinite type"))
636        2 (ppr tv <+> equals <+> ppr ty)
637 \end{code}