Added decidability check for type instances

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 7186b3c..3234e1c 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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)")]