-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, instTypeErr, checkAmbiguity,
+ checkValidInstHead, checkValidInstance, checkAmbiguity,
checkInstTermination,
arityErr,
-- 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 )
import Outputable
+import Control.Monad ( when )
import Data.List ( (\\) )
\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
- gla_exts = dopt Opt_GlasgowExts dflags
+ 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 variable argument"),
+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
- = returnM ()
+ = 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")
-\end{code}
-\begin{code}
+ -- 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) }
+
instTypeErr pp_ty msg
= sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
nest 4 msg]
%* *
%************************************************************************
+
+\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.
+(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
- dflags <- getDOpts
- check_inst_termination dflags theta tys
-
-check_inst_termination dflags theta tys
- | not (dopt Opt_GlasgowExts dflags) = returnM ()
- | dopt Opt_AllowUndecidableInstances dflags = returnM ()
- | otherwise = do
- mappM_ (check_nomore (fvTypes tys)) theta
- mappM_ (check_smaller (sizeTypes tys)) theta
+ = do { mappM_ (check_nomore (fvTypes tys)) theta
+ ; mappM_ (check_smaller (sizeTypes tys)) theta }
check_nomore :: [TyVar] -> PredType -> TcM ()
check_nomore fvs pred
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
+-- 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]
fvPred (ClassP _ tys') = fvTypes tys'
fvPred (IParam _ ty) = fvType ty
--- size of a type: the number of variables and constructors
+-- 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
projects / ghc-hetmet.git / blobdiff