Commit 59c9c122 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Loosen the rules for instance declarations (Part 2)

Tidying up to Ross's  patch, plus adding documenation for it.
parent 1cdafe99
......@@ -13,12 +13,9 @@ import TcBinds ( mkPragFun, tcPrags, badBootDeclErr )
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 )
......@@ -33,8 +30,7 @@ import Type ( zipOpenTvSubst, substTheta, substTys )
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 )
......@@ -186,32 +182,25 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags))
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.
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}
......@@ -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.
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)
......
......@@ -33,8 +33,7 @@ module TcMType (
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
checkInstTermination,
checkValidInstHead, checkValidInstance, checkAmbiguity,
arityErr,
--------------------------------
......@@ -90,10 +89,10 @@ import Kind ( isSubKind )
-- others:
import TcRnMonad -- TcType, amongst others
import FunDeps ( grow )
import FunDeps ( grow, checkInstFDs )
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
......@@ -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
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
......@@ -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
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
......@@ -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
......@@ -1116,13 +1132,8 @@ This is only needed with -fglasgow-exts, as Haskell 98 restrictions
(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
......@@ -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")
-- 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]
......@@ -1164,7 +1175,7 @@ fvPred :: PredType -> [TyVar]
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
......
......@@ -1673,38 +1673,124 @@ class like this:
<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>
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.
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>
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>
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>
<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 id="instance-overlap">
<title>Overlapping instances</title>
<para>
......@@ -1835,117 +1921,6 @@ reversed, but it makes sense to me.
</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>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment