--------------------------------
-- Boxy type variables
- newBoxyTyVar, newBoxyTyVars, readFilledBox,
+ newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
-- Instantiation
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, instTypeErr, checkAmbiguity,
+ checkValidInstHead, checkValidInstance, checkAmbiguity,
+ checkInstTermination,
arityErr,
--------------------------------
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
MetaDetails(..), SkolemInfo(..), BoxInfo(..),
- BoxyTyVar, BoxyThetaType, BoxySigmaType,
+ BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
UserTypeCtxt(..),
isMetaTyVar, isSigTyVar, metaTvRef,
- tcCmpPred, isClassPred, tcEqType, tcGetTyVar,
+ tcCmpPred, isClassPred, tcGetTyVar,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcValidInstHeadTy, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy,
pprPred, pprTheta, pprClassPred )
import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
- liftedTypeKind, openTypeKind, defaultKind
+ liftedTypeKind, defaultKind
)
import Type ( TvSubst, zipTopTvSubst, substTy )
import Class ( Class, classArity, className )
-- others:
import TcRnMonad -- TcType, amongst others
-import FunDeps ( grow )
+import FunDeps ( grow, checkInstCoverage )
import Name ( Name, setNameUnique, mkSysTvName )
import VarSet
-import DynFlags ( dopt, DynFlag(..) )
+import DynFlags ( dopt, DynFlag(..) )
import Util ( nOfThem, isSingleton, notNull )
-import ListSetOps ( removeDups, findDupsEq )
+import ListSetOps ( removeDups )
import Outputable
+
+import Control.Monad ( when )
+import Data.List ( (\\) )
\end{code}
%************************************************************************
\begin{code}
-newBoxyTyVar :: TcM BoxyTyVar -- Of openTypeKind
-newBoxyTyVar = newMetaTyVar BoxTv openTypeKind
+newBoxyTyVar :: Kind -> TcM BoxyTyVar
+newBoxyTyVar kind = newMetaTyVar BoxTv kind
+
+newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
+newBoxyTyVars kinds = mapM newBoxyTyVar kinds
-newBoxyTyVars :: Int -> TcM [BoxyTyVar] -- Of openTypeKind
-newBoxyTyVars n = sequenceM [newMetaTyVar BoxTv openTypeKind | i <- [1..n]]
+newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
+newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
readFilledBox :: BoxyTyVar -> TcM TcType
-- Read the contents of the box, which should be filled in by now
-- f :: N a -> N a
| InstThetaCtxt -- Context of an instance decl
-- instance <S> => C [a] where ...
- | InstHeadCtxt -- Head of an instance decl
- -- instance ... => Eq a where ...
pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
-pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
\end{code}
arity = classArity cls
n_tys = length tys
arity_err = arityErr "Class" class_name arity n_tys
-
- how_to_allow = case ctxt of
- InstHeadCtxt -> empty -- Should not happen
- InstThetaCtxt -> parens undecidableMsg
- other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+ how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-- Implicit parameters only allows in type
check_class_pred_tys dflags ctxt tys
= case ctxt of
TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
- InstHeadCtxt -> True -- We check for instance-head
- -- formation in checkValidInstHead
- InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
- other -> gla_exts || all tyvar_head tys
+ InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
+ -- Further checks on head and theta in
+ -- checkInstTermination
+ other -> gla_exts || all tyvar_head tys
where
- undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
- gla_exts = dopt Opt_GlasgowExts dflags
-
--------------------------
-distinct_tyvars tys -- Check that the types are all distinct type variables
- = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
+ gla_exts = dopt Opt_GlasgowExts dflags
+ undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
-------------------------
tyvar_head ty -- Haskell 98 allows predicates of form
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
+predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
check_inst_head dflags clas tys
-- If GlasgowExts then check at least one isn't a type variable
| dopt Opt_GlasgowExts dflags
- = check_tyvars dflags clas tys
+ = mapM_ check_one tys
-- WITH HASKELL 98, MUST HAVE C (T a b c)
- | isSingleton tys,
- tcValidInstHeadTy first_ty
- = returnM ()
-
| otherwise
- = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
+ = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
+ (instTypeErr (pprClassPred clas tys) head_shape_msg)
where
(first_ty : _) = tys
head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
text "where T is not a synonym, and a,b,c are distinct type variables")
-check_tyvars dflags clas tys
- -- Check that at least one isn't a type variable
- -- unless -fallow-undecideable-instances
- | dopt Opt_AllowUndecidableInstances dflags = returnM ()
- | not (all tcIsTyVarTy tys) = returnM ()
- | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
- where
- msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
- $$ undecidableMsg)
+ -- For now, I only allow tau-types (not polytypes) in
+ -- the head of an instance decl.
+ -- E.g. instance C (forall a. a->a) is rejected
+ -- One could imagine generalising that, but I'm not sure
+ -- what all the consequences might be
+ check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
+ ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
-\end{code}
-
-\begin{code}
instTypeErr pp_ty msg
= sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
nest 4 msg]
\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Checking instance for termination}
+%* *
+%************************************************************************
+
+
+\begin{code}
+checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
+checkValidInstance tyvars theta clas inst_tys
+ = do { gla_exts <- doptM Opt_GlasgowExts
+ ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
+
+ ; checkValidTheta InstThetaCtxt theta
+ ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
+
+ -- Check that instance inference will terminate (if we care)
+ -- For Haskell 98, checkValidTheta has already done that
+ ; when (gla_exts && not undecidable_ok) $
+ checkInstTermination theta inst_tys
+
+ -- The Coverage Condition
+ ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
+ (instTypeErr (pprClassPred clas inst_tys) msg)
+ }
+ where
+ msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
+\end{code}
+
+Termination test: each assertion in the context satisfies
+ (1) no variable has more occurrences in the assertion than in the head, and
+ (2) the assertion has fewer constructors and variables (taken together
+ and counting repetitions) than the head.
+This is only needed with -fglasgow-exts, as Haskell 98 restrictions
+(which have already been checked) guarantee termination.
+
+The underlying idea is that
+
+ for any ground substitution, each assertion in the
+ context has fewer type constructors than the head.
+
+
+\begin{code}
+checkInstTermination :: ThetaType -> [TcType] -> TcM ()
+checkInstTermination theta tys
+ = do { mappM_ (check_nomore (fvTypes tys)) theta
+ ; mappM_ (check_smaller (sizeTypes tys)) theta }
+
+check_nomore :: [TyVar] -> PredType -> TcM ()
+check_nomore fvs pred
+ = checkTc (null (fvPred pred \\ fvs))
+ (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+
+check_smaller :: Int -> PredType -> TcM ()
+check_smaller n pred
+ = checkTc (sizePred pred < n)
+ (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+
+predUndecErr pred msg = sep [msg,
+ nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+
+nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
+undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
+
+-- Free variables of a type, retaining repetitions, and expanding synonyms
+fvType :: Type -> [TyVar]
+fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
+fvType (TyVarTy tv) = [tv]
+fvType (TyConApp _ tys) = fvTypes tys
+fvType (NoteTy _ ty) = fvType ty
+fvType (PredTy pred) = fvPred pred
+fvType (FunTy arg res) = fvType arg ++ fvType res
+fvType (AppTy fun arg) = fvType fun ++ fvType arg
+fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
+
+fvTypes :: [Type] -> [TyVar]
+fvTypes tys = concat (map fvType tys)
+
+fvPred :: PredType -> [TyVar]
+fvPred (ClassP _ tys') = fvTypes tys'
+fvPred (IParam _ ty) = fvType ty
+
+-- Size of a type: the number of variables and constructors
+sizeType :: Type -> Int
+sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
+sizeType (TyVarTy _) = 1
+sizeType (TyConApp _ tys) = sizeTypes tys + 1
+sizeType (NoteTy _ ty) = sizeType ty
+sizeType (PredTy pred) = sizePred pred
+sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
+sizeType (AppTy fun arg) = sizeType fun + sizeType arg
+sizeType (ForAllTy _ ty) = sizeType ty
+
+sizeTypes :: [Type] -> Int
+sizeTypes xs = sum (map sizeType xs)
+
+sizePred :: PredType -> Int
+sizePred (ClassP _ tys') = sizeTypes tys'
+sizePred (IParam _ ty) = sizeType ty
+\end{code}
projects / ghc-hetmet.git / blobdiff