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 | tv1' `elemVarSet` me_tmpls menv
162 = case lookupVarEnv subst tv1' of
163 Nothing -- No existing binding
164 | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
165 -> Nothing -- Occurs check
167 -> do { subst1 <- match_kind menv subst tv1 ty2
168 ; return (extendVarEnv subst1 tv1' ty2) }
169 -- Note [Matching kinds]
171 Just ty1' -- There is an existing binding; check whether ty2 matches it
172 | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
173 -- ty1 has no locally-bound variables, hence nukeRnEnvL
174 -- Note tcEqType...we are doing source-type matching here
176 | otherwise -> Nothing -- ty2 doesn't match
179 | otherwise -- tv1 is not a template tyvar
181 TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
185 tv1' = rnOccL rn_env tv1
187 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
188 = match menv' subst ty1 ty2
189 where -- Use the magic of rnBndr2 to go under the binders
190 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
192 match menv subst (PredTy p1) (PredTy p2)
193 = match_pred menv subst p1 p2
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 }
209 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
210 -- Match the kind of the template tyvar with the kind of Type
211 -- Note [Matching kinds]
212 match_kind menv subst tv ty
213 | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
214 (ty3,ty4) = coercionKind ty
215 ; subst1 <- match menv subst ty1 ty3
216 ; match menv subst1 ty2 ty4 }
217 | otherwise = if typeKind ty `isSubKind` tyVarKind tv
221 -- Note [Matching kinds]
222 -- ~~~~~~~~~~~~~~~~~~~~~
223 -- For ordinary type variables, we don't want (m a) to match (n b)
224 -- if say (a::*) and (b::*->*). This is just a yes/no issue.
226 -- For coercion kinds matters are more complicated. If we have a
227 -- coercion template variable co::a~[b], where a,b are presumably also
228 -- template type variables, then we must match co's kind against the
229 -- kind of the actual argument, so as to give bindings to a,b.
231 -- In fact I have no example in mind that *requires* this kind-matching
232 -- to instantiate template type variables, but it seems like the right
233 -- thing to do. C.f. Note [Matching variable types] in Rules.lhs
236 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
237 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
240 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
241 -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
242 match_list _ subst [] [] = Just subst
243 match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2
244 ; match_list fn subst' tys1 tys2 }
245 match_list _ _ _ _ = Nothing
248 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
249 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
250 | c1 == c2 = match_tys menv subst tys1 tys2
251 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
252 | n1 == n2 = match menv subst t1 t2
253 match_pred _ _ _ _ = Nothing
257 %************************************************************************
261 %************************************************************************
263 Note [Pruning dead case alternatives]
264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
265 Consider data T a where
273 type instance F Bool = Int
275 Now consider case x of { T1 -> e1; T2 -> e2 }
277 The question before the house is this: if I know something about the type
278 of x, can I prune away the T1 alternative?
280 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
281 Answer = YES (clearly)
283 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
284 to 'Bool', in which case x::T Int, so
285 ANSWER = NO (clearly)
287 Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom)
288 value of type (T X) using T1. But *in FC* it's quite possible. The newtype
291 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
292 of type (T X) constructed with T1. Hence
293 ANSWER = NO (surprisingly)
295 Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving
296 mechanism uses a cast, just as above, to move from one dictionary to another,
297 in effect giving the programmer access to CoX.
299 Finally, suppose x::T Y. Then *even in FC* we can't construct a
300 non-bottom value of type (T Y) using T1. That's because we can get
301 from Y to Char, but not to Int.
304 Here's a related question. data Eq a b where EQ :: Eq a a
306 case x of { EQ -> ... }
308 Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
310 What about x::Eq Int a, in a context where we have evidence that a~Char.
311 Then again the alternative is dead.
316 We are really doing a test for unsatisfiability of the type
317 constraints implied by the match. And that is clearly, in general, a
320 However, since we are simply dropping dead code, a conservative test
321 suffices. There is a continuum of tests, ranging from easy to hard, that
322 drop more and more dead code.
324 For now we implement a very simple test: type variables match
325 anything, type functions (incl newtypes) match anything, and only
326 distinct data types fail to match. We can elaborate later.
329 dataConCannotMatch :: [Type] -> DataCon -> Bool
330 -- Returns True iff the data con *definitely cannot* match a
331 -- scrutinee of type (T tys)
332 -- where T is the type constructor for the data con
334 dataConCannotMatch tys con
335 | null eq_spec = False -- Common
336 | all isTyVarTy tys = False -- Also common
338 = cant_match_s (map (substTyVar subst . fst) eq_spec)
341 dc_tvs = dataConUnivTyVars con
342 eq_spec = dataConEqSpec con
343 subst = zipTopTvSubst dc_tvs tys
345 cant_match_s :: [Type] -> [Type] -> Bool
346 cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
347 or (zipWith cant_match tys1 tys2)
349 cant_match :: Type -> Type -> Bool
351 | Just t1' <- coreView t1 = cant_match t1' t2
352 | Just t2' <- coreView t2 = cant_match t1 t2'
354 cant_match (FunTy a1 r1) (FunTy a2 r2)
355 = cant_match a1 a2 || cant_match r1 r2
357 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
358 | isDataTyCon tc1 && isDataTyCon tc2
359 = tc1 /= tc2 || cant_match_s tys1 tys2
361 cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
362 cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
363 -- tc can't be FunTyCon by invariant
365 cant_match (AppTy f1 a1) ty2
366 | Just (f2, a2) <- repSplitAppTy_maybe ty2
367 = cant_match f1 f2 || cant_match a1 a2
368 cant_match ty1 (AppTy f2 a2)
369 | Just (f1, a1) <- repSplitAppTy_maybe ty1
370 = cant_match f1 f2 || cant_match a1 a2
372 cant_match _ _ = False -- Safe!
374 -- Things we could add;
376 -- look through newtypes
377 -- take account of tyvar bindings (EQ example above)
381 %************************************************************************
385 %************************************************************************
388 data Refinement = Reft InScopeSet InternalReft
390 type InternalReft = TyVarEnv (Coercion, Type)
391 -- INVARIANT: a->(co,ty) then co :: (a:=:ty)
392 -- Not necessarily idemopotent
394 instance Outputable Refinement where
395 ppr (Reft _in_scope env)
396 = ptext SLIT("Refinement") <+>
399 emptyRefinement :: Refinement
400 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
402 isEmptyRefinement :: Refinement -> Bool
403 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
405 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
406 -- Apply the refinement to the type.
407 -- If (refineType r ty) = (co, ty')
408 -- Then co :: ty:=:ty'
409 -- Nothing => the refinement does nothing to this type
410 refineType (Reft in_scope env) ty
411 | not (isEmptyVarEnv env), -- Common case
412 any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
413 = Just (substTy co_subst ty, substTy tv_subst ty)
415 = Nothing -- The type doesn't mention any refined type variables
417 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
418 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
420 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
421 refinePred (Reft in_scope env) pred
422 | not (isEmptyVarEnv env), -- Common case
423 any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
424 = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
426 = Nothing -- The type doesn't mention any refined type variables
428 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
429 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
431 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
432 -- Like refineType, but returns the 'sym' coercion
433 -- If (refineResType r ty) = (co, ty')
434 -- Then co :: ty':=:ty
435 refineResType reft ty
436 = case refineType reft ty of
437 Just (co, ty1) -> Just (mkSymCoercion co, ty1)
442 %************************************************************************
444 Simple generation of a type refinement
446 %************************************************************************
449 matchRefine :: [CoVar] -> Refinement
452 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
453 is a specialisation of ty1, produce a type refinement that maps the variables
454 of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
456 matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
457 = { right (left (right co)) :: a ~ c
458 , right (right co) :: b ~ Maybe d
461 Precondition: The rhs types must indeed be a specialisation of the lhs types;
462 i.e., some free variables of the lhs are replaced with either distinct free
463 variables or proper type terms to obtain the rhs. (We don't perform full
464 unification or type matching here!)
466 NB: matchRefine does *not* expand the type synonyms.
470 = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
472 in_scope = foldr extend emptyInScopeSet co_vars
474 -- For each co_var, add it *and* the tyvars it mentions, to in_scope
475 extend co_var in_scope
476 = extendInScopeSetSet in_scope $
477 extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
479 refineOne co_var = refine (TyVarTy co_var) ty1 ty2
481 (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
483 refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
484 refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
485 refine _ (PredTy _) (PredTy _) =
486 error "Unify.matchRefine: PredTy"
487 refine co (FunTy arg res) (FunTy arg' res') =
488 refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
490 refine (mkRightCoercion co) res res'
491 refine co (AppTy fun arg) (AppTy fun' arg') =
492 refine (mkLeftCoercion co) fun fun'
494 refine (mkRightCoercion co) arg arg'
495 refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
496 refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
497 refine _ _ _ = error "RcGadt.matchRefine: mismatch"
499 refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
500 refineArgs co tys tys' =
501 fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
503 refineArg (ty, ty') (reft, coWrapper)
504 = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
505 mkLeftCoercion . coWrapper)
509 %************************************************************************
513 %************************************************************************
516 tcUnifyTys :: (TyVar -> BindFlag)
518 -> Maybe TvSubst -- A regular one-shot substitution
519 -- The two types may have common type variables, and indeed do so in the
520 -- second call to tcUnifyTys in FunDeps.checkClsFD
522 tcUnifyTys bind_fn tys1 tys2
523 = maybeErrToMaybe $ initUM bind_fn $
524 do { subst <- unifyList emptyTvSubstEnv tys1 tys2
526 -- Find the fixed point of the resulting non-idempotent substitution
527 ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
528 tv_env = fixTvSubstEnv in_scope subst
530 ; return (mkTvSubst in_scope tv_env) }
532 tvs1 = tyVarsOfTypes tys1
533 tvs2 = tyVarsOfTypes tys2
535 ----------------------------
536 -- XXX Can we do this more nicely, by exploiting laziness?
537 -- Or avoid needing it in the first place?
538 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
539 fixTvSubstEnv in_scope env = f env
541 f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
542 in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
549 %************************************************************************
553 %************************************************************************
556 unify :: TvSubstEnv -- An existing substitution to extend
557 -> Type -> Type -- Types to be unified, and witness of their equality
558 -> UM TvSubstEnv -- Just the extended substitution,
559 -- Nothing if unification failed
560 -- We do not require the incoming substitution to be idempotent,
561 -- nor guarantee that the outgoing one is. That's fixed up by
564 -- Respects newtypes, PredTypes
566 -- in unify, any NewTcApps/Preds should be taken at face value
567 unify subst (TyVarTy tv1) ty2 = uVar subst tv1 ty2
568 unify subst ty1 (TyVarTy tv2) = uVar subst tv2 ty1
570 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
571 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
573 unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
575 unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
576 | tyc1 == tyc2 = unify_tys subst tys1 tys2
578 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
579 = do { subst' <- unify subst ty1a ty2a
580 ; unify subst' ty1b ty2b }
582 -- Applications need a bit of care!
583 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
584 -- NB: we've already dealt with type variables and Notes,
585 -- so if one type is an App the other one jolly well better be too
586 unify subst (AppTy ty1a ty1b) ty2
587 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
588 = do { subst' <- unify subst ty1a ty2a
589 ; unify subst' ty1b ty2b }
591 unify subst ty1 (AppTy ty2a ty2b)
592 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
593 = do { subst' <- unify subst ty1a ty2a
594 ; unify subst' ty1b ty2b }
596 unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
599 ------------------------------
600 unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
601 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
602 | c1 == c2 = unify_tys subst tys1 tys2
603 unify_pred subst (IParam n1 t1) (IParam n2 t2)
604 | n1 == n2 = unify subst t1 t2
605 unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
607 ------------------------------
608 unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
609 unify_tys subst xs ys = unifyList subst xs ys
611 unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
612 unifyList subst orig_xs orig_ys
613 = go subst orig_xs orig_ys
615 go subst [] [] = return subst
616 go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
618 go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
620 ---------------------------------
621 uVar :: TvSubstEnv -- An existing substitution to extend
622 -> TyVar -- Type variable to be unified
623 -> Type -- with this type
626 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
627 -- if swap=False (tv1:=:ty)
628 -- if swap=True (ty:=:tv1)
631 = -- Check to see whether tv1 is refined by the substitution
632 case (lookupVarEnv subst tv1) of
633 Just ty' -> unify subst ty' ty -- Yes, call back into unify'
634 Nothing -> uUnrefined subst -- No, continue
637 uUnrefined :: TvSubstEnv -- An existing substitution to extend
638 -> TyVar -- Type variable to be unified
639 -> Type -- with this type
640 -> Type -- (version w/ expanded synonyms)
643 -- We know that tv1 isn't refined
645 uUnrefined subst tv1 ty2 ty2'
646 | Just ty2'' <- tcView ty2'
647 = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
648 -- This is essential, in case we have
650 -- and then unify a :=: Foo a
652 uUnrefined subst tv1 ty2 (TyVarTy tv2)
653 | tv1 == tv2 -- Same type variable
656 -- Check to see whether tv2 is refined
657 | Just ty' <- lookupVarEnv subst tv2
658 = uUnrefined subst tv1 ty' ty'
660 -- So both are unrefined; next, see if the kinds force the direction
661 | eqKind k1 k2 -- Can update either; so check the bind-flags
662 = do { b1 <- tvBindFlag tv1
663 ; b2 <- tvBindFlag tv2
665 (BindMe, _) -> bind tv1 ty2
667 (AvoidMe, BindMe) -> bind tv2 ty1
668 (AvoidMe, _) -> bind tv1 ty2
670 (WildCard, WildCard) -> return subst
671 (WildCard, Skolem) -> return subst
672 (WildCard, _) -> bind tv2 ty1
674 (Skolem, WildCard) -> return subst
675 (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
676 (Skolem, _) -> bind tv2 ty1
679 | k1 `isSubKind` k2 = bindTv subst tv2 ty1 -- Must update tv2
680 | k2 `isSubKind` k1 = bindTv subst tv1 ty2 -- Must update tv1
682 | otherwise = failWith (kindMisMatch tv1 ty2)
687 bind tv ty = return $ extendVarEnv subst tv ty
689 uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
690 | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
691 = failWith (occursCheck tv1 ty2) -- Occurs check
692 | not (k2 `isSubKind` k1)
693 = failWith (kindMisMatch tv1 ty2) -- Kind check
695 = bindTv subst tv1 ty2 -- Bind tyvar to the synonym if poss
700 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
701 -- Apply the non-idempotent substitution to a set of type variables,
702 -- remembering that the substitution isn't necessarily idempotent
704 = foldVarSet (unionVarSet . get) emptyVarSet tvs
706 get tv = case lookupVarEnv subst tv of
707 Nothing -> unitVarSet tv
708 Just ty -> substTvSet subst (tyVarsOfType ty)
710 bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
711 bindTv subst tv ty -- ty is not a type variable
712 = do { b <- tvBindFlag tv
714 Skolem -> failWith (misMatch (TyVarTy tv) ty)
715 WildCard -> return subst
716 _other -> return $ extendVarEnv subst tv ty
720 %************************************************************************
724 %************************************************************************
728 = BindMe -- A regular type variable
729 | AvoidMe -- Like BindMe but, given the choice, avoid binding it
731 | Skolem -- This type variable is a skolem constant
732 -- Don't bind it; it only matches itself
734 | WildCard -- This type variable matches anything,
735 -- and does not affect the substitution
737 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
738 -> MaybeErr Message a }
740 instance Monad UM where
741 return a = UM (\_tvs -> Succeeded a)
742 fail s = UM (\_tvs -> Failed (text s))
743 m >>= k = UM (\tvs -> case unUM m tvs of
744 Failed err -> Failed err
745 Succeeded v -> unUM (k v) tvs)
747 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
748 initUM badtvs um = unUM um badtvs
750 tvBindFlag :: TyVar -> UM BindFlag
751 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
753 failWith :: Message -> UM a
754 failWith msg = UM (\_tv_fn -> Failed msg)
756 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
757 maybeErrToMaybe (Succeeded a) = Just a
758 maybeErrToMaybe (Failed _) = Nothing
762 %************************************************************************
765 We go to a lot more trouble to tidy the types
766 in TcUnify. Maybe we'll end up having to do that
767 here too, but I'll leave it for now.
769 %************************************************************************
772 misMatch :: Type -> Type -> SDoc
774 = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
775 ptext SLIT("and") <+> quotes (ppr t2)
777 lengthMisMatch :: [Type] -> [Type] -> SDoc
778 lengthMisMatch tys1 tys2
779 = sep [ptext SLIT("Can't match unequal length lists"),
780 nest 2 (ppr tys1), nest 2 (ppr tys2) ]
782 kindMisMatch :: TyVar -> Type -> SDoc
784 = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
785 ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
786 ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
787 ptext SLIT("with") <+> quotes (ppr t2)]
789 occursCheck :: TyVar -> Type -> SDoc
791 = hang (ptext SLIT("Can't construct the infinite type"))
792 2 (ppr tv <+> equals <+> ppr ty)