newKindVar, tcInstSigVar,
zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
)
-import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
+import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
+ instFunDeps, instFunDepsOfTheta )
+import FunDeps ( tyVarFunDep, oclose )
import TcUnify ( unifyKind, unifyKinds, unifyTypeKind )
import Type ( Type, PredType(..), ThetaType, UsageAnn(..),
mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
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 )
returnTc (kind, mkUsForAllTy uv tc_ty)
tc_type_kind (HsForAllTy (Just tv_names) context ty)
- = tcExtendTyVarScope tv_names $ \ tyvars ->
+ = tcExtendTyVarScope tv_names $ \ forall_tyvars ->
tcContext context `thenTc` \ theta ->
tc_type_kind ty `thenTc` \ (kind, tau) ->
- tcGetInScopeTyVars `thenTc` \ in_scope_vars ->
let
body_kind | null theta = kind
| otherwise = boxedTypeKind
-- 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
- ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
- not (ct_var `elemUFM` 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
+ --
+ -- NOTE: 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.
+ -- This is the is_free test below.
+
+ tau_vars = tyVarsOfType tau
+ fds = instFunDepsOfTheta theta
+ tvFundep = tyVarFunDep fds
+ extended_tau_vars = oclose tvFundep tau_vars
+ is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemUFM` extended_tau_vars)
+ is_free ct_var = not (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 = is_source_polytype && any is_ambig ct_vars
+ all_free = all is_free ct_vars
+
+ -- Check ambiguity only for source-program types, not
+ -- for types coming from inteface files. The latter can
+ -- legitimately have ambiguous types. Example
+ -- class S a where s :: a -> (Int,Int)
+ -- instance S Char where s _ = (1,1)
+ -- f:: S a => [a] -> Int -> (Int,Int)
+ -- f (_::[a]) x = (a*x,b)
+ -- where (a,b) = s (undefined::a)
+ -- Here the worker for f gets the type
+ -- fw :: forall a. S a => Int -> (# Int, Int #)
+ --
+ -- If the list of tv_names is empty, we have a monotype,
+ -- and then we don't need to check for ambiguity either,
+ -- because the test can't fail (see is_ambig).
+ is_source_polytype = case tv_names of
+ (UserTyVar _ : _) -> True
+ other -> False
in
- mapTc check theta `thenTc_`
- returnTc (body_kind, mkSigmaTy tyvars theta tau)
+ mapTc check_pred theta `thenTc_`
+ returnTc (body_kind, mkSigmaTy forall_tyvars theta tau)
\end{code}
Help functions for type applications
-- Does *not* have name = N
-- Has type tau
- Inst -- Empty if theta is null, or
+ [Inst] -- Empty if theta is null, or
-- (method mono_id) otherwise
SrcLoc -- Of the signature
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
tyvar_tys'
theta' tau' `thenNF_Tc` \ inst ->
-- We make a Method even if it's not overloaded; no harm
+ instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
- returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
+ returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
where
name = idName poly_id
\end{code}
%************************************************************************
\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
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}
projects / ghc-hetmet.git / blobdiff