Tidying up to Ross's patch, plus adding documenation for it.
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 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 )
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}
-- 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)
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, instTypeErr, checkAmbiguity,
- checkInstTermination,
+ checkValidInstHead, checkValidInstance, checkAmbiguity,
arityErr,
--------------------------------
-- 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
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_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
%* *
%************************************************************************
+
+\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
(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
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]
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
<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>) => <replaceable>class</replaceable> <replaceable>type</replaceable><subscript>1</subscript> ... <replaceable>type</replaceable><subscript>m</subscript> where ...
+</screen>
+The part before the "<literal>=></literal>" is the
+<emphasis>context</emphasis>, while the part after the
+"<literal>=></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>=></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>
</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>
projects / ghc-hetmet.git / commitdiff