+
+
+%************************************************************************
+%* *
+\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