Loosen the rules for instance declarations (Part 2)

Tidying up to Ross's  patch, plus adding documenation for it.

diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs
index 3fec58d..45338d0 100644 (file)
--- a/ghc/compiler/typecheck/TcInstDcls.lhs
+++ b/ghc/compiler/typecheck/TcInstDcls.lhs
@@ -13,12 +13,9 @@ import TcBinds               ( mkPragFun, tcPrags, badBootDeclErr )
 import TcClassDcl      ( tcMethodBind, mkMethodBind, badMethodErr, 
                          tcClassDecl2, getGenericInstances )
 import TcRnMonad       
 import TcClassDcl      ( tcMethodBind, mkMethodBind, badMethodErr, 
                          tcClassDecl2, getGenericInstances )
 import TcRnMonad       

-import TcMType         ( tcSkolSigType, checkValidTheta, checkValidInstHead,
-                         checkInstTermination, instTypeErr, 
-                         checkAmbiguity, SourceTyCtxt(..) )
-import TcType          ( mkClassPred, tyVarsOfType, 
-                         tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys,
-                         SkolemInfo(InstSkol), tcSplitDFunTy, pprClassPred )
+import TcMType         ( tcSkolSigType, checkValidInstance, checkValidInstHead )
+import TcType          ( mkClassPred, tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys,
+                         SkolemInfo(InstSkol), tcSplitDFunTy )

 import Inst            ( tcInstClassOp, newDicts, instToId, showLIE, 
                          getOverlapFlag, tcExtendLocalInstEnv )
 import InstEnv         ( mkLocalInstance, instanceDFunId )
 import Inst            ( tcInstClassOp, newDicts, instToId, showLIE, 
                          getOverlapFlag, tcExtendLocalInstEnv )
 import InstEnv         ( mkLocalInstance, instanceDFunId )

@@ -33,8 +30,7 @@ import Type           ( zipOpenTvSubst, substTheta, substTys )
 import DataCon         ( classDataCon )
 import Class           ( classBigSig )
 import Var             ( Id, idName, idType )
 import DataCon         ( classDataCon )
 import Class           ( classBigSig )
 import Var             ( Id, idName, idType )

-import MkId            ( mkDictFunId, rUNTIME_ERROR_ID )
-import FunDeps         ( checkInstFDs )
+import MkId            ( mkDictFunId )

 import Name            ( Name, getSrcLoc )
 import Maybe           ( catMaybes )
 import SrcLoc          ( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart )
 import Name            ( Name, getSrcLoc )
 import Maybe           ( catMaybes )
 import SrcLoc          ( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart )

@@ -186,32 +182,25 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags))
     setSrcSpan loc                     $
     addErrCtxt (instDeclCtxt1 poly_ty) $
 
     setSrcSpan loc                     $
     addErrCtxt (instDeclCtxt1 poly_ty) $
 

+    do { is_boot <- tcIsHsBoot
+       ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
+                 badBootDeclErr
+

        -- Typecheck the instance type itself.  We can't use 
        -- tcHsSigType, because it's not a valid user type.
        -- Typecheck the instance type itself.  We can't use 
        -- tcHsSigType, because it's not a valid user type.

-    kcHsSigType poly_ty                        `thenM` \ kinded_ty ->
-    tcHsKindedType kinded_ty           `thenM` \ poly_ty' ->
-    let
-       (tyvars, theta, tau) = tcSplitSigmaTy poly_ty'
-    in
-    checkValidTheta InstThetaCtxt theta                        `thenM_`
-    checkAmbiguity tyvars theta (tyVarsOfType tau)     `thenM_`
-    checkValidInstHead tau                             `thenM` \ (clas,inst_tys) ->
-    checkInstTermination theta inst_tys                        `thenM_`
-    checkTc (checkInstFDs theta clas inst_tys)
-           (instTypeErr (pprClassPred clas inst_tys) msg)      `thenM_`
-    newDFunName clas inst_tys (srcSpanStart loc)               `thenM` \ dfun_name ->
-    getOverlapFlag                                             `thenM` \ overlap_flag ->
-    let dfun  = mkDictFunId dfun_name tyvars theta clas inst_tys
-       ispec = mkLocalInstance dfun overlap_flag
-    in
-
-    tcIsHsBoot                                         `thenM` \ is_boot ->
-    checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
-           badBootDeclErr                              `thenM_`
-
-    returnM (Just (InstInfo { iSpec = ispec, iBinds = VanillaInst binds uprags }))
-  where
-    msg  = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class"))
+       ; kinded_ty <- kcHsSigType poly_ty
+       ; poly_ty'  <- tcHsKindedType kinded_ty
+       ; let (tyvars, theta, tau) = tcSplitSigmaTy poly_ty'
+       
+       ; (clas, inst_tys) <- checkValidInstHead tau
+       ; checkValidInstance tyvars theta clas inst_tys
+
+       ; dfun_name <- newDFunName clas inst_tys (srcSpanStart loc)
+       ; overlap_flag <- getOverlapFlag
+       ; let dfun  = mkDictFunId dfun_name tyvars theta clas inst_tys
+             ispec = mkLocalInstance dfun overlap_flag
+
+       ; return (Just (InstInfo { iSpec = ispec, iBinds = VanillaInst binds uprags })) }

 \end{code}
 
 
 \end{code}
 
 

