2 % (c) The University of Glasgow 2006
8 -- the "tc" prefix indicates that matching always
9 -- respects newtypes (rather than looking through them)
10 tcMatchTy, tcMatchTys, tcMatchTyX,
11 ruleMatchTyX, tcMatchPreds, MatchEnv(..),
15 -- GADT type refinement
16 Refinement, emptyRefinement, isEmptyRefinement,
17 matchRefine, refineType, refinePred, refineResType,
19 -- Side-effect free unification
20 tcUnifyTys, BindFlag(..)
24 #include "HsVersions.h"
43 %************************************************************************
47 %************************************************************************
50 Matching is much tricker than you might think.
52 1. The substitution we generate binds the *template type variables*
53 which are given to us explicitly.
55 2. We want to match in the presence of foralls;
56 e.g (forall a. t1) ~ (forall b. t2)
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
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.
74 = ME { me_tmpls :: VarSet -- Template tyvars
75 , me_env :: RnEnv2 -- Renaming envt for nested foralls
76 } -- In-scope set includes template tyvars
78 tcMatchTy :: TyVarSet -- Template tyvars
81 -> Maybe TvSubst -- One-shot; in principle the template
82 -- variables could be free in the target
84 tcMatchTy tmpls ty1 ty2
85 = case match menv emptyTvSubstEnv ty1 ty2 of
86 Just subst_env -> Just (TvSubst in_scope subst_env)
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
94 tcMatchTys :: TyVarSet -- Template tyvars
97 -> Maybe TvSubst -- One-shot; in principle the template
98 -- variables could be free in the target
100 tcMatchTys tmpls tys1 tys2
101 = case match_tys menv emptyTvSubstEnv tys1 tys2 of
102 Just subst_env -> Just (TvSubst in_scope subst_env)
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
110 -- This is similar, but extends a substitution
111 tcMatchTyX :: TyVarSet -- Template tyvars
112 -> TvSubst -- Substitution to extend
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)
121 menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
124 :: [TyVar] -- Bind these
125 -> [PredType] -> [PredType]
127 tcMatchPreds tmpls ps1 ps2
128 = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
130 menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
131 in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
133 -- This one is called from the expression matcher, which already has a MatchEnv in hand
134 ruleMatchTyX :: MatchEnv
135 -> TvSubstEnv -- Substitution to extend
140 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
143 Now the internals of matching
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
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
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'
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
166 else Nothing -- ty2 doesn't match
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) }
175 | otherwise -- tv1 is not a template tyvar
177 TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
181 tv1' = rnOccL rn_env tv1
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 }
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 }
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) = coVarKind 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
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.
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.
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
232 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
233 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
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
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
253 %************************************************************************
257 %************************************************************************
259 Note [Pruning dead case alternatives]
260 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
261 Consider data T a where
269 type instance F Bool = Int
271 Now consider case x of { T1 -> e1; T2 -> e2 }
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?
276 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
277 Answer = YES (clearly)
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)
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
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)
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.
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.
300 Here's a related question. data Eq a b where EQ :: Eq a a
302 case x of { EQ -> ... }
304 Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
306 What about x::Eq Int a, in a context where we have evidence that a~Char.
307 Then again the alternative is dead.
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
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.
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.
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
330 dataConCannotMatch tys con
331 | null eq_spec = False -- Common
332 | all isTyVarTy tys = False -- Also common
334 = cant_match_s (map (substTyVar subst . fst) eq_spec)
337 dc_tvs = dataConUnivTyVars con
338 eq_spec = dataConEqSpec con
339 subst = zipTopTvSubst dc_tvs tys
341 cant_match_s :: [Type] -> [Type] -> Bool
342 cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
343 or (zipWith cant_match tys1 tys2)
345 cant_match :: Type -> Type -> Bool
347 | Just t1' <- coreView t1 = cant_match t1' t2
348 | Just t2' <- coreView t2 = cant_match t1 t2'
350 cant_match (FunTy a1 r1) (FunTy a2 r2)
351 = cant_match a1 a2 || cant_match r1 r2
353 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
354 | isDataTyCon tc1 && isDataTyCon tc2
355 = tc1 /= tc2 || cant_match_s tys1 tys2
357 cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
358 cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
359 -- tc can't be FunTyCon by invariant
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
368 cant_match _ _ = False -- Safe!
370 -- Things we could add;
372 -- look through newtypes
373 -- take account of tyvar bindings (EQ example above)
377 %************************************************************************
381 %************************************************************************
384 data Refinement = Reft InScopeSet InternalReft
386 type InternalReft = TyVarEnv (Coercion, Type)
387 -- INVARIANT: a->(co,ty) then co :: (a~ty)
388 -- Not necessarily idemopotent
390 instance Outputable Refinement where
391 ppr (Reft _in_scope env)
392 = ptext (sLit "Refinement") <+>
395 emptyRefinement :: Refinement
396 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
398 isEmptyRefinement :: Refinement -> Bool
399 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
401 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
402 -- Apply the refinement to the type.
403 -- If (refineType r ty) = (co, 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)
411 = Nothing -- The type doesn't mention any refined type variables
413 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
414 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
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)
422 = Nothing -- The type doesn't mention any refined type variables
424 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
425 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
427 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
428 -- Like refineType, but returns the 'sym' coercion
429 -- If (refineResType r ty) = (co, ty')
431 refineResType reft ty
432 = case refineType reft ty of
433 Just (co, ty1) -> Just (mkSymCoercion co, ty1)
438 %************************************************************************
440 Simple generation of a type refinement
442 %************************************************************************
445 matchRefine :: [TyVar] -> [Coercion] -> Refinement
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,
452 matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
453 = { right (left (right co)) :: a ~ c
454 , right (right co) :: b ~ Maybe d
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!)
462 NB: matchRefine does *not* expand the type synonyms.
465 matchRefine in_scope_tvs cos
466 = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
468 in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
469 -- NB: in_scope_tvs include both coercion variables
470 -- *and* the tyvars in their kinds
472 refineOne co = refine co ty1 ty2
474 (ty1, ty2) = coercionKind co
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'
483 refine (mkRightCoercion co) res res'
484 refine co (AppTy fun arg) (AppTy fun' arg') =
485 refine (mkLeftCoercion co) fun fun'
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"
492 refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
493 refineArgs co tys tys' =
494 fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
496 refineArg (ty, ty') (reft, coWrapper)
497 = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
498 mkLeftCoercion . coWrapper)
502 %************************************************************************
506 %************************************************************************
509 tcUnifyTys :: (TyVar -> BindFlag)
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
515 tcUnifyTys bind_fn tys1 tys2
516 = maybeErrToMaybe $ initUM bind_fn $
517 do { subst <- unifyList emptyTvSubstEnv tys1 tys2
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
523 ; return (mkTvSubst in_scope tv_env) }
525 tvs1 = tyVarsOfTypes tys1
526 tvs2 = tyVarsOfTypes tys2
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
534 f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
535 in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
542 %************************************************************************
546 %************************************************************************
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
557 -- Respects newtypes, PredTypes
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
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'
566 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
568 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
569 | tyc1 == tyc2 = unify_tys subst tys1 tys2
571 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
572 = do { subst' <- unify subst ty1a ty2a
573 ; unify subst' ty1b ty2b }
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 }
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 }
589 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
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))
600 ------------------------------
601 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
602 unify_tys subst xs ys = unifyList subst xs ys
604 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
605 unifyList subst orig_xs orig_ys
606 = go subst orig_xs orig_ys
608 go subst [] [] = return subst
609 go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
611 go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
613 ---------------------------------
614 uVar :: TvSubstEnv -- An existing substitution to extend
615 -> TyVar -- Type variable to be unified
616 -> Type -- with this type
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)
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
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)
636 -- We know that tv1 isn't refined
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
643 -- and then unify a ~ Foo a
645 uUnrefined subst tv1 ty2 (TyVarTy tv2)
646 | tv1 == tv2 -- Same type variable
649 -- Check to see whether tv2 is refined
650 | Just ty' <- lookupVarEnv subst tv2
651 = uUnrefined subst tv1 ty' ty'
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
658 (BindMe, _) -> bind tv1 ty2
659 (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
660 (Skolem, _) -> bind tv2 ty1
663 | k1 `isSubKind` k2 = bindTv subst tv2 ty1 -- Must update tv2
664 | k2 `isSubKind` k1 = bindTv subst tv1 ty2 -- Must update tv1
666 | otherwise = failWith (kindMisMatch tv1 ty2)
671 bind tv ty = return $ extendVarEnv subst tv ty
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
679 = bindTv subst tv1 ty2 -- Bind tyvar to the synonym if poss
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
688 = foldVarSet (unionVarSet . get) emptyVarSet tvs
690 get tv = case lookupVarEnv subst tv of
691 Nothing -> unitVarSet tv
692 Just ty -> substTvSet subst (tyVarsOfType ty)
694 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
695 bindTv subst tv ty -- ty is not a type variable
696 = do { b <- tvBindFlag tv
698 Skolem -> failWith (misMatch (TyVarTy tv) ty)
699 BindMe -> return $ extendVarEnv subst tv ty
703 %************************************************************************
707 %************************************************************************
711 = BindMe -- A regular type variable
713 | Skolem -- This type variable is a skolem constant
714 -- Don't bind it; it only matches itself
718 %************************************************************************
722 %************************************************************************
725 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
726 -> MaybeErr Message a }
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)
735 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
736 initUM badtvs um = unUM um badtvs
738 tvBindFlag :: TyVar -> UM BindFlag
739 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
741 failWith :: Message -> UM a
742 failWith msg = UM (\_tv_fn -> Failed msg)
744 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
745 maybeErrToMaybe (Succeeded a) = Just a
746 maybeErrToMaybe (Failed _) = Nothing
750 %************************************************************************
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.
757 %************************************************************************
760 misMatch :: Type -> Type -> SDoc
762 = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+>
763 ptext (sLit "and") <+> quotes (ppr t2)
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) ]
770 kindMisMatch :: TyVar -> Type -> SDoc
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)]
777 occursCheck :: TyVar -> Type -> SDoc
779 = hang (ptext (sLit "Can't construct the infinite type"))
780 2 (ppr tv <+> equals <+> ppr ty)