2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Type subsumption and unification
10 -- Full-blown subsumption
11 tcWrapResult, tcSubType, tcGen,
12 checkConstraints, newImplication, sigCtxt,
14 -- Various unifications
15 unifyType, unifyTypeList, unifyTheta, unifyKind,
17 --------------------------------
20 matchExpectedListTy, matchExpectedPArrTy,
21 matchExpectedTyConApp, matchExpectedAppTy,
22 matchExpectedFunTys, matchExpectedFunKind,
23 wrapFunResCoercion, failWithMisMatch
26 #include "HsVersions.h"
30 import CoreUtils( mkPiTypes )
31 import TcErrors ( unifyCtxt )
47 import Maybes ( allMaybes )
56 %************************************************************************
58 matchExpected functions
60 %************************************************************************
62 Note [Herald for matchExpectedFunTys]
63 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
64 The 'herald' always looks like:
65 "The equation(s) for 'f' have"
66 "The abstraction (\x.e) takes"
67 "The section (+ x) expects"
68 "The function 'f' is applied to"
70 This is used to construct a message of form
72 The abstraction `\Just 1 -> ...' takes two arguments
73 but its type `Maybe a -> a' has only one
75 The equation(s) for `f' have two arguments
76 but its type `Maybe a -> a' has only one
78 The section `(f 3)' requires 'f' to take two arguments
79 but its type `Int -> Int' has only one
81 The function 'f' is applied to two arguments
82 but its type `Int -> Int' has only one
84 Note [matchExpectedFunTys]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~
86 matchExpectedFunTys checks that an (Expected rho) has the form
87 of an n-ary function. It passes the decomposed type to the
88 thing_inside, and returns a wrapper to coerce between the two types
90 It's used wherever a language construct must have a functional type,
96 This is not (currently) where deep skolemisation occurs;
97 matchExpectedFunTys does not skolmise nested foralls in the
98 expected type, becuase it expects that to have been done already
102 matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
105 -> TcM (Coercion, [TcSigmaType], TcRhoType)
107 -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
108 -- then co : ty ~ (t1 -> ... -> tn -> ty_r)
110 -- Does not allocate unnecessary meta variables: if the input already is
111 -- a function, we just take it apart. Not only is this efficient,
112 -- it's important for higher rank: the argument might be of form
113 -- (forall a. ty) -> other
114 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
115 -- hide the forall inside a meta-variable
117 matchExpectedFunTys herald arity orig_ty
120 -- If go n ty = (co, [t1,..,tn], ty_r)
121 -- then co : ty ~ t1 -> .. -> tn -> ty_r
124 | n_req == 0 = return (mkReflCo ty, [], ty)
127 | Just ty' <- tcView ty = go n_req ty'
129 go n_req (FunTy arg_ty res_ty)
130 | not (isPredTy arg_ty)
131 = do { (coi, tys, ty_r) <- go (n_req-1) res_ty
132 ; return (mkFunCo (mkReflCo arg_ty) coi, arg_ty:tys, ty_r) }
134 go _ (TyConApp tc _) -- A common case
135 | not (isSynFamilyTyCon tc)
136 = do { (env,msg) <- mk_ctxt emptyTidyEnv
137 ; failWithTcM (env,msg) }
139 go n_req ty@(TyVarTy tv)
140 | ASSERT( isTcTyVar tv) isMetaTyVar tv
141 = do { cts <- readMetaTyVar tv
143 Indirect ty' -> go n_req ty'
144 Flexi -> defer n_req ty }
146 -- In all other cases we bale out into ordinary unification
147 go n_req ty = defer n_req ty
151 = addErrCtxtM mk_ctxt $
152 do { arg_tys <- newFlexiTyVarTys n_req argTypeKind
153 ; res_ty <- newFlexiTyVarTy openTypeKind
154 ; coi <- unifyType fun_ty (mkFunTys arg_tys res_ty)
155 ; return (coi, arg_tys, res_ty) }
158 mk_ctxt :: TidyEnv -> TcM (TidyEnv, Message)
159 mk_ctxt env = do { orig_ty1 <- zonkTcType orig_ty
160 ; let (env', orig_ty2) = tidyOpenType env orig_ty1
161 (args, _) = tcSplitFunTys orig_ty2
162 n_actual = length args
163 ; return (env', mk_msg orig_ty2 n_actual) }
166 = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
167 sep [ptext (sLit "but its type") <+> quotes (pprType ty),
168 if n_args == 0 then ptext (sLit "has none")
169 else ptext (sLit "has only") <+> speakN n_args]
174 ----------------------
175 matchExpectedListTy :: TcRhoType -> TcM (Coercion, TcRhoType)
176 -- Special case for lists
177 matchExpectedListTy exp_ty
178 = do { (coi, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
179 ; return (coi, elt_ty) }
181 ----------------------
182 matchExpectedPArrTy :: TcRhoType -> TcM (Coercion, TcRhoType)
183 -- Special case for parrs
184 matchExpectedPArrTy exp_ty
185 = do { (coi, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
186 ; return (coi, elt_ty) }
188 ----------------------
189 matchExpectedTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
190 -> TcRhoType -- orig_ty
191 -> TcM (Coercion, -- T a b c ~ orig_ty
192 [TcSigmaType]) -- Element types, a b c
194 -- It's used for wired-in tycons, so we call checkWiredInTyCon
195 -- Precondition: never called with FunTyCon
196 -- Precondition: input type :: *
198 matchExpectedTyConApp tc orig_ty
199 = do { checkWiredInTyCon tc
200 ; go (tyConArity tc) orig_ty [] }
202 go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (Coercion, [TcSigmaType])
203 -- If go n ty tys = (co, [t1..tn] ++ tys)
204 -- then co : T t1..tn ~ ty
207 | Just ty' <- tcView ty = go n_req ty' tys
209 go n_req ty@(TyVarTy tv) tys
210 | ASSERT( isTcTyVar tv) isMetaTyVar tv
211 = do { cts <- readMetaTyVar tv
213 Indirect ty -> go n_req ty tys
214 Flexi -> defer n_req ty tys }
216 go n_req ty@(TyConApp tycon args) tys
218 = ASSERT( n_req == length args) -- ty::*
219 return (mkReflCo ty, args ++ tys)
221 go n_req (AppTy fun arg) tys
223 = do { (coi, args) <- go (n_req - 1) fun (arg : tys)
224 ; return (mkAppCo coi (mkReflCo arg), args) }
226 go n_req ty tys = defer n_req ty tys
230 = do { tau_tys <- mapM newFlexiTyVarTy arg_kinds
231 ; coi <- unifyType (mkTyConApp tc tau_tys) ty
232 ; return (coi, tau_tys ++ tys) }
234 (arg_kinds, _) = splitKindFunTysN n_req (tyConKind tc)
236 ----------------------
237 matchExpectedAppTy :: TcRhoType -- orig_ty
238 -> TcM (Coercion, -- m a ~ orig_ty
239 (TcSigmaType, TcSigmaType)) -- Returns m, a
240 -- If the incoming type is a mutable type variable of kind k, then
241 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
243 matchExpectedAppTy orig_ty
247 | Just ty' <- tcView ty = go ty'
249 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
250 = return (mkReflCo orig_ty, (fun_ty, arg_ty))
253 | ASSERT( isTcTyVar tv) isMetaTyVar tv
254 = do { cts <- readMetaTyVar tv
261 -- Defer splitting by generating an equality constraint
262 defer = do { ty1 <- newFlexiTyVarTy kind1
263 ; ty2 <- newFlexiTyVarTy kind2
264 ; coi <- unifyType (mkAppTy ty1 ty2) orig_ty
265 ; return (coi, (ty1, ty2)) }
267 orig_kind = typeKind orig_ty
268 kind1 = mkArrowKind liftedTypeKind (defaultKind orig_kind)
269 kind2 = liftedTypeKind -- m :: * -> k
271 -- The defaultKind is a bit smelly. If you remove it,
272 -- try compiling f x = do { x }
273 -- and you'll get a kind mis-match. It smells, but
274 -- not enough to lose sleep over.
278 %************************************************************************
282 %************************************************************************
284 All the tcSub calls have the form
285 tcSub actual_ty expected_ty
287 actual_ty <= expected_ty
289 That is, that a value of type actual_ty is acceptable in
290 a place expecting a value of type expected_ty.
292 It returns a coercion function
293 co_fn :: actual_ty ~ expected_ty
294 which takes an HsExpr of type actual_ty into one of type
298 tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
299 -- Check that ty_actual is more polymorphic than ty_expected
300 -- Both arguments might be polytypes, so we must instantiate and skolemise
301 -- Returns a wrapper of shape ty_actual ~ ty_expected
302 tcSubType origin ctxt ty_actual ty_expected
303 | isSigmaTy ty_actual
304 = do { (sk_wrap, inst_wrap)
305 <- tcGen ctxt ty_expected $ \ _ sk_rho -> do
306 { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
307 ; coi <- unifyType in_rho sk_rho
308 ; return (coToHsWrapper coi <.> in_wrap) }
309 ; return (sk_wrap <.> inst_wrap) }
311 | otherwise -- Urgh! It seems deeply weird to have equality
312 -- when actual is not a polytype, and it makes a big
313 -- difference e.g. tcfail104
314 = do { coi <- unifyType ty_actual ty_expected
315 ; return (coToHsWrapper coi) }
317 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
318 tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind
323 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
324 tcWrapResult expr actual_ty res_ty
325 = do { coi <- unifyType actual_ty res_ty
326 -- Both types are deeply skolemised
327 ; return (mkHsWrapCo coi expr) }
329 -----------------------------------
331 :: [TcType] -- Type of args
332 -> HsWrapper -- HsExpr a -> HsExpr b
333 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
334 wrapFunResCoercion arg_tys co_fn_res
335 | isIdHsWrapper co_fn_res
340 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
341 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
346 %************************************************************************
348 \subsection{Generalisation}
350 %************************************************************************
353 tcGen :: UserTypeCtxt -> TcType
354 -> ([TcTyVar] -> TcRhoType -> TcM result)
355 -> TcM (HsWrapper, result)
356 -- The expression has type: spec_ty -> expected_ty
358 tcGen ctxt expected_ty thing_inside
359 -- We expect expected_ty to be a forall-type
360 -- If not, the call is a no-op
361 = do { traceTc "tcGen" empty
362 ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
365 traceTc "tcGen" $ vcat [
366 text "expected_ty" <+> ppr expected_ty,
367 text "inst ty" <+> ppr tvs' <+> ppr rho' ]
369 -- Generally we must check that the "forall_tvs" havn't been constrained
370 -- The interesting bit here is that we must include the free variables
371 -- of the expected_ty. Here's an example:
372 -- runST (newVar True)
373 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
374 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
375 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
376 -- So now s' isn't unconstrained because it's linked to a.
378 -- However [Oct 10] now that the untouchables are a range of
379 -- TcTyVars, all this is handled automatically with no need for
380 -- extra faffing around
382 -- Use the *instantiated* type in the SkolemInfo
383 -- so that the names of displayed type variables line up
384 ; let skol_info = SigSkol ctxt (mkPiTypes given rho')
386 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
387 thing_inside tvs' rho'
389 ; return (wrap <.> mkWpLet ev_binds, result) }
390 -- The ev_binds returned by checkConstraints is very
391 -- often empty, in which case mkWpLet is a no-op
393 checkConstraints :: SkolemInfo
394 -> [TcTyVar] -- Skolems
397 -> TcM (TcEvBinds, result)
399 checkConstraints skol_info skol_tvs given thing_inside
400 | null skol_tvs && null given
401 = do { res <- thing_inside; return (emptyTcEvBinds, res) }
402 -- Just for efficiency. We check every function argument with
403 -- tcPolyExpr, which uses tcGen and hence checkConstraints.
406 = newImplication skol_info skol_tvs given thing_inside
408 newImplication :: SkolemInfo -> [TcTyVar]
409 -> [EvVar] -> TcM result
410 -> TcM (TcEvBinds, result)
411 newImplication skol_info skol_tvs given thing_inside
412 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
413 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
414 do { ((result, untch), wanted) <- captureConstraints $
415 captureUntouchables $
418 ; if isEmptyWC wanted && not (hasEqualities given)
419 -- Optimisation : if there are no wanteds, and the givens
420 -- are sufficiently simple, don't generate an implication
421 -- at all. Reason for the hasEqualities test:
422 -- we don't want to lose the "inaccessible alternative"
425 return (emptyTcEvBinds, result)
427 { ev_binds_var <- newTcEvBinds
428 ; lcl_env <- getLclTypeEnv
429 ; loc <- getCtLoc skol_info
430 ; emitImplication $ Implic { ic_untch = untch
432 , ic_skols = mkVarSet skol_tvs
435 , ic_insol = insolubleWC wanted
436 , ic_binds = ev_binds_var
439 ; return (TcEvBinds ev_binds_var, result) } }
442 %************************************************************************
446 %************************************************************************
448 The exported functions are all defined as versions of some
449 non-exported generic functions.
453 unifyType :: TcTauType -> TcTauType -> TcM Coercion
454 -- Actual and expected types
455 -- Returns a coercion : ty1 ~ ty2
456 unifyType ty1 ty2 = uType [] ty1 ty2
459 unifyPred :: PredType -> PredType -> TcM Coercion
460 -- Actual and expected types
461 unifyPred p1 p2 = uPred [UnifyOrigin (mkPredTy p1) (mkPredTy p2)] p1 p2
464 unifyTheta :: TcThetaType -> TcThetaType -> TcM [Coercion]
465 -- Actual and expected types
466 unifyTheta theta1 theta2
467 = do { checkTc (equalLength theta1 theta2)
468 (vcat [ptext (sLit "Contexts differ in length"),
469 nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
470 ; zipWithM unifyPred theta1 theta2 }
473 @unifyTypeList@ takes a single list of @TauType@s and unifies them
474 all together. It is used, for example, when typechecking explicit
475 lists, when all the elts should be of the same type.
478 unifyTypeList :: [TcTauType] -> TcM ()
479 unifyTypeList [] = return ()
480 unifyTypeList [_] = return ()
481 unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
482 ; unifyTypeList tys }
485 %************************************************************************
489 %************************************************************************
491 uType is the heart of the unifier. Each arg occurs twice, because
492 we want to report errors in terms of synomyms if possible. The first of
493 the pair is used in error messages only; it is always the same as the
494 second, except that if the first is a synonym then the second may be a
495 de-synonym'd version. This way we get better error messages.
499 = NotSwapped -- Args are: actual, expected
500 | IsSwapped -- Args are: expected, actual
502 instance Outputable SwapFlag where
503 ppr IsSwapped = ptext (sLit "Is-swapped")
504 ppr NotSwapped = ptext (sLit "Not-swapped")
506 unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
507 unSwap NotSwapped f a b = f a b
508 unSwap IsSwapped f a b = f b a
511 uType, uType_np, uType_defer
513 -> TcType -- ty1 is the *actual* type
514 -> TcType -- ty2 is the *expected* type
518 -- It is always safe to defer unification to the main constraint solver
519 -- See Note [Deferred unification]
520 uType_defer (item : origin) ty1 ty2
521 = wrapEqCtxt origin $
522 do { co_var <- newCoVar ty1 ty2
523 ; loc <- getCtLoc (TypeEqOrigin item)
524 ; emitFlat (mkEvVarX co_var loc)
528 ; doc <- mkErrInfo emptyTidyEnv ctxt
529 ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin, doc])
531 ; return $ mkCoVarCo co_var }
533 = panic "uType_defer"
536 -- Push a new item on the origin stack (the most common case)
537 uType origin ty1 ty2 -- Push a new item on the origin stack
538 = uType_np (pushOrigin ty1 ty2 origin) ty1 ty2
541 -- unify_np (short for "no push" on the origin stack) does the work
542 uType_np origin orig_ty1 orig_ty2
543 = do { traceTc "u_tys " $ vcat
544 [ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
546 ; coi <- go orig_ty1 orig_ty2
548 then traceTc "u_tys yields no coercion" empty
549 else traceTc "u_tys yields coercion:" (ppr coi)
552 bale_out :: [EqOrigin] -> TcM a
553 bale_out origin = failWithMisMatch origin
555 go :: TcType -> TcType -> TcM Coercion
556 -- The arguments to 'go' are always semantically identical
557 -- to orig_ty{1,2} except for looking through type synonyms
559 -- Variables; go for uVar
560 -- Note that we pass in *original* (before synonym expansion),
561 -- so that type variables tend to get filled in with
562 -- the most informative version of the type
563 go (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2
564 go ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1
567 -- see Note [Unification and synonyms]
568 -- Do this after the variable case so that we tend to unify
569 -- variables with un-expanded type synonym
571 -- Also NB that we recurse to 'go' so that we don't push a
572 -- new item on the origin stack. As a result if we have
574 -- and we try to unify Foo ~ Bool
575 -- we'll end up saying "can't match Foo with Bool"
576 -- rather than "can't match "Int with Bool". See Trac #4535.
578 | Just ty1' <- tcView ty1 = go ty1' ty2
579 | Just ty2' <- tcView ty2 = go ty1 ty2'
582 go (PredTy p1) (PredTy p2) = uPred origin p1 p2
584 -- Functions (or predicate functions) just check the two parts
585 go (FunTy fun1 arg1) (FunTy fun2 arg2)
586 = do { coi_l <- uType origin fun1 fun2
587 ; coi_r <- uType origin arg1 arg2
588 ; return $ mkFunCo coi_l coi_r }
590 -- Always defer if a type synonym family (type function)
591 -- is involved. (Data families behave rigidly.)
592 go ty1@(TyConApp tc1 _) ty2
593 | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
594 go ty1 ty2@(TyConApp tc2 _)
595 | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
597 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
598 | tc1 == tc2 -- See Note [TyCon app]
599 = do { cois <- uList origin uType tys1 tys2
600 ; return $ mkTyConAppCo tc1 cois }
602 -- See Note [Care with type applications]
604 | Just (s2,t2) <- tcSplitAppTy_maybe ty2
605 = do { coi_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy]
606 ; coi_t <- uType origin t1 t2
607 ; return $ mkAppCo coi_s coi_t }
610 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
611 = do { coi_s <- uType_np origin s1 s2
612 ; coi_t <- uType origin t1 t2
613 ; return $ mkAppCo coi_s coi_t }
616 | tcIsForAllTy ty1 || tcIsForAllTy ty2
617 = unifySigmaTy origin ty1 ty2
619 -- Anything else fails
620 go _ _ = bale_out origin
622 unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM Coercion
623 unifySigmaTy origin ty1 ty2
624 = do { let (tvs1, body1) = tcSplitForAllTys ty1
625 (tvs2, body2) = tcSplitForAllTys ty2
626 ; unless (equalLength tvs1 tvs2) (failWithMisMatch origin)
627 ; skol_tvs <- tcInstSkolTyVars tvs1
628 -- Get location from monad, not from tvs1
629 ; let tys = mkTyVarTys skol_tvs
630 in_scope = mkInScopeSet (mkVarSet skol_tvs)
631 phi1 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
632 phi2 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
634 ; ((coi, _untch), lie) <- captureConstraints $
635 captureUntouchables $
636 uType origin phi1 phi2
637 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
638 -- VERY UNSATISFACTORY; the constraint might be fine, but
639 -- we fail eagerly because we don't have any place to put
640 -- the bindings from an implication constraint
641 -- This only works because most constraints get solved on the fly
642 -- See Note [Avoid deferring]
643 ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs)
644 (failWithMisMatch origin) -- ToDo: give details from bad_lie
646 ; emitConstraints lie
647 ; return (foldr mkForAllCo coi skol_tvs) }
650 uPred :: [EqOrigin] -> PredType -> PredType -> TcM Coercion
651 uPred origin (IParam n1 t1) (IParam n2 t2)
653 = do { coi <- uType origin t1 t2
654 ; return $ mkPredCo $ IParam n1 coi }
655 uPred origin (ClassP c1 tys1) (ClassP c2 tys2)
657 = do { cois <- uList origin uType tys1 tys2
658 -- Guaranteed equal lengths because the kinds check
659 ; return $ mkPredCo $ ClassP c1 cois }
661 uPred origin (EqPred ty1a ty1b) (EqPred ty2a ty2b)
662 = do { coa <- uType origin ty1a ty2a
663 ; cob <- uType origin ty1b ty2b
664 ; return $ mkPredCo $ EqPred coa cob }
666 uPred origin _ _ = failWithMisMatch origin
670 -> ([EqOrigin] -> a -> a -> TcM b)
671 -> [a] -> [a] -> TcM [b]
672 -- Unify corresponding elements of two lists of types, which
673 -- should be of equal length. We charge down the list explicitly so that
674 -- we can complain if their lengths differ.
675 uList _ _ [] [] = return []
676 uList origin unify (ty1:tys1) (ty2:tys2) = do { x <- unify origin ty1 ty2;
677 ; xs <- uList origin unify tys1 tys2
679 uList origin _ _ _ = failWithMisMatch origin
680 -- See Note [Mismatched type lists and application decomposition]
684 Note [Care with type applications]
685 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
686 Note: type applications need a bit of care!
687 They can match FunTy and TyConApp, so use splitAppTy_maybe
688 NB: we've already dealt with type variables and Notes,
689 so if one type is an App the other one jolly well better be too
691 Note [Unifying AppTy]
692 ~~~~~~~~~~~~~~~~~~~~~
693 Considerm unifying (m Int) ~ (IO Int) where m is a unification variable
694 that is now bound to (say) (Bool ->). Then we want to report
695 "Can't unify (Bool -> Int) with (IO Int)
697 "Can't unify ((->) Bool) with IO"
698 That is why we use the "_np" variant of uType, which does not alter the error
703 When we find two TyConApps, the argument lists are guaranteed equal
704 length. Reason: intially the kinds of the two types to be unified is
705 the same. The only way it can become not the same is when unifying two
706 AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
707 the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
708 which we do, that ensures that f1,f2 have the same kind; and that
709 means a1,a2 have the same kind. And now the argument repeats.
711 Note [Mismatched type lists and application decomposition]
712 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
713 When we find two TyConApps, you might think that the argument lists
714 are guaranteed equal length. But they aren't. Consider matching
715 w (T x) ~ Foo (T x y)
716 We do match (w ~ Foo) first, but in some circumstances we simply create
717 a deferred constraint; and then go ahead and match (T x ~ T x y).
718 This came up in Trac #3950.
721 (a) either we must check for identical argument kinds
722 when decomposing applications,
724 (b) or we must be prepared for ill-kinded unification sub-problems
726 Currently we adopt (b) since it seems more robust -- no need to maintain
729 Note [Unification and synonyms]
730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
731 If you are tempted to make a short cut on synonyms, as in this
734 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
735 = if (con1 == con2) then
736 -- Good news! Same synonym constructors, so we can shortcut
737 -- by unifying their arguments and ignoring their expansions.
738 unifyTypepeLists args1 args2
740 -- Never mind. Just expand them and try again
743 then THINK AGAIN. Here is the whole story, as detected and reported
746 Here's a test program that should detect the problem:
749 x = (1 :: Bogus Char) :: Bogus Bool
751 The problem with [the attempted shortcut code] is that
755 is not a sufficient condition to be able to use the shortcut!
756 You also need to know that the type synonym actually USES all
757 its arguments. For example, consider the following type synonym
758 which does not use all its arguments.
762 If you ever tried unifying, say, (Bogus Char) with )Bogus Bool), the
763 unifier would blithely try to unify Char with Bool and would fail,
764 even though the expanded forms (both Int) should match. Similarly,
765 unifying (Bogus Char) with (Bogus t) would unnecessarily bind t to
768 ... You could explicitly test for the problem synonyms and mark them
769 somehow as needing expansion, perhaps also issuing a warning to the
772 Note [Deferred Unification]
773 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
774 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
775 and yet its consistency is undetermined. Previously, there was no way to still
776 make it consistent. So a mismatch error was issued.
778 Now these unfications are deferred until constraint simplification, where type
779 family instances and given equations may (or may not) establish the consistency.
780 Deferred unifications are of the form
783 where F is a type function and x is a type variable.
785 id :: x ~ y => x -> y
788 involves the unfication x = y. It is deferred until we bring into account the
789 context x ~ y to establish that it holds.
791 If available, we defer original types (rather than those where closed type
792 synonyms have already been expanded via tcCoreView). This is, as usual, to
793 improve error messages.
796 %************************************************************************
800 %************************************************************************
802 @uVar@ is called when at least one of the types being unified is a
803 variable. It does {\em not} assume that the variable is a fixed point
804 of the substitution; rather, notice that @uVar@ (defined below) nips
805 back into @uTys@ if it turns out that the variable is already bound.
808 uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM Coercion
809 uVar origin swapped tv1 ty2
810 = do { traceTc "uVar" (vcat [ ppr origin
812 , ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
813 , nest 2 (ptext (sLit " ~ "))
814 , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)])
815 ; details <- lookupTcTyVar tv1
817 Filled ty1 -> unSwap swapped (uType_np origin) ty1 ty2
818 Unfilled details1 -> uUnfilledVar origin swapped tv1 details1 ty2
822 uUnfilledVar :: [EqOrigin]
824 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
825 -> TcTauType -- Type 2
827 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
828 -- It might be a skolem, or untouchable, or meta
830 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
831 | tv1 == tv2 -- Same type variable => no-op
832 = return (mkReflCo (mkTyVarTy tv1))
834 | otherwise -- Distinct type variables
835 = do { lookup2 <- lookupTcTyVar tv2
837 Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
838 Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
841 uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type variable
844 -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
846 Nothing -> do { traceTc "Occ/kind defer" (ppr tv1); defer }
847 Just ty2' -> updateMeta tv1 ref1 ty2'
850 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
852 defer | Just ty2' <- tcView non_var_ty2 -- Note [Avoid deferring]
853 -- non_var_ty2 isn't expanded yet
854 = uUnfilledVar origin swapped tv1 details1 ty2'
856 = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
857 -- Occurs check or an untouchable: just defer
858 -- NB: occurs check isn't necessarily fatal:
859 -- eg tv1 occured in type family parameter
862 uUnfilledVars :: [EqOrigin]
864 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
865 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
867 -- Invarant: The type variables are distinct,
868 -- Neither is filled in yet
870 uUnfilledVars origin swapped tv1 details1 tv2 details2
871 = case (details1, details2) of
872 (MetaTv i1 ref1, MetaTv i2 ref2)
873 | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1 i1 i2
874 then updateMeta tv1 ref1 ty2
875 else updateMeta tv2 ref2 ty1
876 | k2_sub_k1 -> updateMeta tv1 ref1 ty2
878 (_, MetaTv _ ref2) | k1_sub_k2 -> updateMeta tv2 ref2 ty1
879 (MetaTv _ ref1, _) | k2_sub_k1 -> updateMeta tv1 ref1 ty2
881 (_, _) -> unSwap swapped (uType_defer origin) ty1 ty2
882 -- Defer for skolems of all sorts
886 k1_sub_k2 = k1 `isSubKind` k2
887 k2_sub_k1 = k2 `isSubKind` k1
891 nicer_to_update_tv1 _ SigTv = True
892 nicer_to_update_tv1 SigTv _ = False
893 nicer_to_update_tv1 _ _ = isSystemName (Var.varName tv1)
894 -- Try not to update SigTvs; and try to update sys-y type
895 -- variables in preference to ones gotten (say) by
896 -- instantiating a polymorphic function with a user-written
900 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
901 -- (checkTauTvUpdate tv ty)
902 -- We are about to update the TauTv tv with ty.
903 -- Check (a) that tv doesn't occur in ty (occurs check)
904 -- (b) that kind(ty) is a sub-kind of kind(tv)
905 -- (c) that ty does not contain any type families, see Note [Type family sharing]
907 -- We have two possible outcomes:
908 -- (1) Return the type to update the type variable with,
909 -- [we know the update is ok]
910 -- (2) Return Nothing,
911 -- [the update might be dodgy]
913 -- Note that "Nothing" does not mean "definite error". For example
915 -- type instance F Int = Int
918 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
919 -- we return Nothing, leaving it to the later constraint simplifier to
922 checkTauTvUpdate tv ty
923 = do { ty' <- zonkTcType ty
924 ; if typeKind ty' `isSubKind` tyVarKind tv then
926 Nothing -> return Nothing
927 Just ty'' -> return (Just ty'')
928 else return Nothing }
930 where ok :: TcType -> Maybe TcType
931 ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv')
932 ok this_ty@(TyConApp tc tys)
933 | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys)
934 = Just (TyConApp tc tys')
935 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
936 = ok ty_expanded -- See Note [Type synonyms and the occur check]
937 ok (PredTy sty) | Just sty' <- ok_pred sty = Just (PredTy sty')
938 ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
939 = Just (FunTy arg' res')
940 ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg
941 = Just (AppTy fun' arg')
942 ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1')
946 ok_pred (IParam nm ty) | Just ty' <- ok ty = Just (IParam nm ty')
947 ok_pred (ClassP cl tys)
948 | Just tys' <- allMaybes (map ok tys)
949 = Just (ClassP cl tys')
950 ok_pred (EqPred ty1 ty2)
951 | Just ty1' <- ok ty1, Just ty2' <- ok ty2
952 = Just (EqPred ty1' ty2')
954 ok_pred _pty = Nothing
957 Note [Avoid deferring]
958 ~~~~~~~~~~~~~~~~~~~~~~
959 We try to avoid creating deferred constraints for two reasons.
961 * Second, currently we can only defer some constraints
962 under a forall. See unifySigmaTy.
963 So expanding synonyms here is a good thing to do. Example (Trac #4917)
965 where type Const a b = a. We can solve this immediately, even when
966 'a' is a skolem, just by expanding the synonym; and we should do so
967 in case this unification happens inside unifySigmaTy (sigh).
969 Note [Type synonyms and the occur check]
970 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
971 Generally speaking we try to update a variable with type synonyms not
972 expanded, which improves later error messages, unless looking
973 inside a type synonym may help resolve a spurious occurs check
977 f :: (A a -> a -> ()) -> ()
983 We will eventually get a constraint of the form t ~ A t. The ok function above will
984 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
985 unified with the original type A t, we would lead the type checker into an infinite loop.
987 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
988 the ok function expands the synonym to detect opportunities for occurs check success using
989 the underlying definition of the type synonym.
991 The same applies later on in the constraint interaction code; see TcInteract,
992 function @occ_check_ok@.
995 Note [Type family sharing]
997 We must avoid eagerly unifying type variables to types that contain function symbols,
998 because this may lead to loss of sharing, and in turn, in very poor performance of the
999 constraint simplifier. Assume that we have a wanted constraint:
1008 where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m2],
1009 then, after zonking, our constraint simplifier will be faced with the following wanted
1016 which has to be flattened by the constraint solver. However, because the sharing is lost,
1017 an polynomially larger number of flatten skolems will be created and the constraint sets
1018 we are working with will be polynomially larger.
1020 Instead, if we defer the unifications m1 := [F m2], etc. we will only be generating three
1021 flatten skolems, which is the maximum possible sharing arising from the original constraint.
1024 data LookupTyVarResult -- The result of a lookupTcTyVar call
1025 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
1028 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
1030 | MetaTv _ ref <- details
1031 = do { meta_details <- readMutVar ref
1032 ; case meta_details of
1033 Indirect ty -> return (Filled ty)
1034 Flexi -> do { is_untch <- isUntouchable tyvar
1035 ; let -- Note [Unifying untouchables]
1036 ret_details | is_untch = vanillaSkolemTv
1037 | otherwise = details
1038 ; return (Unfilled ret_details) } }
1040 = return (Unfilled details)
1042 details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
1043 tcTyVarDetails tyvar
1045 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM Coercion
1046 updateMeta tv1 ref1 ty2
1047 = do { writeMetaTyVarRef tv1 ref1 ty2
1048 ; return (mkReflCo ty2) }
1051 Note [Unifying untouchables]
1052 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1053 We treat an untouchable type variable as if it was a skolem. That
1054 ensures it won't unify with anything. It's a slight had, because
1055 we return a made-up TcTyVarDetails, but I think it works smoothly.
1058 %************************************************************************
1062 %************************************************************************
1065 pushOrigin :: TcType -> TcType -> [EqOrigin] -> [EqOrigin]
1066 pushOrigin ty_act ty_exp origin
1067 = UnifyOrigin { uo_actual = ty_act, uo_expected = ty_exp } : origin
1070 wrapEqCtxt :: [EqOrigin] -> TcM a -> TcM a
1071 -- Build a suitable error context from the origin and do the thing inside
1072 -- The "couldn't match" error comes from the innermost item on the stack,
1073 -- and, if there is more than one item, the "Expected/inferred" part
1074 -- comes from the outermost item
1075 wrapEqCtxt [] thing_inside = thing_inside
1076 wrapEqCtxt items thing_inside = addErrCtxtM (unifyCtxt (last items)) thing_inside
1079 failWithMisMatch :: [EqOrigin] -> TcM a
1080 -- Generate the message when two types fail to match,
1081 -- going to some trouble to make it helpful.
1082 -- We take the failing types from the top of the origin stack
1083 -- rather than reporting the particular ones we are looking
1085 failWithMisMatch (item:origin)
1086 = wrapEqCtxt origin $
1087 do { ty_act <- zonkTcType (uo_actual item)
1088 ; ty_exp <- zonkTcType (uo_expected item)
1089 ; env0 <- tcInitTidyEnv
1090 ; let (env1, pp_exp) = tidyOpenType env0 ty_exp
1091 (env2, pp_act) = tidyOpenType env1 ty_act
1092 ; failWithTcM (env2, misMatchMsg pp_act pp_exp) }
1094 = panic "failWithMisMatch"
1096 misMatchMsg :: TcType -> TcType -> SDoc
1097 misMatchMsg ty_act ty_exp
1098 = sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp)
1099 , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)]
1103 -----------------------------------------
1105 -----------------------------------------
1109 -- If an error happens we try to figure out whether the function
1110 -- function has been given too many or too few arguments, and say so.
1111 addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
1112 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
1113 = addErrCtxtM mk_err thing_inside
1116 = do { exp_ty' <- zonkTcType expected_res_ty
1117 ; act_ty' <- zonkTcType actual_res_ty
1118 ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1119 (env2, act_ty'') = tidyOpenType env1 act_ty'
1120 (exp_args, _) = tcSplitFunTys exp_ty''
1121 (act_args, _) = tcSplitFunTys act_ty''
1123 len_act_args = length act_args
1124 len_exp_args = length exp_args
1126 message = case orig of
1128 | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
1129 | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
1130 _ -> mkExpectedActualMsg act_ty'' exp_ty''
1131 ; return (env2, message) }
1134 %************************************************************************
1138 %************************************************************************
1140 Unifying kinds is much, much simpler than unifying types.
1143 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1144 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1146 matchExpectedFunKind (TyVarTy kvar) = do
1147 maybe_kind <- readKindVar kvar
1149 Indirect fun_kind -> matchExpectedFunKind fun_kind
1151 do { arg_kind <- newKindVar
1152 ; res_kind <- newKindVar
1153 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1154 ; return (Just (arg_kind,res_kind)) }
1156 matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
1157 matchExpectedFunKind _ = return Nothing
1160 unifyKind :: TcKind -- Expected
1164 unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
1165 | isSubKindCon kc2 kc1 = return ()
1167 unifyKind (FunTy a1 r1) (FunTy a2 r2)
1168 = do { unifyKind a2 a1; unifyKind r1 r2 }
1169 -- Notice the flip in the argument,
1170 -- so that the sub-kinding works right
1171 unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
1172 unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
1173 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1176 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1177 uKVar swapped kv1 k2
1178 = do { mb_k1 <- readKindVar kv1
1180 Flexi -> uUnboundKVar swapped kv1 k2
1181 Indirect k1 | swapped -> unifyKind k2 k1
1182 | otherwise -> unifyKind k1 k2 }
1185 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1186 uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
1187 | kv1 == kv2 = return ()
1188 | otherwise -- Distinct kind variables
1189 = do { mb_k2 <- readKindVar kv2
1191 Indirect k2 -> uUnboundKVar swapped kv1 k2
1192 Flexi -> writeKindVar kv1 k2 }
1194 uUnboundKVar swapped kv1 non_var_k2
1195 = do { k2' <- zonkTcKind non_var_k2
1196 ; kindOccurCheck kv1 k2'
1197 ; k2'' <- kindSimpleKind swapped k2'
1198 -- KindVars must be bound only to simple kinds
1199 -- Polarities: (kindSimpleKind True ?) succeeds
1200 -- returning *, corresponding to unifying
1203 ; writeKindVar kv1 k2'' }
1206 kindOccurCheck :: TyVar -> Type -> TcM ()
1207 kindOccurCheck kv1 k2 -- k2 is zonked
1208 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1210 not_in (TyVarTy kv2) = kv1 /= kv2
1211 not_in (FunTy a2 r2) = not_in a2 && not_in r2
1214 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1215 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1216 -- If the flag is False, it requires k <: sk
1217 -- E.g. kindSimpleKind False ?? = *
1218 -- What about (kv -> *) ~ ?? -> *
1219 kindSimpleKind orig_swapped orig_kind
1220 = go orig_swapped orig_kind
1222 go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
1224 ; return (mkArrowKind k1' k2') }
1226 | isOpenTypeKind k = return liftedTypeKind
1227 | isArgTypeKind k = return liftedTypeKind
1229 | isLiftedTypeKind k = return liftedTypeKind
1230 | isUnliftedTypeKind k = return unliftedTypeKind
1231 go _ k@(TyVarTy _) = return k -- KindVars are always simple
1232 go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")
1233 <+> ppr orig_swapped <+> ppr orig_kind)
1234 -- I think this can't actually happen
1236 -- T v = MkT v v must be a type
1237 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1239 unifyKindMisMatch :: TcKind -> TcKind -> TcM ()
1240 unifyKindMisMatch ty1 ty2 = do
1241 ty1' <- zonkTcKind ty1
1242 ty2' <- zonkTcKind ty2
1244 msg = hang (ptext (sLit "Couldn't match kind"))
1245 2 (sep [quotes (ppr ty1'),
1246 ptext (sLit "against"),
1251 kindOccurCheckErr :: Var -> Type -> SDoc
1252 kindOccurCheckErr tyvar ty
1253 = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
1254 2 (sep [ppr tyvar, char '=', ppr ty])
1257 %************************************************************************
1259 \subsection{Checking signature type variables}
1261 %************************************************************************
1263 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1264 are not mentioned in the environment. In particular:
1266 (a) Not mentioned in the type of a variable in the envt
1267 eg the signature for f in this:
1273 Here, f is forced to be monorphic by the free occurence of x.
1275 (d) Not (unified with another type variable that is) in scope.
1276 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1277 when checking the expression type signature, we find that
1278 even though there is nothing in scope whose type mentions r,
1279 nevertheless the type signature for the expression isn't right.
1281 Another example is in a class or instance declaration:
1283 op :: forall b. a -> b
1285 Here, b gets unified with a
1287 Before doing this, the substitution is applied to the signature type variable.
1290 checkSigTyVars :: [TcTyVar] -> TcM ()
1291 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1293 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1294 -- The extra_tvs can include boxy type variables;
1295 -- e.g. TcMatches.tcCheckExistentialPat
1296 checkSigTyVarsWrt extra_tvs sig_tvs
1297 = do { extra_tvs' <- zonkTcTyVarsAndFV extra_tvs
1298 ; check_sig_tyvars extra_tvs' sig_tvs }
1301 :: TcTyVarSet -- Global type variables. The universally quantified
1302 -- tyvars should not mention any of these
1303 -- Guaranteed already zonked.
1304 -> [TcTyVar] -- Universally-quantified type variables in the signature
1305 -- Guaranteed to be skolems
1307 check_sig_tyvars _ []
1309 check_sig_tyvars extra_tvs sig_tvs
1310 = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )
1311 do { gbl_tvs <- tcGetGlobalTyVars
1312 ; traceTc "check_sig_tyvars" $ vcat
1313 [ text "sig_tys" <+> ppr sig_tvs
1314 , text "gbl_tvs" <+> ppr gbl_tvs
1315 , text "extra_tvs" <+> ppr extra_tvs]
1317 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1318 ; when (any (`elemVarSet` env_tvs) sig_tvs)
1319 (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1322 bleatEscapedTvs :: TcTyVarSet -- The global tvs
1323 -> [TcTyVar] -- The possibly-escaping type variables
1324 -> [TcTyVar] -- The zonked versions thereof
1326 -- Complain about escaping type variables
1327 -- We pass a list of type variables, at least one of which
1328 -- escapes. The first list contains the original signature type variable,
1329 -- while the second contains the type variable it is unified to (usually itself)
1330 bleatEscapedTvs globals sig_tvs zonked_tvs
1331 = do { env0 <- tcInitTidyEnv
1332 ; let (env1, tidy_tvs) = tidyOpenTyVars env0 sig_tvs
1333 (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1335 ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1336 ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1338 main_msg = ptext (sLit "Inferred type is less polymorphic than expected")
1340 check (tidy_env, msgs) (sig_tv, zonked_tv)
1341 | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1343 = do { lcl_env <- getLclTypeEnv
1344 ; (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) lcl_env tidy_env
1345 ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1347 -----------------------
1348 escape_msg :: Var -> Var -> [SDoc] -> SDoc
1349 escape_msg sig_tv zonked_tv globs
1351 = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],
1352 nest 2 (vcat globs)]
1354 = msg <+> ptext (sLit "escapes")
1355 -- Sigh. It's really hard to give a good error message
1356 -- all the time. One bad case is an existential pattern match.
1357 -- We rely on the "When..." context to help.
1359 msg = ptext (sLit "Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1361 | sig_tv == zonked_tv = empty
1362 | otherwise = ptext (sLit "is unified with") <+> quotes (ppr zonked_tv) <+> ptext (sLit "which")
1365 These two context are used with checkSigTyVars
1368 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1369 -> TidyEnv -> TcM (TidyEnv, Message)
1370 sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do
1371 actual_tau <- zonkTcType sig_tau
1373 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1374 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1375 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1376 sub_msg = vcat [ptext (sLit "Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1377 ptext (sLit "Type to generalise:") <+> pprType tidy_actual_tau
1379 msg = vcat [ptext (sLit "When trying to generalise the type inferred for") <+> quotes (ppr id),