@@ -401,9 +390,6 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds })
                -- member) are dealt with by the common MkId.mkDataConWrapId code rather
                -- than needing to be repeated here.
 
                -- member) are dealt with by the common MkId.mkDataConWrapId code rather
                -- than needing to be repeated here.
 

-         where
-           msg = "Compiler error: bad dictionary " ++ showSDoc (ppr clas)
-

        dict_bind  = noLoc (VarBind this_dict_id dict_rhs)
        all_binds  = dict_bind `consBag` (sc_binds `unionBags` meth_binds)
 
        dict_bind  = noLoc (VarBind this_dict_id dict_rhs)
        all_binds  = dict_bind `consBag` (sc_binds `unionBags` meth_binds)
 

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index df1f069..3a232b7 100644 (file)
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -33,8 +33,7 @@ module TcMType (
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, 
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, 
   SourceTyCtxt(..), checkValidTheta, checkFreeness,

-  checkValidInstHead, instTypeErr, checkAmbiguity,
-  checkInstTermination,
+  checkValidInstHead, checkValidInstance, checkAmbiguity,

   arityErr, 
 
   --------------------------------
   arityErr, 
 
   --------------------------------

@@ -90,10 +89,10 @@ import Kind         ( isSubKind )
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 
 -- others:
 import TcRnMonad          -- TcType, amongst others

-import FunDeps         ( grow )
+import FunDeps         ( grow, checkInstFDs )

 import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet

-import DynFlags        ( dopt, DynFlag(..) )
+import DynFlags                ( dopt, DynFlag(..), DynFlags )

 import Util            ( nOfThem, isSingleton, notNull )
 import ListSetOps      ( removeDups )
 import Outputable
 import Util            ( nOfThem, isSingleton, notNull )
 import ListSetOps      ( removeDups )
 import Outputable

@@ -907,11 +906,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
     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_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type

@@ -930,10 +925,10 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 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 || 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
 
   where
     gla_exts      = dopt Opt_GlasgowExts dflags
 

@@ -1108,6 +1103,27 @@ instTypeErr pp_ty msg
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

+
+\begin{code}
+checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
+checkValidInstance tyvars theta clas inst_tys
+  = do { dflags <- getDOpts
+
+       ; checkValidTheta InstThetaCtxt theta
+       ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
+
+       -- Check that instance inference will termainate
+       -- For Haskell 98, checkValidTheta has already done that
+       ; checkInstTermination dflags theta inst_tys
+       
+       -- The Coverage Condition
+       ; checkTc (checkInstFDs theta 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"))
+\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
 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

@@ -1116,13 +1132,8 @@ This is only needed with -fglasgow-exts, as Haskell 98 restrictions
 (which have already been checked) guarantee termination.
 
 \begin{code}
 (which have already been checked) guarantee termination.
 
 \begin{code}

-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
-  = do
-    dflags <- getDOpts
-    check_inst_termination dflags theta tys
-
-check_inst_termination dflags theta tys
+checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM ()
+checkInstTermination dflags theta tys

   | not (dopt Opt_GlasgowExts dflags)         = returnM ()
   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
   | otherwise = do
   | not (dopt Opt_GlasgowExts dflags)         = returnM ()
   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
   | otherwise = do

@@ -1146,7 +1157,7 @@ nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the i
 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
 
 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]
 fvType :: Type -> [TyVar]
 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
 fvType (TyVarTy tv)        = [tv]

@@ -1164,7 +1175,7 @@ fvPred :: PredType -> [TyVar]
 fvPred (ClassP _ tys')     = fvTypes tys'
 fvPred (IParam _ ty)       = fvType ty
 
 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
 sizeType :: Type -> Int
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy _)       = 1

diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index 4d7577d..a5ac2b3 100644 (file)
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -1673,38 +1673,124 @@ class like this:
 <sect2 id="instance-decls">
 <title>Instance declarations</title>
 
 <sect2 id="instance-decls">
 <title>Instance declarations</title>
 

-<sect3 id="instance-heads">
-<title>Instance heads</title>
+<sect3 id="instance-rules">
+<title>Relaxed rules for instance declarations</title>
+
+<para>An instance declaration has the form
+<screen>
+  instance ( <replaceable>assertion</replaceable><subscript>1</subscript>, ..., <replaceable>assertion</replaceable><subscript>n</subscript>) =&gt; <replaceable>class</replaceable> <replaceable>type</replaceable><subscript>1</subscript> ... <replaceable>type</replaceable><subscript>m</subscript> where ...
+</screen>
+The part before the "<literal>=&gt;</literal>" is the
+<emphasis>context</emphasis>, while the part after the
+"<literal>=&gt;</literal>" is the <emphasis>head</emphasis> of the instance declaration.
+</para>

 
 <para>
 
 <para>

-The <emphasis>head</emphasis> of an instance declaration is the part to the
-right of the "<literal>=&gt;</literal>".  In Haskell 98 the head of an instance
-declaration
+In Haskell 98 the head of an instance declaration

 must be of the form <literal>C (T a1 ... an)</literal>, where
 <literal>C</literal> is the class, <literal>T</literal> is a type constructor,
 and the <literal>a1 ... an</literal> are distinct type variables.
 must be of the form <literal>C (T a1 ... an)</literal>, where
 <literal>C</literal> is the class, <literal>T</literal> is a type constructor,
 and the <literal>a1 ... an</literal> are distinct type variables.

+Furthermore, the assertions in the context of the instance declaration be of
+the form <literal>C a</literal> where <literal>a</literal> is a type variable.

 </para>
 <para>
 </para>
 <para>

-The <option>-fglasgow-exts</option> flag lifts this restriction and allows the
-instance head to be of form <literal>C t1 ... tn</literal> where <literal>t1
-... tn</literal> are arbitrary types (provided, of course, everything is
-well-kinded).  In particular, types <literal>ti</literal> can be type variables
-or structured types, and can contain repeated occurrences of a single type
-variable.
-Examples:
+The <option>-fglasgow-exts</option> flag loosens these restrictions
+considerably.  Firstly, multi-parameter type classes are permitted.  Secondly,
+the context and head of the instance declaration can each consist of arbitrary
+(well-kinded) assertions <literal>(C t1 ... tn)</literal> subject only to the following rule:
+for each assertion in the context
+<orderedlist>
+<listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
+<listitem><para>Tthe assertion has fewer constructors and variables (taken together
+      and counting repetitions) than the head</para></listitem>
+</orderedlist>
+These restrictions ensure that context reduction terminates: each reduction
+step makes the problem smaller
+constructor.  For example, the following would make the type checker
+loop if it wasn't excluded:
+<programlisting>
+  instance C a => C a where ...
+</programlisting>
+For example, these are OK:

 <programlisting>
 <programlisting>

-  instance Eq (T a a) where ...
-       -- Repeated type variable
+  instance C Int [a]          -- Multiple parameters
+  instance Eq (S [a])         -- Structured type in head

 
 

-  instance Eq (S [a]) where ...
-       -- Structured type
+      -- Repeated type variable in head
+  instance C4 a a => C4 [a] [a] 
+  instance Stateful (ST s) (MutVar s)

 
 

-  instance C Int [a] where ...
-       -- Multiple parameters
+      -- Head can consist of type variables only
+  instance C a
+  instance (Eq a, Show b) => C2 a b
+
+      -- Non-type variables in context
+  instance Show (s a) => Show (Sized s a)
+  instance C2 Int a => C3 Bool [a]
+  instance C2 Int a => C3 [a] b
+</programlisting>
+But these are not:
+<programlisting>
+  instance C a => C a where ...
+      -- Context assertion no smaller than head
+  instance C b b => Foo [b] where ...
+      -- (C b b) has more more occurrences of b than the head

 </programlisting>
 </para>
 </programlisting>
 </para>

+
+<para>
+A couple of useful idioms are these.  First, 
+if one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
+<programlisting>
+  instance C a where
+    op = ... -- Default
+</programlisting>
+
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
+
+
+<programlisting>
+  class (C1 a, C2 a, C3 a) => C a where { }
+
+  instance (C1 a, C2 a, C3 a) => C a where { }
+</programlisting>
+This allows you to write shorter signatures:
+
+<programlisting>
+  f :: C a => ...
+</programlisting>
+instead of
+<programlisting>
+  f :: (C1 a, C2 a, C3 a) => ...
+</programlisting>
+</para>
+</sect3>
+
+<sect3 id="undecidable-instances">
+<title>Undecidable instances</title>
+
+<para>
+Sometimes even the rules of <xref linkend="instance-rules"/> are too onerous.
+Voluminous correspondence on the Haskell mailing list has convinced me
+that it's worth experimenting with more liberal rules.  If you use
+the experimental flag <option>-fallow-undecidable-instances</option>
+<indexterm><primary>-fallow-undecidable-instances
+option</primary></indexterm>, you can use arbitrary
+types in both an instance context and instance head.  Termination is ensured by having a
+fixed-depth recursion stack.  If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with <option>-fcontext-stack</option><emphasis>N</emphasis>.
+</para>
+<para>
+I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
+allowing these idioms interesting idioms.  
+</para>

 </sect3>
 
 </sect3>
 

+

 <sect3 id="instance-overlap">
 <title>Overlapping instances</title>
 <para>
 <sect3 id="instance-overlap">
 <title>Overlapping instances</title>
 <para>

@@ -1835,117 +1921,6 @@ reversed, but it makes sense to me.
 </para>
 </sect3>
 
 </para>
 </sect3>
 

-<sect3 id="undecidable-instances">
-<title>Undecidable instances</title>
-
-<para>An instance declaration must normally obey the following rules:
-<orderedlist>
-<listitem><para>At least one of the types in the <emphasis>head</emphasis> of
-an instance declaration <emphasis>must not</emphasis> be a type variable.
-For example, these are OK:
-
-<programlisting>
-  instance C Int a where ...
-
-  instance D (Int, Int) where ...
-
-  instance E [[a]] where ...
-</programlisting>
-but this is not:
-<programlisting>
-  instance F a where ...
-</programlisting>
-Note that instance heads may contain repeated type variables (<xref linkend="instance-heads"/>).
-For example, this is OK:
-<programlisting>
-  instance Stateful (ST s) (MutVar s) where ...
-</programlisting>
-</para>
-</listitem>
-
-
-<listitem>
-<para>All of the types in the <emphasis>context</emphasis> of
-an instance declaration <emphasis>must</emphasis> be type variables, and
-there must be no repeated type variables in any one constraint.
-Thus
-<programlisting>
-instance C a b => Eq (a,b) where ...
-</programlisting>
-is OK, but
-<programlisting>
-instance C Int b => Foo [b] where ...
-</programlisting>
-is not OK (because of the non-type-variable <literal>Int</literal> in the context), and nor is
-<programlisting>
-instance C b b => Foo [b] where ...
-</programlisting>
-(because of the repeated type variable).
-</para>
-</listitem>
-</orderedlist>
-These restrictions ensure that 
-context reduction terminates: each reduction step removes one type
-constructor.  For example, the following would make the type checker
-loop if it wasn't excluded:
-<programlisting>
-  instance C a => C a where ...
-</programlisting>
-There are two situations in which the rule is a bit of a pain. First,
-if one allows overlapping instance declarations then it's quite
-convenient to have a "default instance" declaration that applies if
-something more specific does not:
-
-
-<programlisting>
-  instance C a where
-    op = ... -- Default
-</programlisting>
-
-
-Second, sometimes you might want to use the following to get the
-effect of a "class synonym":
-
-
-<programlisting>
-  class (C1 a, C2 a, C3 a) => C a where { }
-
-  instance (C1 a, C2 a, C3 a) => C a where { }
-</programlisting>
-
-
-This allows you to write shorter signatures:
-
-
-<programlisting>
-  f :: C a => ...
-</programlisting>
-
-
-instead of
-
-
-<programlisting>
-  f :: (C1 a, C2 a, C3 a) => ...
-</programlisting>
-
-
-Voluminous correspondence on the Haskell mailing list has convinced me
-that it's worth experimenting with more liberal rules.  If you use
-the experimental flag <option>-fallow-undecidable-instances</option>
-<indexterm><primary>-fallow-undecidable-instances
-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head.  Termination is ensured by having a
-fixed-depth recursion stack.  If you exceed the stack depth you get a
-sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack</option><emphasis>N</emphasis>.
-</para>
-<para>
-I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
-allowing these idioms interesting idioms.  
-</para>
-</sect3>
-

 
 </sect2>
 
 
 </sect2>