\begin{code}
module TcUnify (
-- Full-blown subsumption
- tcSubPat, tcSubExp, tcGen,
- checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
+ tcSubPat, tcSubExp, tcSub, tcGen,
+ checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
- unifyTauTy, unifyTauTyList,
+ unifyTauTy, unifyTauTyList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
checkExpectedKind,
#include "HsVersions.h"
--- gaw 2004
import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats )
import TcHsSyn ( mkHsLet, mkHsDictLam,
ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
import TcRnMonad -- TcType, amongst others
import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
- TcTyVarSet, TcThetaType, Expected(..),
+ TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
SkolemInfo( GenSkol ), MetaDetails(..),
- pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
+ pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
- tyVarsOfType, mkPhiTy, mkTyVarTy,
+ tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
- pprType, isSkolemTyVar )
+ pprType, tidySkolemTyVar, isSkolemTyVar )
import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
- openTypeKind, liftedTypeKind, mkArrowKind, kindFunResult,
+ openTypeKind, liftedTypeKind, mkArrowKind,
isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
isSubKind, pprKind, splitKindFunTys )
import Inst ( newDicts, instToId, tcInstCall )
import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
- putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
- newTyFlexiVarTy, zonkTcKind,
- zonkType, zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV,
+ tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
+ newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
+import TcIface ( checkWiredInTyCon )
import TcEnv ( tcGetGlobalTyVars, findGlobals )
import TyCon ( TyCon, tyConArity, tyConTyVars )
import TysWiredIn ( listTyCon )
import Id ( Id, mkSysLocal )
import Var ( Var, varName, tyVarKind )
-import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet,
- varSetElems, intersectsVarSet, mkVarSet )
+import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
import VarEnv
import Name ( isSystemName, mkSysTvName )
import ErrUtils ( Message )
import SrcLoc ( noLoc )
import BasicTypes ( Arity )
-import Util ( notNull )
+import Util ( notNull, equalLength )
import Outputable
\end{code}
-> Expected TcSigmaType -- Expected type (T a b c)
-> TcM [TcType] -- Element types, a b c
-- Insists that the Expected type is not a forall-type
-
+ -- It's used for wired-in tycons, so we call checkWiredInTyCOn
zapToTyConApp tc (Check ty)
- = unifyTyConApp tc ty -- NB: fails for a forall-type
+ = do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type
+
zapToTyConApp tc (Infer hole)
= do { (tc_app, elt_tys) <- newTyConApp tc
; writeMutVar hole tc_app
+ ; traceTc (text "zap" <+> ppr tc)
+ ; checkWiredInTyCon tc
; return elt_tys }
zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists
unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
-----------
unify_tc_app_help tc ty -- Revert to ordinary unification
= do { (tc_app, arg_tys) <- newTyConApp tc
; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
----------------------
-unifyAppTy :: TcType -- Expected type function: m
- -> TcType -- Type to split: m a
- -> TcM TcType -- Type arg: a
-unifyAppTy tc ty = unify_app_ty True tc ty
+unifyAppTy :: TcType -- Type to split: m a
+ -> TcM (TcType, TcType) -- (m,a)
+-- Assumes (m:*->*)
+
+unifyAppTy ty = unify_app_ty True ty
-unify_app_ty use tc (NoteTy _ ty) = unify_app_ty use tc ty
+unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty
-unify_app_ty use tc ty@(TyVarTy tyvar)
+unify_app_ty use ty@(TyVarTy tyvar)
= do { details <- condLookupTcTyVar use tyvar
; case details of
- IndirectTv use' ty' -> unify_app_ty use' tc ty'
- other -> unify_app_ty_help tc ty
+ IndirectTv use' ty' -> unify_app_ty use' ty'
+ other -> unify_app_ty_help ty
}
-unify_app_ty use tc ty
+unify_app_ty use ty
| Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
- = do { unifyTauTy tc fun_ty
- ; wobblify use arg_ty }
+ = do { fun' <- wobblify use fun_ty
+ ; arg' <- wobblify use arg_ty
+ ; return (fun', arg') }
- | otherwise = unify_app_ty_help tc ty
+ | otherwise = unify_app_ty_help ty
-unify_app_ty_help tc ty -- Revert to ordinary unification
- = do { arg_ty <- newTyFlexiVarTy (kindFunResult (typeKind tc))
- ; unifyTauTy (mkAppTy tc arg_ty) ty
- ; return arg_ty }
+unify_app_ty_help ty -- Revert to ordinary unification
+ = do { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind)
+ ; arg_ty <- newTyFlexiVarTy liftedTypeKind
+ ; unifyTauTy (mkAppTy fun_ty arg_ty) ty
+ ; return (fun_ty, arg_ty) }
----------------------
tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
- = do { span <- getSrcSpanM
- ; let rigid_info = GenSkol expected_ty span
- ; (forall_tvs, theta, phi_ty) <- tcSkolType rigid_info expected_ty
+ = do { -- We want the GenSkol info in the skolemised type variables to
+ -- mention the *instantiated* tyvar names, so that we get a
+ -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+ -- Hence the tiresome but innocuous fixM
+ ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+ do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
+ ; span <- getSrcSpanM
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+ ; return ((forall_tvs, theta, rho_ty), skol_info) })
+
+#ifdef DEBUG
+ ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
+ text "expected_ty" <+> ppr expected_ty,
+ text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
+ text "free_tvs" <+> ppr free_tvs,
+ text "forall_tvs" <+> ppr forall_tvs])
+#endif
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside phi_ty)
+ ; (result, lie) <- getLIE (thing_inside rho_ty)
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- Conclusion: include the free vars of the expected_ty in the
-- list of "free vars" for the signature check.
- ; dicts <- newDicts (SigOrigin rigid_info) theta
+ ; dicts <- newDicts (SigOrigin skol_info) theta
; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
-#ifdef DEBUG
- ; forall_tys <- zonkTcTyVars forall_tvs
- ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
- text "expected_ty" <+> ppr expected_ty,
- text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
- text "free_tvs" <+> ppr free_tvs,
- text "forall_tys" <+> ppr forall_tys])
-#endif
-
; checkSigTyVarsWrt free_tvs forall_tvs
; traceTc (text "tcGen:done")
ASSERT2( isTauTy ty2, ppr ty2 )
addErrCtxtM (unifyCtxt "type" ty1 ty2) $
uTys True ty1 ty1 True ty2 ty2
+
+unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
+unifyTheta theta1 theta2
+ = do { checkTc (equalLength theta1 theta2)
+ (ptext SLIT("Contexts differ in length"))
+ ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
\end{code}
@unifyTauTyList@ unifies corresponding elements of two lists of
case details of
IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
| otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
- FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2
- RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2
-
- -- Expand synonyms; ignore FTVs
-uFlexiVar :: Bool -> TcTyVar ->
- Bool -> -- Allow refinements to ty2
- TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Flexi
-uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
- = uFlexiVar swapped tv1 r2 ps_ty2 ty2
-
-uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
+ DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+----------------
+uDoneVar :: Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> Bool -- Allow refinements to ty2
+ -> TcTauType -> TcTauType -- Type 2
+ -> TcM ()
+-- Invariant: tyvar 1 is not unified with anything
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
+ = -- Expand synonyms; ignore FTVs
+ uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
= returnM ()
-- Distinct type variables
| otherwise
- = condLookupTcTyVar r2 tv2 `thenM` \ details ->
- case details of
- IndirectTv b ty2' -> uFlexiVar swapped tv1 b ty2' ty2'
- FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1)
- | otherwise -> updateFlexi swapped tv1 ty2
- RigidTv -> updateFlexi swapped tv1 ty2
- -- Note that updateFlexi does a sub-kind check
+ = do { lookup2 <- condLookupTcTyVar r2 tv2
+ ; case lookup2 of
+ IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2'
+ DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2
+ }
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
+ = case details1 of
+ MetaTv ref1 -> do { -- Do the occurs check, and check that we are not
+ -- unifying a type variable with a polytype
+ -- Returns a zonked type ready for the update
+ ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
+ ; updateMeta swapped tv1 ref1 ty2 }
+
+ skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
+
+
+----------------
+uDoneVars :: Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 2
+ -> TcM ()
+-- Invarant: the type variables are distinct,
+-- and are not already unified with anything
+
+uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
+ = case details2 of
+ MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ -- Note that updateMeta does a sub-kind check
-- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
where
k1 = tyVarKind tv1
-- so we can choose which to do.
nicer_to_update_tv2 = isSystemName (varName tv2)
- -- Try to update sys-y type variables in preference to sig-y ones
-
- -- First one is flexi, second one isn't a type variable
-uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2
- = -- Do the occurs check, and check that we are not
- -- unifying a type variable with a polytype
- -- Returns a zonked type ready for the update
- do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
- ; updateFlexi swapped tv1 ty2 }
-
--- Ready to update tv1, which is flexi; occurs check is done
-updateFlexi swapped tv1 ty2
- = do { checkKinds swapped tv1 ty2
- ; putMetaTyVar tv1 ty2 }
-
-
-uRigidVar :: Bool -> TcTyVar
- -> Bool -> -- Allow refinements to ty2
- TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Rigid
-uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
- = uRigidVar swapped tv1 r2 ps_ty2 ty2
-
- -- The both-type-variable case
-uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
- -- Same type variable => no-op
- | tv1 == tv2
- = returnM ()
+ -- Try to update sys-y type variables in preference to ones
+ -- gotten (say) by instantiating a polymorphic function with
+ -- a user-written type sig
+
+uDoneVars swapped tv1 (SkolemTv _) tv2 details2
+ = case details2 of
+ MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
- -- Distinct type variables
- | otherwise
- = condLookupTcTyVar r2 tv2 `thenM` \ details ->
- case details of
- IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2'
- FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1)
- RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2)
+uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
+ = case details2 of
+ MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
- -- Second one isn't a type variable
-uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2
- = unifyMisMatch (TyVarTy tv1) ps_ty2
+----------------
+updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+updateMeta swapped tv1 ref1 ty2
+ = do { checkKinds swapped tv1 ty2
+ ; writeMutVar ref1 (Indirect ty2) }
\end{code}
\begin{code}
-- unlifted type: e.g. (id 3#) is illegal
= addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
unifyKindMisMatch k1 k2
-
where
(k1,k2) | swapped = (tk2,tk1)
| otherwise = (tk1,tk2)
simple_result = (env1, quotes (ppr tidy_ty), empty)
; case tidy_ty of
TyVarTy tv
- | isSkolemTyVar tv -> return (env1, pp_rigid tv,
- pprSkolemTyVar tv)
+ | isSkolemTyVar tv -> return (env2, pp_rigid tv',
+ pprTcTyVar tv')
| otherwise -> return simple_result
+ where
+ (env2, tv') = tidySkolemTyVar env1 tv
other -> return simple_result }
where
pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
<+> ptext SLIT("is lifted")
| otherwise -- E.g. Monad [Int]
- = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
- ptext SLIT("but") <+> quotes (ppr ty) <+>
- ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
+ = ptext SLIT("Kind mis-match")
+
+ more_info = sep [ ptext SLIT("Expected kind") <+>
+ quotes (pprKind exp_kind) <> comma,
+ ptext SLIT("but") <+> quotes (ppr ty) <+>
+ ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
in
- failWithTc (ptext SLIT("Kind error:") <+> err)
+ failWithTc (err $$ more_info)
}
\end{code}
%* *
%************************************************************************
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found. It then checks that the type variables of the type signature
-are
- (a) Still all type variables
- eg matching signature [a] against inferred type [(p,q)]
- [then a will be unified to a non-type variable]
+@checkSigTyVars@ checks that a set of universally quantified type varaibles
+are not mentioned in the environment. In particular:
- (b) Still all distinct
- eg matching signature [(a,b)] against inferred type [(p,p)]
- [then a and b will be unified together]
-
- (c) Not mentioned in the environment
+ (a) Not mentioned in the type of a variable in the envt
eg the signature for f in this:
g x = ... where
Before doing this, the substitution is applied to the signature type variable.
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing. Then points (a) and (b) were
-self-checking. But it gave rise to bogus consequential error messages.
-For example:
-
- f = (*) -- Monomorphic
-
- g :: Num a => a -> a
- g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
-
\begin{code}
checkSigTyVars :: [TcTyVar] -> TcM ()
checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
-- tyvars should not mention any of these
-- Guaranteed already zonked.
-> [TcTyVar] -- Universally-quantified type variables in the signature
- -- Not guaranteed zonked.
+ -- Guaranteed to be skolems
-> TcM ()
-
check_sig_tyvars extra_tvs []
= returnM ()
check_sig_tyvars extra_tvs sig_tvs
- = do { gbl_tvs <- tcGetGlobalTyVars
+ = ASSERT( all isSkolemTyVar sig_tvs )
+ do { gbl_tvs <- tcGetGlobalTyVars
; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
text "gbl_tvs" <+> ppr gbl_tvs,
text "extra_tvs" <+> ppr extra_tvs]))
- -- Check that that the signature type vars are not free in the envt
; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
- ; checkM (not (mkVarSet sig_tvs `intersectsVarSet` env_tvs))
- (complain sig_tvs env_tvs)
+ ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
+ (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
+ }
- ; ASSERT( all isSkolemTyVar sig_tvs )
- return () }
+bleatEscapedTvs :: TcTyVarSet -- The global tvs
+ -> [TcTyVar] -- The possibly-escaping type variables
+ -> [TcTyVar] -- The zonked versions thereof
+ -> TcM ()
+-- Complain about escaping type variables
+-- We pass a list of type variables, at least one of which
+-- escapes. The first list contains the original signature type variable,
+-- while the second contains the type variable it is unified to (usually itself)
+bleatEscapedTvs globals sig_tvs zonked_tvs
+ = do { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
+ ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
where
- complain sig_tvs globals
- = -- "check" checks each sig tyvar in turn
- foldlM check
- (env, emptyVarEnv, [])
- tidy_tvs `thenM` \ (env2, _, msgs) ->
-
- failWithTcM (env2, main_msg $$ nest 2 (vcat msgs))
- where
- (env, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
-
- main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
-
- check (tidy_env, acc, msgs) tv
- -- sig_tyvar is from the signature;
- -- ty is what you get if you zonk sig_tyvar and then tidy it
- --
- -- acc maps a zonked type variable back to a signature type variable
- = case lookupVarEnv acc tv of {
- Just sig_tyvar' -> -- Error (b)!
- returnM (tidy_env, acc, unify_msg tv thing : msgs)
- where
- thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
-
- ; Nothing ->
-
- if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
- -- The least comprehensible, so put it last
- -- Game plan:
- -- get the local TcIds and TyVars from the environment,
- -- and pass them to find_globals (they might have tv free)
- then
- findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
- -- This rigid type variable has escaped into the envt
- -- We make it flexi so that subequent uses of these
- -- variables don't give rise to a cascade of further errors
- returnM (tidy_env1, acc, escape_msg tv globs : msgs)
-
- else -- All OK
- returnM (tidy_env, extendVarEnv acc tv tv, msgs)
- }
-\end{code}
+ (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
+ (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
+ main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
+
+ check (tidy_env, msgs) (sig_tv, zonked_tv)
+ | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
+ | otherwise
+ = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
+ ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
-\begin{code}
-----------------------
-escape_msg sig_tv globs
- = mk_msg sig_tv <+> ptext SLIT("escapes") $$
- if notNull globs then
- vcat [ptext SLIT("It is mentioned in the environment:"),
- nest 2 (vcat globs)]
- else
- empty -- Sigh. It's really hard to give a good error message
- -- all the time. One bad case is an existential pattern match.
- -- We rely on the "When..." context to help.
-
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
-mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
+escape_msg sig_tv zonked_tv globs
+ | notNull globs
+ = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
+ nest 2 (vcat globs)]
+ | otherwise
+ = msg <+> ptext SLIT("escapes")
+ -- Sigh. It's really hard to give a good error message
+ -- all the time. One bad case is an existential pattern match.
+ -- We rely on the "When..." context to help.
+ where
+ msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
+ is_bound_to
+ | sig_tv == zonked_tv = empty
+ | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
\end{code}
These two context are used with checkSigTyVars