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,
18 typeExtraInfoMsg, emitMisMatchErr,
20 --------------------------------
23 matchExpectedListTy, matchExpectedPArrTy,
24 matchExpectedTyConApp, matchExpectedAppTy,
25 matchExpectedFunTys, matchExpectedFunKind,
29 #include "HsVersions.h"
34 import TcErrors ( typeExtraInfoMsg )
60 %************************************************************************
62 matchExpected functions
64 %************************************************************************
66 Note [Herald for matchExpectedFunTys]
67 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68 The 'herald' always looks like:
69 "The equation(s) for 'f' have"
70 "The abstraction (\x.e) takes"
71 "The section (+ x) expects"
72 "The function 'f' is applied to"
74 This is used to construct a message of form
76 The abstraction `\Just 1 -> ...' takes two arguments
77 but its type `Maybe a -> a' has only one
79 The equation(s) for `f' have two arguments
80 but its type `Maybe a -> a' has only one
82 The section `(f 3)' requires 'f' to take two arguments
83 but its type `Int -> Int' has only one
85 The function 'f' is applied to two arguments
86 but its type `Int -> Int' has only one
88 Note [matchExpectedFunTys]
89 ~~~~~~~~~~~~~~~~~~~~~~~~~~
90 matchExpectedFunTys checks that an (Expected rho) has the form
91 of an n-ary function. It passes the decomposed type to the
92 thing_inside, and returns a wrapper to coerce between the two types
94 It's used wherever a language construct must have a functional type,
100 This is not (currently) where deep skolemisation occurs;
101 matchExpectedFunTys does not skolmise nested foralls in the
102 expected type, becuase it expects that to have been done already
106 matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
109 -> TcM (CoercionI, [TcSigmaType], TcRhoType)
111 -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
112 -- then co : ty ~ (t1 -> ... -> tn -> ty_r)
114 -- Does not allocate unnecessary meta variables: if the input already is
115 -- a function, we just take it apart. Not only is this efficient,
116 -- it's important for higher rank: the argument might be of form
117 -- (forall a. ty) -> other
118 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
119 -- hide the forall inside a meta-variable
121 matchExpectedFunTys herald arity orig_ty
124 -- If go n ty = (co, [t1,..,tn], ty_r)
125 -- then co : ty ~ t1 -> .. -> tn -> ty_r
128 | n_req == 0 = return (IdCo ty, [], ty)
131 | Just ty' <- tcView ty = go n_req ty'
133 go n_req (FunTy arg_ty res_ty)
134 | not (isPredTy arg_ty)
135 = do { (coi, tys, ty_r) <- go (n_req-1) res_ty
136 ; return (mkFunTyCoI (IdCo arg_ty) coi, arg_ty:tys, ty_r) }
138 go _ (TyConApp tc _) -- A common case
139 | not (isSynFamilyTyCon tc)
140 = do { (env,msg) <- mk_ctxt emptyTidyEnv
141 ; failWithTcM (env,msg) }
143 go n_req ty@(TyVarTy tv)
144 | ASSERT( isTcTyVar tv) isMetaTyVar tv
145 = do { cts <- readMetaTyVar tv
147 Indirect ty' -> go n_req ty'
148 Flexi -> defer n_req ty }
150 -- In all other cases we bale out into ordinary unification
151 go n_req ty = defer n_req ty
155 = addErrCtxtM mk_ctxt $
156 do { arg_tys <- newFlexiTyVarTys n_req argTypeKind
157 ; res_ty <- newFlexiTyVarTy openTypeKind
158 ; coi <- unifyType fun_ty (mkFunTys arg_tys res_ty)
159 ; return (coi, arg_tys, res_ty) }
162 mk_ctxt :: TidyEnv -> TcM (TidyEnv, Message)
163 mk_ctxt env = do { orig_ty1 <- zonkTcType orig_ty
164 ; let (env', orig_ty2) = tidyOpenType env orig_ty1
165 (args, _) = tcSplitFunTys orig_ty2
166 n_actual = length args
167 ; return (env', mk_msg orig_ty2 n_actual) }
170 = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
171 sep [ptext (sLit "but its type") <+> quotes (pprType ty),
172 if n_args == 0 then ptext (sLit "has none")
173 else ptext (sLit "has only") <+> speakN n_args]
178 ----------------------
179 matchExpectedListTy :: TcRhoType -> TcM (CoercionI, TcRhoType)
180 -- Special case for lists
181 matchExpectedListTy exp_ty
182 = do { (coi, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
183 ; return (coi, elt_ty) }
185 ----------------------
186 matchExpectedPArrTy :: TcRhoType -> TcM (CoercionI, TcRhoType)
187 -- Special case for parrs
188 matchExpectedPArrTy exp_ty
189 = do { (coi, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
190 ; return (coi, elt_ty) }
192 ----------------------
193 matchExpectedTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
194 -> TcRhoType -- orig_ty
195 -> TcM (CoercionI, -- T a b c ~ orig_ty
196 [TcSigmaType]) -- Element types, a b c
198 -- It's used for wired-in tycons, so we call checkWiredInTyCon
199 -- Precondition: never called with FunTyCon
200 -- Precondition: input type :: *
202 matchExpectedTyConApp tc orig_ty
203 = do { checkWiredInTyCon tc
204 ; go (tyConArity tc) orig_ty [] }
206 go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (CoercionI, [TcSigmaType])
207 -- If go n ty tys = (co, [t1..tn] ++ tys)
208 -- then co : T t1..tn ~ ty
211 | Just ty' <- tcView ty = go n_req ty' tys
213 go n_req ty@(TyVarTy tv) tys
214 | ASSERT( isTcTyVar tv) isMetaTyVar tv
215 = do { cts <- readMetaTyVar tv
217 Indirect ty -> go n_req ty tys
218 Flexi -> defer n_req ty tys }
220 go n_req ty@(TyConApp tycon args) tys
222 = ASSERT( n_req == length args) -- ty::*
223 return (IdCo ty, args ++ tys)
225 go n_req (AppTy fun arg) tys
227 = do { (coi, args) <- go (n_req - 1) fun (arg : tys)
228 ; return (mkAppTyCoI coi (IdCo arg), args) }
230 go n_req ty tys = defer n_req ty tys
234 = do { tau_tys <- mapM newFlexiTyVarTy arg_kinds
235 ; coi <- unifyType (mkTyConApp tc tau_tys) ty
236 ; return (coi, tau_tys ++ tys) }
238 (arg_kinds, _) = splitKindFunTysN n_req (tyConKind tc)
240 ----------------------
241 matchExpectedAppTy :: TcRhoType -- orig_ty
242 -> TcM (CoercionI, -- m a ~ orig_ty
243 (TcSigmaType, TcSigmaType)) -- Returns m, a
244 -- If the incoming type is a mutable type variable of kind k, then
245 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
247 matchExpectedAppTy orig_ty
251 | Just ty' <- tcView ty = go ty'
253 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
254 = return (IdCo orig_ty, (fun_ty, arg_ty))
257 | ASSERT( isTcTyVar tv) isMetaTyVar tv
258 = do { cts <- readMetaTyVar tv
265 -- Defer splitting by generating an equality constraint
266 defer = do { ty1 <- newFlexiTyVarTy kind1
267 ; ty2 <- newFlexiTyVarTy kind2
268 ; coi <- unifyType (mkAppTy ty1 ty2) orig_ty
269 ; return (coi, (ty1, ty2)) }
271 orig_kind = typeKind orig_ty
272 kind1 = mkArrowKind liftedTypeKind (defaultKind orig_kind)
273 kind2 = liftedTypeKind -- m :: * -> k
275 -- The defaultKind is a bit smelly. If you remove it,
276 -- try compiling f x = do { x }
277 -- and you'll get a kind mis-match. It smells, but
278 -- not enough to lose sleep over.
282 %************************************************************************
286 %************************************************************************
288 All the tcSub calls have the form
290 tcSub actual_ty expected_ty
292 actual_ty <= expected_ty
294 That is, that a value of type actual_ty is acceptable in
295 a place expecting a value of type expected_ty.
297 It returns a coercion function
298 co_fn :: actual_ty ~ expected_ty
299 which takes an HsExpr of type actual_ty into one of type
303 tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
304 -- Check that ty_actual is more polymorphic than ty_expected
305 -- Both arguments might be polytypes, so we must instantiate and skolemise
306 -- Returns a wrapper of shape ty_actual ~ ty_expected
307 tcSubType origin skol_info ty_actual ty_expected
308 | isSigmaTy ty_actual
309 = do { let extra_tvs = tyVarsOfType ty_actual
310 ; (sk_wrap, inst_wrap)
311 <- tcGen skol_info extra_tvs ty_expected $ \ _ sk_rho -> do
312 { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
313 ; coi <- unifyType in_rho sk_rho
314 ; return (coiToHsWrapper coi <.> in_wrap) }
315 ; return (sk_wrap <.> inst_wrap) }
317 | otherwise -- Urgh! It seems deeply weird to have equality
318 -- when actual is not a polytype, and it makes a big
319 -- difference e.g. tcfail104
320 = do { coi <- unifyType ty_actual ty_expected
321 ; return (coiToHsWrapper coi) }
323 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
324 tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind
329 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
330 tcWrapResult expr actual_ty res_ty
331 = do { coi <- unifyType actual_ty res_ty
332 -- Both types are deeply skolemised
333 ; return (mkHsWrapCoI coi expr) }
335 -----------------------------------
337 :: [TcType] -- Type of args
338 -> HsWrapper -- HsExpr a -> HsExpr b
339 -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
340 wrapFunResCoercion arg_tys co_fn_res
341 | isIdHsWrapper co_fn_res
346 = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
347 ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
352 %************************************************************************
354 \subsection{Generalisation}
356 %************************************************************************
359 tcGen :: SkolemInfo -> TcTyVarSet -> TcType
360 -> ([TcTyVar] -> TcRhoType -> TcM result)
361 -> TcM (HsWrapper, result)
362 -- The expression has type: spec_ty -> expected_ty
364 tcGen skol_info extra_tvs
365 expected_ty thing_inside -- We expect expected_ty to be a forall-type
366 -- If not, the call is a no-op
367 = do { traceTc "tcGen" empty
368 ; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty
371 traceTc "tcGen" $ vcat [
372 text "expected_ty" <+> ppr expected_ty,
373 text "inst ty" <+> ppr tvs' <+> ppr rho' ]
375 -- In 'free_tvs' we must check that the "forall_tvs" havn't been constrained
376 -- The interesting bit here is that we must include the free variables
377 -- of the expected_ty. Here's an example:
378 -- runST (newVar True)
379 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
380 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
381 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
382 -- So now s' isn't unconstrained because it's linked to a.
383 -- Conclusion: pass the free vars of the expected_ty to checkConsraints
384 ; let free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
386 ; (ev_binds, result) <- checkConstraints skol_info free_tvs 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 -> TcTyVarSet -- Free variables (other than the type envt)
395 -- for the skolem escape check
396 -> [TcTyVar] -- Skolems
399 -> TcM (TcEvBinds, result)
401 checkConstraints skol_info free_tvs skol_tvs given thing_inside
402 | null skol_tvs && null given
403 = do { res <- thing_inside; return (emptyTcEvBinds, res) }
404 -- Just for efficiency. We check every function argument with
405 -- tcPolyExpr, which uses tcGen and hence checkConstraints.
408 = do { (ev_binds, wanted, result) <- newImplication skol_info free_tvs
409 skol_tvs given thing_inside
410 ; emitConstraints wanted
411 ; return (ev_binds, result) }
413 newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar]
414 -> [EvVar] -> TcM result
415 -> TcM (TcEvBinds, WantedConstraints, result)
416 newImplication skol_info free_tvs skol_tvs given thing_inside
417 = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
418 ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
419 do { gbl_tvs <- tcGetGlobalTyVars
420 ; lcl_env <- getLclTypeEnv
421 ; let all_free_tvs = gbl_tvs `unionVarSet` free_tvs
423 ; (result, wanted) <- getConstraints $
424 setUntouchables all_free_tvs $
427 ; if isEmptyBag wanted && not (hasEqualities given)
428 -- Optimisation : if there are no wanteds, and the givens
429 -- are sufficiently simple, don't generate an implication
430 -- at all. Reason for the hasEqualities test:
431 -- we don't want to lose the "inaccessible alternative"
434 return (emptyTcEvBinds, emptyWanteds, result)
436 { ev_binds_var <- newTcEvBinds
437 ; loc <- getCtLoc skol_info
438 ; let implic = Implic { ic_env_tvs = all_free_tvs
440 , ic_skols = mkVarSet skol_tvs
441 , ic_scoped = panic "emitImplication"
444 , ic_binds = ev_binds_var
447 ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } }
451 %************************************************************************
455 %************************************************************************
457 The exported functions are all defined as versions of some
458 non-exported generic functions.
462 unifyType :: TcTauType -> TcTauType -> TcM CoercionI
463 -- Actual and expected types
464 -- Returns a coercion : ty1 ~ ty2
465 unifyType ty1 ty2 = uType [] ty1 ty2
468 unifyPred :: PredType -> PredType -> TcM CoercionI
469 -- Actual and expected types
470 unifyPred p1 p2 = uPred [UnifyOrigin (mkPredTy p1) (mkPredTy p2)] p1 p2
473 unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
474 -- Actual and expected types
475 unifyTheta theta1 theta2
476 = do { checkTc (equalLength theta1 theta2)
477 (vcat [ptext (sLit "Contexts differ in length"),
478 nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
479 ; zipWithM unifyPred theta1 theta2 }
482 @unifyTypeList@ takes a single list of @TauType@s and unifies them
483 all together. It is used, for example, when typechecking explicit
484 lists, when all the elts should be of the same type.
487 unifyTypeList :: [TcTauType] -> TcM ()
488 unifyTypeList [] = return ()
489 unifyTypeList [_] = return ()
490 unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
491 ; unifyTypeList tys }
494 %************************************************************************
498 %************************************************************************
500 uType is the heart of the unifier. Each arg occurs twice, because
501 we want to report errors in terms of synomyms if possible. The first of
502 the pair is used in error messages only; it is always the same as the
503 second, except that if the first is a synonym then the second may be a
504 de-synonym'd version. This way we get better error messages.
508 = NotSwapped -- Args are: actual, expected
509 | IsSwapped -- Args are: expected, actual
511 instance Outputable SwapFlag where
512 ppr IsSwapped = ptext (sLit "Is-swapped")
513 ppr NotSwapped = ptext (sLit "Not-swapped")
515 unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
516 unSwap NotSwapped f a b = f a b
517 unSwap IsSwapped f a b = f b a
520 uType, uType_np, uType_defer
522 -> TcType -- ty1 is the *actual* type
523 -> TcType -- ty2 is the *expected* type
527 -- It is always safe to defer unification to the main constraint solver
528 -- See Note [Deferred unification]
529 uType_defer origin ty1 ty2
530 = do { co_var <- newWantedCoVar ty1 ty2
531 ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin])
532 ; loc <- getCtLoc TypeEqOrigin
533 ; wrapEqCtxt origin $
534 emitConstraint (WcEvVar (WantedEvVar co_var loc))
535 ; return $ ACo $ mkTyVarTy co_var }
538 -- Push a new item on the origin stack (the most common case)
539 uType origin ty1 ty2 -- Push a new item on the origin stack
540 = uType_np (pushOrigin ty1 ty2 origin) ty1 ty2
543 -- unify_np (short for "no push" on the origin stack) does the work
544 uType_np origin orig_ty1 orig_ty2
545 = do { traceTc "u_tys " $ vcat
546 [ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
548 ; coi <- go origin orig_ty1 orig_ty2
550 ACo co -> traceTc "u_tys yields coercion:" (ppr co)
551 IdCo _ -> traceTc "u_tys yields no coercion" empty
554 bale_out :: [EqOrigin] -> TcM a
555 bale_out origin = failWithMisMatch origin
557 go :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI
558 -- The arguments to 'go' are always semantically identical
559 -- to orig_ty{1,2} except for looking through type synonyms
561 -- Variables; go for uVar
562 -- Note that we pass in *original* (before synonym expansion),
563 -- so that type variables tend to get filled in with
564 -- the most informative version of the type
565 go origin (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2
566 go origin ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1
569 -- see Note [Unification and synonyms]
570 -- Do this after the variable case so that we tend to unify
571 -- variables with un-expended type synonym
573 | Just ty1' <- tcView ty1 = uType origin ty1' ty2
574 | Just ty2' <- tcView ty2 = uType origin ty1 ty2'
577 go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2
579 -- Functions; just check the two parts
580 go origin (FunTy fun1 arg1) (FunTy fun2 arg2)
581 = do { coi_l <- uType origin fun1 fun2
582 ; coi_r <- uType origin arg1 arg2
583 ; return $ mkFunTyCoI coi_l coi_r }
585 -- Always defer if a type synonym family (type function)
586 -- is involved. (Data families behave rigidly.)
587 go origin ty1@(TyConApp tc1 _) ty2
588 | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
589 go origin ty1 ty2@(TyConApp tc2 _)
590 | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
592 go origin (TyConApp tc1 tys1) (TyConApp tc2 tys2)
593 | tc1 == tc2 -- See Note [TyCon app]
594 = do { cois <- uList origin uType tys1 tys2
595 ; return $ mkTyConAppCoI tc1 cois }
597 -- See Note [Care with type applications]
598 go origin (AppTy s1 t1) ty2
599 | Just (s2,t2) <- tcSplitAppTy_maybe ty2
600 = do { coi_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy]
601 ; coi_t <- uType origin t1 t2
602 ; return $ mkAppTyCoI coi_s coi_t }
604 go origin ty1 (AppTy s2 t2)
605 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
606 = do { coi_s <- uType_np origin s1 s2
607 ; coi_t <- uType origin t1 t2
608 ; return $ mkAppTyCoI coi_s coi_t }
611 | isSigmaTy ty1 || isSigmaTy ty2
612 = unifySigmaTy origin ty1 ty2
614 -- Anything else fails
615 go origin _ _ = bale_out origin
617 unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI
618 unifySigmaTy origin ty1 ty2
619 = do { let (tvs1, body1) = tcSplitForAllTys ty1
620 (tvs2, body2) = tcSplitForAllTys ty2
621 ; unless (equalLength tvs1 tvs2) (failWithMisMatch origin)
622 ; skol_tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
623 -- Get location from monad, not from tvs1
624 ; let tys = mkTyVarTys skol_tvs
625 in_scope = mkInScopeSet (mkVarSet skol_tvs)
626 phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
627 phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
628 untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
630 ; (coi, lie) <- getConstraints $
631 setUntouchables untch $
632 uType origin phi1 phi2
634 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
635 ; let bad_lie = filterBag is_bad lie
636 is_bad w = any (`elemVarSet` tyVarsOfWanted w) skol_tvs
637 ; when (not (isEmptyBag bad_lie))
638 (failWithMisMatch origin) -- ToDo: give details from bad_lie
640 ; emitConstraints lie
641 ; return (foldr mkForAllTyCoI coi skol_tvs) }
644 uPred :: [EqOrigin] -> PredType -> PredType -> TcM CoercionI
645 uPred origin (IParam n1 t1) (IParam n2 t2)
647 = do { coi <- uType origin t1 t2
648 ; return $ mkIParamPredCoI n1 coi }
649 uPred origin (ClassP c1 tys1) (ClassP c2 tys2)
651 = do { cois <- uList origin uType tys1 tys2
652 -- Guaranteed equal lengths because the kinds check
653 ; return $ mkClassPPredCoI c1 cois }
654 uPred origin (EqPred ty1a ty1b) (EqPred ty2a ty2b)
655 = do { coia <- uType origin ty1a ty2a
656 ; coib <- uType origin ty1b ty2b
657 ; return $ mkEqPredCoI coia coib }
659 uPred origin _ _ = failWithMisMatch origin
663 -> ([EqOrigin] -> a -> a -> TcM b)
664 -> [a] -> [a] -> TcM [b]
665 -- Unify corresponding elements of two lists of types, which
666 -- should be of equal length. We charge down the list explicitly so that
667 -- we can complain if their lengths differ.
668 uList _ _ [] [] = return []
669 uList origin unify (ty1:tys1) (ty2:tys2) = do { x <- unify origin ty1 ty2;
670 ; xs <- uList origin unify tys1 tys2
672 uList origin _ _ _ = failWithMisMatch origin
673 -- See Note [Mismatched type lists and application decomposition]
677 Note [Care with type applications]
678 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679 Note: type applications need a bit of care!
680 They can match FunTy and TyConApp, so use splitAppTy_maybe
681 NB: we've already dealt with type variables and Notes,
682 so if one type is an App the other one jolly well better be too
684 Note [Unifying AppTy]
685 ~~~~~~~~~~~~~~~~~~~~~
686 Considerm unifying (m Int) ~ (IO Int) where m is a unification variable
687 that is now bound to (say) (Bool ->). Then we want to report
688 "Can't unify (Bool -> Int) with (IO Int)
690 "Can't unify ((->) Bool) with IO"
691 That is why we use the "_np" variant of uType, which does not alter the error
696 When we find two TyConApps, the argument lists are guaranteed equal
697 length. Reason: intially the kinds of the two types to be unified is
698 the same. The only way it can become not the same is when unifying two
699 AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
700 the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
701 which we do, that ensures that f1,f2 have the same kind; and that
702 means a1,a2 have the same kind. And now the argument repeats.
704 Note [Mismatched type lists and application decomposition]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 When we find two TyConApps, you might think that the argument lists
707 are guaranteed equal length. But they aren't. Consider matching
708 w (T x) ~ Foo (T x y)
709 We do match (w ~ Foo) first, but in some circumstances we simply create
710 a deferred constraint; and then go ahead and match (T x ~ T x y).
711 This came up in Trac #3950.
714 (a) either we must check for identical argument kinds
715 when decomposing applications,
717 (b) or we must be prepared for ill-kinded unification sub-problems
719 Currently we adopt (b) since it seems more robust -- no need to maintain
722 Note [Unification and synonyms]
723 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
724 If you are tempted to make a short cut on synonyms, as in this
727 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
728 = if (con1 == con2) then
729 -- Good news! Same synonym constructors, so we can shortcut
730 -- by unifying their arguments and ignoring their expansions.
731 unifyTypepeLists args1 args2
733 -- Never mind. Just expand them and try again
736 then THINK AGAIN. Here is the whole story, as detected and reported
739 Here's a test program that should detect the problem:
742 x = (1 :: Bogus Char) :: Bogus Bool
744 The problem with [the attempted shortcut code] is that
748 is not a sufficient condition to be able to use the shortcut!
749 You also need to know that the type synonym actually USES all
750 its arguments. For example, consider the following type synonym
751 which does not use all its arguments.
755 If you ever tried unifying, say, (Bogus Char) with )Bogus Bool), the
756 unifier would blithely try to unify Char with Bool and would fail,
757 even though the expanded forms (both Int) should match. Similarly,
758 unifying (Bogus Char) with (Bogus t) would unnecessarily bind t to
761 ... You could explicitly test for the problem synonyms and mark them
762 somehow as needing expansion, perhaps also issuing a warning to the
765 Note [Deferred Unification]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
768 and yet its consistency is undetermined. Previously, there was no way to still
769 make it consistent. So a mismatch error was issued.
771 Now these unfications are deferred until constraint simplification, where type
772 family instances and given equations may (or may not) establish the consistency.
773 Deferred unifications are of the form
776 where F is a type function and x is a type variable.
778 id :: x ~ y => x -> y
781 involves the unfication x = y. It is deferred until we bring into account the
782 context x ~ y to establish that it holds.
784 If available, we defer original types (rather than those where closed type
785 synonyms have already been expanded via tcCoreView). This is, as usual, to
786 improve error messages.
789 %************************************************************************
793 %************************************************************************
795 @uVar@ is called when at least one of the types being unified is a
796 variable. It does {\em not} assume that the variable is a fixed point
797 of the substitution; rather, notice that @uVar@ (defined below) nips
798 back into @uTys@ if it turns out that the variable is already bound.
801 uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM CoercionI
802 uVar origin swapped tv1 ty2
803 = do { traceTc "uVar" (vcat [ ppr origin
805 , ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
806 , nest 2 (ptext (sLit " ~ "))
807 , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)])
808 ; details <- lookupTcTyVar tv1
810 Filled ty1 -> unSwap swapped (uType_np origin) ty1 ty2
811 Unfilled details1 -> uUnfilledVar origin swapped tv1 details1 ty2
815 uUnfilledVar :: [EqOrigin]
817 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
818 -> TcTauType -- Type 2
820 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
821 -- It might be a skolem, or untouchable, or meta
823 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
824 | tv1 == tv2 -- Same type variable => no-op
825 = return (IdCo (mkTyVarTy tv1))
827 | otherwise -- Distinct type variables
828 = do { lookup2 <- lookupTcTyVar tv2
830 Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
831 Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
834 uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type variable
837 -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
839 Nothing -> do { traceTc "Occ/kind defer" (ppr tv1); defer }
840 Just ty2' -> updateMeta tv1 ref1 ty2'
843 _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
845 defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
846 -- Occurs check or an untouchable: just defer
847 -- NB: occurs check isn't necessarily fatal:
848 -- eg tv1 occured in type family parameter
851 uUnfilledVars :: [EqOrigin]
853 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
854 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
856 -- Invarant: The type variables are distinct,
857 -- Neither is filled in yet
859 uUnfilledVars origin swapped tv1 details1 tv2 details2
860 = case (details1, details2) of
861 (MetaTv i1 ref1, MetaTv i2 ref2)
862 | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1 i1 i2
863 then updateMeta tv1 ref1 ty2
864 else updateMeta tv2 ref2 ty1
865 | k2_sub_k1 -> updateMeta tv1 ref1 ty2
867 (_, MetaTv _ ref2) | k1_sub_k2 -> updateMeta tv2 ref2 ty1
868 (MetaTv _ ref1, _) | k2_sub_k1 -> updateMeta tv1 ref1 ty2
870 (_, _) -> unSwap swapped (uType_defer origin) ty1 ty2
871 -- Defer for skolems of all sorts
875 k1_sub_k2 = k1 `isSubKind` k2
876 k2_sub_k1 = k2 `isSubKind` k1
880 nicer_to_update_tv1 _ (SigTv _) = True
881 nicer_to_update_tv1 (SigTv _) _ = False
882 nicer_to_update_tv1 _ _ = isSystemName (Var.varName tv1)
883 -- Try not to update SigTvs; and try to update sys-y type
884 -- variables in preference to ones gotten (say) by
885 -- instantiating a polymorphic function with a user-written
889 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
890 -- (checkTauTvUpdate tv ty)
891 -- We are about to update the TauTv tv with ty.
892 -- Check (a) that tv doesn't occur in ty (occurs check)
893 -- (b) that ty is a monotype
894 -- (c) that kind(ty) is a sub-kind of kind(tv)
896 -- We have two possible outcomes:
897 -- (1) Return the type to update the type variable with,
898 -- [we know the update is ok]
899 -- (2) Return Nothing,
900 -- [the update might be dodgy]
902 -- Note that "Nothing" does not mean "definite error". For example
904 -- type instance F Int = Int
907 -- This is perfectly reasonable, if we later get a ~ Int. For now, though,
908 -- we return Nothing, leaving it to the later constraint simplifier to
911 checkTauTvUpdate tv ty
912 = do { ty' <- zonkTcType ty
913 ; if not (tv `elemVarSet` tyVarsOfType ty')
914 && typeKind ty' `isSubKind` tyVarKind tv
915 then return (Just ty')
916 else return Nothing }
921 data LookupTyVarResult -- The result of a lookupTcTyVar call
922 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
925 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
927 | MetaTv _ ref <- details
928 = do { meta_details <- readMutVar ref
929 ; case meta_details of
930 Indirect ty -> return (Filled ty)
931 Flexi -> do { is_untch <- isUntouchable tyvar
932 ; let -- Note [Unifying untouchables]
933 ret_details | is_untch = SkolemTv UnkSkol
934 | otherwise = details
935 ; return (Unfilled ret_details) } }
937 = return (Unfilled details)
939 details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
942 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM CoercionI
943 updateMeta tv1 ref1 ty2
944 = do { writeMetaTyVarRef tv1 ref1 ty2
945 ; return (IdCo ty2) }
948 Note [Unifying untouchables]
949 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
950 We treat an untouchable type variable as if it was a skolem. That
951 ensures it won't unify with anything. It's a slight had, because
952 we return a made-up TcTyVarDetails, but I think it works smoothly.
955 %************************************************************************
959 %************************************************************************
962 pushOrigin :: TcType -> TcType -> [EqOrigin] -> [EqOrigin]
963 pushOrigin ty_act ty_exp origin
964 = UnifyOrigin { uo_actual = ty_act, uo_expected = ty_exp } : origin
967 wrapEqCtxt :: [EqOrigin] -> TcM a -> TcM a
968 -- Build a suitable error context from the origin and do the thing inside
969 -- The "couldn't match" error comes from the innermost item on the stack,
970 -- and, if there is more than one item, the "Expected/inferred" part
971 -- comes from the outermost item
972 wrapEqCtxt [] thing_inside = thing_inside
973 wrapEqCtxt [_] thing_inside = thing_inside
974 wrapEqCtxt items thing_inside = addErrCtxtM (unifyCtxt (last items)) thing_inside
977 failWithMisMatch :: [EqOrigin] -> TcM a
978 -- Generate the message when two types fail to match,
979 -- going to some trouble to make it helpful.
980 -- The argument order is: actual type, expected type
982 = panic "failWithMisMatch"
983 failWithMisMatch origin@(item:_)
984 = wrapEqCtxt origin $
985 emitMisMatchErr (uo_actual item) (uo_expected item)
987 mkExpectedActualMsg :: Type -> Type -> SDoc
988 mkExpectedActualMsg act_ty exp_ty
989 = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
990 text " Actual type" <> colon <+> ppr act_ty ])
992 emitMisMatchErr :: TcType -> TcType -> TcM a
993 emitMisMatchErr ty_act ty_exp
994 = do { ty_act <- zonkTcType ty_act
995 ; ty_exp <- zonkTcType ty_exp
996 ; env0 <- tcInitTidyEnv
997 ; let (env1, pp_exp) = tidyOpenType env0 ty_exp
998 (env2, pp_act) = tidyOpenType env1 ty_act
999 ; failWithTcM (misMatchMsg env2 pp_act pp_exp) }
1001 misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc)
1002 misMatchMsg env ty_act ty_exp
1003 = (env2, sep [sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp)
1004 , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)]
1005 , nest 2 (extra1 $$ extra2) ])
1007 (env1, extra1) = typeExtraInfoMsg env ty_exp
1008 (env2, extra2) = typeExtraInfoMsg env1 ty_act
1010 --------------------
1011 unifyCtxt :: EqOrigin -> TidyEnv -> TcM (TidyEnv, SDoc)
1012 unifyCtxt (UnifyOrigin { uo_actual = act_ty, uo_expected = exp_ty }) tidy_env
1013 = do { act_ty' <- zonkTcType act_ty
1014 ; exp_ty' <- zonkTcType exp_ty
1015 ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1016 (env2, act_ty'') = tidyOpenType env1 act_ty'
1017 ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
1021 -----------------------------------------
1023 -----------------------------------------
1027 -- If an error happens we try to figure out whether the function
1028 -- function has been given too many or too few arguments, and say so.
1029 addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
1030 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
1031 = addErrCtxtM mk_err thing_inside
1034 = do { exp_ty' <- zonkTcType expected_res_ty
1035 ; act_ty' <- zonkTcType actual_res_ty
1036 ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1037 (env2, act_ty'') = tidyOpenType env1 act_ty'
1038 (exp_args, _) = tcSplitFunTys exp_ty''
1039 (act_args, _) = tcSplitFunTys act_ty''
1041 len_act_args = length act_args
1042 len_exp_args = length exp_args
1044 message = case orig of
1046 | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
1047 | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
1048 _ -> mkExpectedActualMsg act_ty'' exp_ty''
1049 ; return (env2, message) }
1052 %************************************************************************
1056 %************************************************************************
1058 Unifying kinds is much, much simpler than unifying types.
1061 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1062 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1064 matchExpectedFunKind (TyVarTy kvar) = do
1065 maybe_kind <- readKindVar kvar
1067 Indirect fun_kind -> matchExpectedFunKind fun_kind
1069 do { arg_kind <- newKindVar
1070 ; res_kind <- newKindVar
1071 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1072 ; return (Just (arg_kind,res_kind)) }
1074 matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
1075 matchExpectedFunKind _ = return Nothing
1078 unifyKind :: TcKind -- Expected
1082 unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
1083 | isSubKindCon kc2 kc1 = return ()
1085 unifyKind (FunTy a1 r1) (FunTy a2 r2)
1086 = do { unifyKind a2 a1; unifyKind r1 r2 }
1087 -- Notice the flip in the argument,
1088 -- so that the sub-kinding works right
1089 unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
1090 unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
1091 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1094 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1095 uKVar swapped kv1 k2
1096 = do { mb_k1 <- readKindVar kv1
1098 Flexi -> uUnboundKVar swapped kv1 k2
1099 Indirect k1 | swapped -> unifyKind k2 k1
1100 | otherwise -> unifyKind k1 k2 }
1103 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1104 uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
1105 | kv1 == kv2 = return ()
1106 | otherwise -- Distinct kind variables
1107 = do { mb_k2 <- readKindVar kv2
1109 Indirect k2 -> uUnboundKVar swapped kv1 k2
1110 Flexi -> writeKindVar kv1 k2 }
1112 uUnboundKVar swapped kv1 non_var_k2
1113 = do { k2' <- zonkTcKind non_var_k2
1114 ; kindOccurCheck kv1 k2'
1115 ; k2'' <- kindSimpleKind swapped k2'
1116 -- KindVars must be bound only to simple kinds
1117 -- Polarities: (kindSimpleKind True ?) succeeds
1118 -- returning *, corresponding to unifying
1121 ; writeKindVar kv1 k2'' }
1124 kindOccurCheck :: TyVar -> Type -> TcM ()
1125 kindOccurCheck kv1 k2 -- k2 is zonked
1126 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1128 not_in (TyVarTy kv2) = kv1 /= kv2
1129 not_in (FunTy a2 r2) = not_in a2 && not_in r2
1132 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1133 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1134 -- If the flag is False, it requires k <: sk
1135 -- E.g. kindSimpleKind False ?? = *
1136 -- What about (kv -> *) ~ ?? -> *
1137 kindSimpleKind orig_swapped orig_kind
1138 = go orig_swapped orig_kind
1140 go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
1142 ; return (mkArrowKind k1' k2') }
1144 | isOpenTypeKind k = return liftedTypeKind
1145 | isArgTypeKind k = return liftedTypeKind
1147 | isLiftedTypeKind k = return liftedTypeKind
1148 | isUnliftedTypeKind k = return unliftedTypeKind
1149 go _ k@(TyVarTy _) = return k -- KindVars are always simple
1150 go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")
1151 <+> ppr orig_swapped <+> ppr orig_kind)
1152 -- I think this can't actually happen
1154 -- T v = MkT v v must be a type
1155 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1157 unifyKindMisMatch :: TcKind -> TcKind -> TcM ()
1158 unifyKindMisMatch ty1 ty2 = do
1159 ty1' <- zonkTcKind ty1
1160 ty2' <- zonkTcKind ty2
1162 msg = hang (ptext (sLit "Couldn't match kind"))
1163 2 (sep [quotes (ppr ty1'),
1164 ptext (sLit "against"),
1169 kindOccurCheckErr :: Var -> Type -> SDoc
1170 kindOccurCheckErr tyvar ty
1171 = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
1172 2 (sep [ppr tyvar, char '=', ppr ty])
1175 %************************************************************************
1177 \subsection{Checking signature type variables}
1179 %************************************************************************
1181 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1182 are not mentioned in the environment. In particular:
1184 (a) Not mentioned in the type of a variable in the envt
1185 eg the signature for f in this:
1191 Here, f is forced to be monorphic by the free occurence of x.
1193 (d) Not (unified with another type variable that is) in scope.
1194 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1195 when checking the expression type signature, we find that
1196 even though there is nothing in scope whose type mentions r,
1197 nevertheless the type signature for the expression isn't right.
1199 Another example is in a class or instance declaration:
1201 op :: forall b. a -> b
1203 Here, b gets unified with a
1205 Before doing this, the substitution is applied to the signature type variable.
1208 checkSigTyVars :: [TcTyVar] -> TcM ()
1209 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1211 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1212 -- The extra_tvs can include boxy type variables;
1213 -- e.g. TcMatches.tcCheckExistentialPat
1214 checkSigTyVarsWrt extra_tvs sig_tvs
1215 = do { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
1216 ; check_sig_tyvars extra_tvs' sig_tvs }
1219 :: TcTyVarSet -- Global type variables. The universally quantified
1220 -- tyvars should not mention any of these
1221 -- Guaranteed already zonked.
1222 -> [TcTyVar] -- Universally-quantified type variables in the signature
1223 -- Guaranteed to be skolems
1225 check_sig_tyvars _ []
1227 check_sig_tyvars extra_tvs sig_tvs
1228 = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )
1229 do { gbl_tvs <- tcGetGlobalTyVars
1230 ; traceTc "check_sig_tyvars" $ vcat
1231 [ text "sig_tys" <+> ppr sig_tvs
1232 , text "gbl_tvs" <+> ppr gbl_tvs
1233 , text "extra_tvs" <+> ppr extra_tvs]
1235 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1236 ; when (any (`elemVarSet` env_tvs) sig_tvs)
1237 (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1240 bleatEscapedTvs :: TcTyVarSet -- The global tvs
1241 -> [TcTyVar] -- The possibly-escaping type variables
1242 -> [TcTyVar] -- The zonked versions thereof
1244 -- Complain about escaping type variables
1245 -- We pass a list of type variables, at least one of which
1246 -- escapes. The first list contains the original signature type variable,
1247 -- while the second contains the type variable it is unified to (usually itself)
1248 bleatEscapedTvs globals sig_tvs zonked_tvs
1249 = do { env0 <- tcInitTidyEnv
1250 ; let (env1, tidy_tvs) = tidyOpenTyVars env0 sig_tvs
1251 (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1253 ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1254 ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1256 main_msg = ptext (sLit "Inferred type is less polymorphic than expected")
1258 check (tidy_env, msgs) (sig_tv, zonked_tv)
1259 | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1261 = do { lcl_env <- getLclTypeEnv
1262 ; (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) lcl_env tidy_env
1263 ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1265 -----------------------
1266 escape_msg :: Var -> Var -> [SDoc] -> SDoc
1267 escape_msg sig_tv zonked_tv globs
1269 = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],
1270 nest 2 (vcat globs)]
1272 = msg <+> ptext (sLit "escapes")
1273 -- Sigh. It's really hard to give a good error message
1274 -- all the time. One bad case is an existential pattern match.
1275 -- We rely on the "When..." context to help.
1277 msg = ptext (sLit "Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1279 | sig_tv == zonked_tv = empty
1280 | otherwise = ptext (sLit "is unified with") <+> quotes (ppr zonked_tv) <+> ptext (sLit "which")
1283 These two context are used with checkSigTyVars
1286 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1287 -> TidyEnv -> TcM (TidyEnv, Message)
1288 sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do
1289 actual_tau <- zonkTcType sig_tau
1291 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1292 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1293 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1294 sub_msg = vcat [ptext (sLit "Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1295 ptext (sLit "Type to generalise:") <+> pprType tidy_actual_tau
1297 msg = vcat [ptext (sLit "When trying to generalise the type inferred for") <+> quotes (ppr id),