From bf9eb20fbc731c05724297022a4b9a1479ddd180 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Thu, 30 Aug 2007 14:49:01 +0000 Subject: [PATCH] Added decidability check for type instances --- compiler/typecheck/TcMType.lhs | 110 ++++++++++++++++++++++++++++++++++- compiler/typecheck/TcRnDriver.lhs | 4 +- compiler/typecheck/TcTyClsDecls.lhs | 42 ++----------- 3 files changed, 115 insertions(+), 41 deletions(-) diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 7186b3c..3234e1c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -41,7 +41,7 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, arityErr, -------------------------------- @@ -1182,7 +1182,7 @@ checkValidInstance tyvars theta clas inst_tys -- Check that instance inference will terminate (if we care) -- For Haskell 98 this will already have been done by checkValidTheta, - -- but as we may be using other extensions we need to check. + -- but as we may be using other extensions we need to check. ; unless undecidable_ok $ mapM_ addErrTc (checkInstTermination inst_tys theta) @@ -1233,7 +1233,101 @@ predUndecErr pred msg = sep [msg, 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") +\end{code} + + +%************************************************************************ +%* * +\subsection{Checking type instance well-formedness and termination} +%* * +%************************************************************************ + +\begin{code} +-- Check that a "type instance" is well-formed (which includes decidability +-- unless -fallow-undecidable-instances is given). +-- +checkValidTypeInst :: [Type] -> Type -> TcM () +checkValidTypeInst typats rhs + = do { -- left-hand side contains no type family applications + -- (vanilla synonyms are fine, though) + ; mappM_ checkTyFamFreeness typats + + -- the right-hand side is a tau type + ; checkTc (isTauTy rhs) $ + polyTyErr rhs + + -- we have a decidable instance unless otherwise permitted + ; undecidable_ok <- doptM Opt_UndecidableInstances + ; unless undecidable_ok $ + mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) + } + +-- Make sure that each type family instance is +-- (1) strictly smaller than the lhs, +-- (2) mentions no type variable more often than the lhs, and +-- (3) does not contain any further type family instances. +-- +checkFamInst :: [Type] -- lhs + -> [(TyCon, [Type])] -- type family instances + -> [Message] +checkFamInst lhsTys famInsts + = mapCatMaybes check famInsts + where + size = sizeTypes lhsTys + fvs = fvTypes lhsTys + check (tc, tys) + | not (all isTyFamFree tys) + = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg) + | not (null (fvTypes tys \\ fvs)) + = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg) + | size <= sizeTypes tys + = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg) + | otherwise + = Nothing + where + famInst = TyConApp tc tys + +-- Ensure that no type family instances occur in a type. +-- +checkTyFamFreeness :: Type -> TcM () +checkTyFamFreeness ty + = checkTc (isTyFamFree ty) $ + tyFamInstInIndexErr ty + +-- Check that a type does not contain any type family applications. +-- +isTyFamFree :: Type -> Bool +isTyFamFree = null . tyFamInsts + +-- Error messages + +tyFamInstInIndexErr ty + = hang (ptext SLIT("Illegal type family application in type instance") <> + colon) 4 $ + ppr ty + +polyTyErr ty + = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $ + ppr ty + +famInstUndecErr ty msg + = sep [msg, + nest 2 (ptext SLIT("in the type family application:") <+> + pprType ty)] + +nestedMsg = ptext SLIT("Nested type family application") +nomoreVarMsg = ptext SLIT("Variable occurs more often than in instance head") +smallerAppMsg = ptext SLIT("Application is no smaller than the instance head") +\end{code} + +%************************************************************************ +%* * +\subsection{Auxiliary functions} +%* * +%************************************************************************ + +\begin{code} -- Free variables of a type, retaining repetitions, and expanding synonyms fvType :: Type -> [TyVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty @@ -1271,4 +1365,16 @@ sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 + +-- Type family instances occuring in a type after expanding synonyms +tyFamInsts :: Type -> [(TyCon, [Type])] +tyFamInsts ty + | Just exp_ty <- tcView ty = tyFamInsts exp_ty +tyFamInsts (TyVarTy _) = [] +tyFamInsts (TyConApp tc tys) + | isOpenSynTyCon tc = [(tc, tys)] + | otherwise = concat (map tyFamInsts tys) +tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (ForAllTy _ ty) = tyFamInsts ty \end{code} diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index bb67d9b..3b868a1 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -1060,16 +1060,18 @@ tcGhciStmts stmts } ; -- OK, we're ready to typecheck the stmts - traceTc (text "tcs 2") ; + traceTc (text "TcRnDriver.tcGhciStmts: tc stmts") ; ((tc_stmts, ids), lie) <- getLIE $ tc_io_stmts stmts $ \ _ -> mappM tcLookupId names ; -- Look up the names right in the middle, -- where they will all be in scope -- Simplify the context + traceTc (text "TcRnDriver.tcGhciStmts: simplify ctxt") ; const_binds <- checkNoErrs (tcSimplifyInteractive lie) ; -- checkNoErrs ensures that the plan fails if context redn fails + traceTc (text "TcRnDriver.tcGhciStmts: done") ; return (ids, mkHsDictLet const_binds $ noLoc (HsDo DoExpr tc_stmts (mk_return ids) io_ret_ty)) } diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 863cd6d..5dfb630 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -275,13 +275,8 @@ tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name}) ; t_rhs <- tcHsKindedType k_rhs -- (3) check that - -- - left-hand side contains no type family applications - -- (vanilla synonyms are fine, though) - ; mappM_ checkTyFamFreeness t_typats - - -- - the right-hand side is a tau type - ; unless (isTauTy t_rhs) $ - addErr (polyTyErr t_rhs) + -- - check the well-formedness of the instance + ; checkValidTypeInst t_typats t_rhs -- (4) construct representation tycon ; rep_tc_name <- newFamInstTyConName tc_name loc @@ -317,7 +312,8 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name, -- (3) Check that -- - left-hand side contains no type family applications - -- (vanilla synonyms are fine, though) + -- (vanilla synonyms are fine, though, and we checked for + -- foralls earlier) ; mappM_ checkTyFamFreeness t_typats -- - we don't use GADT syntax for indexed types @@ -354,27 +350,6 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name, L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False other -> True --- Check that a type index does not contain any type family applications --- --- * Earlier phases have already checked that there are no foralls in the --- type; we also cannot have PredTys and NoteTys are being skipped by using --- the core view. --- -checkTyFamFreeness :: Type -> TcM () -checkTyFamFreeness ty | Just (tycon, tys) <- splitTyConApp_maybe ty - = if isSynTyCon tycon - then addErr $ tyFamAppInIndexErr ty - else mappM_ checkTyFamFreeness tys - -- splitTyConApp_maybe uses the core view; hence, - -- any synonym tycon must be a family tycon - - | Just (ty1, ty2) <- splitAppTy_maybe ty - = checkTyFamFreeness ty1 >> checkTyFamFreeness ty2 - - | otherwise -- only vars remaining - = return () - - -- Kind checking of indexed types -- - @@ -1278,15 +1253,6 @@ wrongKindOfFamily family = | isAlgTyCon family = ptext SLIT("data type") | otherwise = pprPanic "wrongKindOfFamily" (ppr family) -polyTyErr ty - = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $ - ppr ty - -tyFamAppInIndexErr ty - = hang (ptext SLIT("Illegal type family application in type instance") <> - colon) 4 $ - ppr ty - emptyConDeclsErr tycon = sep [quotes (ppr tycon) <+> ptext SLIT("has no constructors"), nest 2 $ ptext SLIT("(-XEmptyDataDecls permits this)")] -- 1.7.10.4