From b610eca3e4405e185bab53204cf2829893ada268 Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Fri, 9 Jun 2000 15:53:12 +0000
Subject: [PATCH] [project @ 2000-06-09 15:53:12 by simonpj] GHC gets upset if
you have types like
Eq a => a->a
where 'a' is *not* universally quantified.
By "upset" I mean that the typechecker generates
rather bogus code, that subsequently kills Lint.
Such types used to be rejected in the renamer,
but Jeff removed that in favour of an ambiguity
check in TcMonoType. I remember agreeing to move
the renamer check to the type checker, and Jeff did this,
but the check in TcMonoType was only checking for
*ambiguity*, which isn't quite the same.
I've restored the missing check and commented it
better in TcMonoType.
Jeff: if this isn't right for you, let's dicuss.
Incidentally, I also generalise the ambiguity check
to detect
forall a. ?x::a => Int
which is ambiguous.
I did a few formatting changes too.
---
ghc/compiler/hsSyn/HsMatches.lhs | 4 +-
ghc/compiler/rename/RnSource.lhs | 11 ++---
ghc/compiler/typecheck/TcMonoType.lhs | 67 ++++++++++++++++++++-------
ghc/compiler/types/PprType.lhs | 7 +--
4 files changed, 55 insertions(+), 34 deletions(-)
diff --git a/ghc/compiler/hsSyn/HsMatches.lhs b/ghc/compiler/hsSyn/HsMatches.lhs
index 640c717148cf..151e499d5b3c 100644
--- a/ghc/compiler/hsSyn/HsMatches.lhs
+++ b/ghc/compiler/hsSyn/HsMatches.lhs
@@ -44,8 +44,8 @@ patterns in each equation.
\begin{code}
data Match id pat
= Match
- [HsTyVarBndr id] -- Tyvars wrt which this match is universally quantified
- -- emtpy after typechecking
+ [HsTyVarBndr id] -- Tyvars wrt which this match is universally quantified
+ -- empty after typechecking
[pat] -- The patterns
(Maybe (HsType id)) -- A type signature for the result of the match
-- Nothing after typechecking
diff --git a/ghc/compiler/rename/RnSource.lhs b/ghc/compiler/rename/RnSource.lhs
index f987c027373f..60615a9769a2 100644
--- a/ghc/compiler/rename/RnSource.lhs
+++ b/ghc/compiler/rename/RnSource.lhs
@@ -566,21 +566,16 @@ rnHsType doc (HsForAllTy Nothing ctxt ty)
rnHsType doc (HsForAllTy (Just forall_tyvars) ctxt tau)
-- Explicit quantification.
- -- Check that the forall'd tyvars are a subset of the
- -- free tyvars in the tau-type part
- -- That's only a warning... unless the tyvar is constrained by a
- -- context in which case it's an error
+ -- Check that the forall'd tyvars are actually
+ -- mentioned in the type, and produce a warning if not
= let
mentioned_in_tau = extractHsTyRdrTyVars tau
mentioned_in_ctxt = extractHsCtxtRdrTyVars ctxt
mentioned = nub (mentioned_in_tau ++ mentioned_in_ctxt)
- tys_of_pred (HsPClass clas tys) = tys
- tys_of_pred (HsPIParam n ty) = [ty]
forall_tyvar_names = map getTyVarName forall_tyvars
- -- explicitly quantified but not mentioned in ctxt or tau
+ -- Explicitly quantified but not mentioned in ctxt or tau
warn_guys = filter (`notElem` mentioned) forall_tyvar_names
-
in
mapRn_ (forAllWarn doc tau) warn_guys `thenRn_`
rnForAll doc forall_tyvars ctxt tau
diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index cb70d6a08405..250410139848 100644
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -37,12 +37,12 @@ import Type ( Type, PredType(..), ThetaType, UsageAnn(..),
mkUsForAllTy, zipFunTys, hoistForAllTys,
mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
- boxedTypeKind, unboxedTypeKind, tyVarsOfType,
+ boxedTypeKind, unboxedTypeKind,
mkArrowKinds, getTyVar_maybe, getTyVar,
tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
- tyVarsOfType, tyVarsOfTypes, mkForAllTys
+ tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys
)
-import PprType ( pprConstraint, pprType )
+import PprType ( pprConstraint, pprType, pprPred )
import Subst ( mkTopTyVarSubst, substTy )
import Id ( mkVanillaId, idName, idType, idFreeTyVars )
import Var ( TyVar, mkTyVar, mkNamedUVar, varName )
@@ -214,19 +214,41 @@ tc_type_kind (HsForAllTy (Just tv_names) context ty)
-- give overloaded functions like
-- f :: forall a. Num a => (# a->a, a->a #)
-- And we want these to get through the type checker
- check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
- where ct_vars = tyVarsOfTypes tys
- forall_tyvars = map varName in_scope_vars
- tau_vars = tyVarsOfType tau
- fds = instFunDepsOfTheta theta
- tvFundep = tyVarFunDep fds
- extended_tau_vars = oclose tvFundep tau_vars
- ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
- not (ct_var `elemUFM` extended_tau_vars)
- ambiguous = foldUFM ((||) . ambig) False ct_vars
- check _ = returnTc ()
+
+ -- Check for ambiguity
+ -- forall V. P => tau
+ -- is ambiguous if P contains generic variables
+ -- (i.e. one of the Vs) that are not mentioned in tau
+ --
+ -- However, we need to take account of functional dependencies
+ -- when we speak of 'mentioned in tau'. Example:
+ -- class C a b | a -> b where ...
+ -- Then the type
+ -- forall x y. (C x y) => x
+ -- is not ambiguous because x is mentioned and x determines y
+ --
+ -- In addition, GHC insists that at least one type variable
+ -- in each constraint is in V. So we disallow a type like
+ -- forall a. Eq b => b -> b
+ -- even in a scope where b is in scope.
+
+ forall_tyvars = map varName tyvars -- was: in_scope_vars. Why???
+ tau_vars = tyVarsOfType tau
+ fds = instFunDepsOfTheta theta
+ tvFundep = tyVarFunDep fds
+ extended_tau_vars = oclose tvFundep tau_vars
+ is_ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemUFM` extended_tau_vars)
+ is_free ct_var = not (varName ct_var `elem` forall_tyvars)
+
+ check_pred pred = checkTc (not any_ambig) (ambigErr pred ty) `thenTc_`
+ checkTc (not all_free) (freeErr pred ty)
+ where
+ ct_vars = varSetElems (tyVarsOfPred pred)
+ any_ambig = any is_ambig ct_vars
+ all_free = all is_free ct_vars
in
- mapTc check theta `thenTc_`
+ mapTc check_pred theta `thenTc_`
returnTc (body_kind, mkSigmaTy tyvars theta tau)
\end{code}
@@ -410,7 +432,8 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
tcTySig :: RenamedSig -> TcM s TcSigInfo
tcTySig (Sig v ty src_loc)
- = tcAddSrcLoc src_loc $
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxt (tcsigCtxt v) $
tcHsSigType ty `thenTc` \ sigma_tc_ty ->
mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
returnTc sig
@@ -699,6 +722,8 @@ sigPatCtxt bound_tvs bound_ids tidy_env
%************************************************************************
\begin{code}
+tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
+
typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
typeKindCtxt :: RenamedHsType -> Message
@@ -718,8 +743,14 @@ tyConAsClassErr name
tyVarAsClassErr name
= ptext SLIT("Type variable used as a class:") <+> ppr name
-ambigErr (c, ts) ty
- = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
+ambigErr pred ty
+ = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
nest 4 (ptext SLIT("for the type:") <+> ppr ty),
nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
+
+freeErr pred ty
+ = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
+ ptext SLIT("does not mention any of the universally quantified type variables"),
+ nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
+ ]
\end{code}
diff --git a/ghc/compiler/types/PprType.lhs b/ghc/compiler/types/PprType.lhs
index 6b22faa886d3..45717e66c44a 100644
--- a/ghc/compiler/types/PprType.lhs
+++ b/ghc/compiler/types/PprType.lhs
@@ -72,7 +72,7 @@ pprPred (Class clas tys) = pprConstraint clas tys
pprPred (IParam n ty) = hsep [ppr n, ptext SLIT("::"), ppr ty]
pprConstraint :: Class -> [Type] -> SDoc
-pprConstraint clas tys = ppr clas <+> hsep (map (pprParendType) tys)
+pprConstraint clas tys = ppr clas <+> hsep (map pprParendType tys)
pprTheta :: ThetaType -> SDoc
pprTheta theta = parens (hsep (punctuate comma (map pprPred theta)))
@@ -226,11 +226,6 @@ ppr_pred env (Class clas tys) = ppr clas <+>
hsep (map (ppr_ty env tYCON_PREC) tys)
ppr_pred env (IParam n ty) = hsep [char '?' <> ppr n, text "::",
ppr_ty env tYCON_PREC ty]
-
-{-
-ppr_dict env ctxt (clas, tys) = ppr clas <+>
- hsep (map (ppr_ty env tYCON_PREC) tys)
--}
\end{code}
\begin{code}
--
GitLab