-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
SourceTyCtxt(..), checkValidTheta,
+ checkValidTyCon, checkValidClass,
checkValidInstHead, instTypeErr, checkAmbiguity,
--------------------------------
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcSplitTyConApp_maybe, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy,
- isUnLiftedType, isIPPred, isHoleTyVar,
+ isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
)
import qualified Type ( splitFunTys )
import Subst ( Subst, mkTopTyVarSubst, substTy )
-import Class ( Class, classArity, className )
+import Class ( Class, DefMeth(..), classArity, className, classBigSig )
import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
- tyConArity, tyConName, tyConKind )
+ tyConArity, tyConName, tyConKind, tyConTheta,
+ getSynTyConDefn, tyConDataCons )
+import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
+import FieldLabel ( fieldLabelName, fieldLabelType )
import PrimRep ( PrimRep(VoidRep) )
-import Var ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
-- others:
+import Generics ( validGenericMethodType )
import TcMonad -- TcType, amongst others
import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
import CmdLineOpts ( dopt, DynFlag(..) )
import Unique ( Uniquable(..) )
import SrcLoc ( noSrcLoc )
-import Util ( nOfThem, isSingleton, equalLength )
-import ListSetOps ( removeDups )
+import Util ( nOfThem, isSingleton, equalLength, notNull )
+import ListSetOps ( equivClasses, removeDups )
import Outputable
\end{code}
= tupleTyCon Boxed (length args) -- *-> ... ->*->*
| otherwise
- = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+ = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
mkPrimTyCon tc_name kind 0 [] VoidRep
-- Same name as the tyvar, apart from making it start with a colon (sigh)
-- I dread to think what will happen if this gets out into an
-- so that all other occurrences of the tyvar will get zapped too
zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
+ -- This warning shows up if the allegedly-unbound tyvar is
+ -- already bound to something. It can actually happen, and
+ -- in a harmless way (see [Silly Type Synonyms] below) so
+ -- it's only a warning
WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
returnNF_Tc immut_tv
\end{code}
+[Silly Type Synonyms]
+
+Consider this:
+ type C u a = u -- Note 'a' unused
+
+ foo :: (forall a. C u a -> C u a) -> u
+ foo x = ...
+
+ bar :: Num u => u
+ bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type {Num d} => d -> d
+ where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+ {Num (C d a)} => C d a -> C d a
+ where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+ because it does not 'really' mention a. (see Type.tyVarsOfType)
+ The arg to foo becomes
+ /\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+ a = ()
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly. I think its harmless to ignore the problem.
+
%************************************************************************
%* *
-- This shows up in the complaint about
-- case C a where
-- op :: Eq a => a -> a
-ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
+ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
| otherwise = ppr ty
where
(forall_tvs, theta, tau) = tcSplitSigmaTy ty
check_tau_type rank ubx_tup (AppTy ty1 ty2)
= check_arg_type ty1 `thenTc_` check_arg_type ty2
-check_tau_type rank ubx_tup (NoteTy note ty)
- = check_tau_type rank ubx_tup ty
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
-- Synonym notes are built only when the synonym is
-- saturated (see Type.mkSynTy)
- -- Not checking the 'note' part allows us to instantiate a synonym
- -- defn with a for-all type, or with a partially-applied type synonym,
- -- but that seems OK too
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ (if gla_exts then
+ -- If -fglasgow-exts then don't check the 'note' part.
+ -- This allows us to instantiate a synonym defn with a
+ -- for-all type, or with a partially-applied type synonym.
+ -- e.g. type T a b = a
+ -- type S m = m ()
+ -- f :: S (T Int)
+ -- Here, T is partially applied, so it's illegal in H98.
+ -- But if you expand S first, then T we get just
+ -- f :: Int
+ -- which is fine.
+ returnTc ()
+ else
+ -- For H98, do check the un-expanded part
+ check_tau_type rank ubx_tup syn
+ ) `thenTc_`
+
+ check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+ = check_tau_type rank ubx_tup ty
check_tau_type rank ubx_tup ty@(TyConApp tc tys)
| isSynTyCon tc
= -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
- -- synonym application, leaving it to checkValidType (i.e. right here
+ -- synonym application, leaving it to checkValidType (i.e. right here)
-- to find the error
checkTc syn_arity_ok arity_msg `thenTc_`
mapTc_ check_arg_type tys
freeErr pred
= sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
ptext SLIT("are already in scope"),
- nest 4 (ptext SLIT("At least one must be universally quantified here"))
+ nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
]
\end{code}
= returnTc ()
check_valid_theta ctxt theta
= getDOptsTc `thenNF_Tc` \ dflags ->
- warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
+ warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_`
mapTc_ (check_source_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
= -- Class predicates are valid in all contexts
mapTc_ check_arg_type tys `thenTc_`
checkTc (arity == n_tys) arity_err `thenTc_`
- checkTc (all tyvar_head tys || arby_preds_ok)
+ checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
where
n_tys = length tys
arity_err = arityErr "Class" class_name arity n_tys
- arby_preds_ok = case ctxt of
- InstHeadCtxt -> True -- We check for instance-head formation
- -- in checkValidInstHead
- InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
- other -> dopt Opt_GlasgowExts dflags
-
how_to_allow = case ctxt of
InstHeadCtxt -> empty -- Should not happen
InstThetaCtxt -> parens undecidableMsg
check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
-------------------------
+check_class_pred_tys dflags ctxt tys
+ = case ctxt of
+ InstHeadCtxt -> True -- We check for instance-head
+ -- formation in checkValidInstHead
+ InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
+ other -> gla_exts || all tyvar_head tys
+ where
+ undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
+ gla_exts = dopt Opt_GlasgowExts dflags
+
+-------------------------
tyvar_head ty -- Haskell 98 allows predicates of form
| tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
| otherwise -- where a is a type variable
%************************************************************************
%* *
+\subsection{Validity check for TyCons}
+%* *
+%************************************************************************
+
+checkValidTyCon is called once the mutually-recursive knot has been
+tied, so we can look at things freely.
+
+\begin{code}
+checkValidTyCon :: TyCon -> TcM ()
+checkValidTyCon tc
+ | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
+ | otherwise
+ = -- Check the context on the data decl
+ checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
+
+ -- Check arg types of data constructors
+ mapTc_ checkValidDataCon data_cons `thenTc_`
+
+ -- Check that fields with the same name share a type
+ mapTc_ check_fields groups
+
+ where
+ name = tyConName tc
+ (_, syn_rhs) = getSynTyConDefn tc
+ data_cons = tyConDataCons tc
+
+ fields = [field | con <- data_cons, field <- dataConFieldLabels con]
+ groups = equivClasses cmp_name fields
+ cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
+
+ check_fields fields@(first_field_label : other_fields)
+ -- These fields all have the same name, but are from
+ -- different constructors in the data type
+ = -- Check that all the fields in the group have the same type
+ -- NB: this check assumes that all the constructors of a given
+ -- data type use the same type variables
+ checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
+ where
+ field_ty = fieldLabelType first_field_label
+ field_name = fieldLabelName first_field_label
+ other_tys = map fieldLabelType other_fields
+
+checkValidDataCon :: DataCon -> TcM ()
+checkValidDataCon con
+ = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
+ -- This checks the argument types and
+ -- ambiguity of the existential context (if any)
+ tcAddErrCtxt (existentialCtxt con)
+ (checkFreeness ex_tvs ex_theta)
+ where
+ ctxt = ConArgCtxt (dataConName con)
+ (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
+
+
+fieldTypeMisMatch field_name
+ = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
+
+existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
+ <+> quotes (ppr con)
+\end{code}
+
+
+checkValidClass is called once the mutually-recursive knot has been
+tied, so we can look at things freely.
+
+\begin{code}
+checkValidClass :: Class -> TcM ()
+checkValidClass cls
+ = -- CHECK ARITY 1 FOR HASKELL 1.4
+ doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
+
+ -- Check that the class is unary, unless GlaExs
+ checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
+ checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
+
+ -- Check the super-classes
+ checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
+
+ -- Check the class operations
+ mapTc_ check_op op_stuff `thenTc_`
+
+ -- Check that if the class has generic methods, then the
+ -- class has only one parameter. We can't do generic
+ -- multi-parameter type classes!
+ checkTc (unary || no_generics) (genericMultiParamErr cls)
+
+ where
+ (tyvars, theta, _, op_stuff) = classBigSig cls
+ unary = isSingleton tyvars
+ no_generics = null [() | (_, GenDefMeth) <- op_stuff]
+
+ check_op (sel_id, dm)
+ = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
+ -- The 'tail' removes the initial (C a) from the
+ -- class itself, leaving just the method type
+
+ checkValidType (FunSigCtxt op_name) tau `thenTc_`
+
+ -- Check that for a generic method, the type of
+ -- the method is sufficiently simple
+ checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
+ (badGenericMethodType op_name op_ty)
+ where
+ op_name = idName sel_id
+ op_ty = idType sel_id
+ (_,theta,tau) = tcSplitSigmaTy op_ty
+
+nullaryClassErr cls
+ = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
+
+classArityErr cls
+ = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
+ parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
+
+genericMultiParamErr clas
+ = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
+ ptext SLIT("cannot have generic methods")
+
+badGenericMethodType op op_ty
+ = hang (ptext SLIT("Generic method type is too complex"))
+ 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
+ ptext SLIT("You can only use type variables, arrows, and tuples")])
+\end{code}
+
+
+%************************************************************************
+%* *
\subsection{Checking for a decent instance head type}
%* *
%************************************************************************
projects / ghc-hetmet.git / blobdiff