[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

@@ -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

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

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}

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}