Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance, checkAmbiguity,
+ checkInstTermination,
arityErr,
--------------------------------
-- others:
import TcRnMonad -- TcType, amongst others
-import FunDeps ( grow, checkInstFDs )
+import FunDeps ( grow, checkInstCoverage )
import Name ( Name, setNameUnique, mkSysTvName )
import VarSet
-import DynFlags ( dopt, DynFlag(..), DynFlags )
+import DynFlags ( dopt, DynFlag(..) )
import Util ( nOfThem, isSingleton, notNull )
import ListSetOps ( removeDups )
import Outputable
+import Control.Monad ( when )
import Data.List ( (\\) )
\end{code}
check_class_pred_tys dflags ctxt tys
= case ctxt of
TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
- InstThetaCtxt -> gla_exts || all tcIsTyVarTy 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 { dflags <- getDOpts
+ = 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 termainate
+ -- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
- ; checkInstTermination dflags theta inst_tys
+ ; when (gla_exts && not undecidable_ok) $
+ checkInstTermination theta inst_tys
-- The Coverage Condition
- ; checkTc (checkInstFDs theta clas inst_tys)
+ ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
}
where
- msg = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class"))
+ msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
\end{code}
Termination test: each assertion in the context satisfies
(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 :: DynFlags -> ThetaType -> [TcType] -> TcM ()
-checkInstTermination 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
+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
projects / ghc-hetmet.git / blobdiff