Commit 8e512635 authored by Ross Paterson's avatar Ross Paterson
Browse files

Loosen the rules for instance declarations (Part 3)

Relax the restrictions on derived instances in the same way, so we
can write

	data MinHeap h a = H a (h a) deriving (Show)
parent e68a5b60
......@@ -727,7 +727,7 @@ solveDerivEqns overlap_flag orig_eqns
gen_soln (_, clas, tc,tyvars,deriv_rhs)
= setSrcSpan (srcLocSpan (getSrcLoc tc)) $
addErrCtxt (derivCtxt (Just clas) tc) $
tcSimplifyDeriv tyvars deriv_rhs `thenM` \ theta ->
tcSimplifyDeriv tc tyvars deriv_rhs `thenM` \ theta ->
returnM (sortLe (<=) theta) -- Canonicalise before returning the soluction
------------------------------------------------------------------
......
......@@ -34,6 +34,7 @@ module TcMType (
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance, checkAmbiguity,
checkInstTermination,
arityErr,
--------------------------------
......@@ -97,6 +98,7 @@ import Util ( nOfThem, isSingleton, notNull )
import ListSetOps ( removeDups )
import Outputable
import Control.Monad ( when )
import Data.List ( (\\) )
\end{code}
......@@ -1107,18 +1109,19 @@ instTypeErr pp_ty msg
\begin{code}
checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
checkValidInstance tyvars theta clas inst_tys
= do { dflags <- getDOpts
= do { gla_exts <- doptM Opt_GlasgowExts
; undecidable_ok <- doptM Opt_AllowUndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- Check that instance inference will termainate
-- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
; checkInstTermination dflags theta inst_tys
; when (gla_exts && not undecidable_ok) $
checkInstTermination theta inst_tys
-- The Coverage Condition
; checkTc (dopt Opt_AllowUndecidableInstances dflags ||
checkInstCoverage clas inst_tys)
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
}
where
......@@ -1133,11 +1136,9 @@ This is only needed with -fglasgow-exts, as Haskell 98 restrictions
(which have already been checked) guarantee termination.
\begin{code}
checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM ()
checkInstTermination dflags theta tys
| not (dopt Opt_GlasgowExts dflags) = returnM ()
| dopt Opt_AllowUndecidableInstances dflags = returnM ()
| otherwise = do
checkInstTermination :: ThetaType -> [TcType] -> TcM ()
checkInstTermination theta tys
= do
mappM_ (check_nomore (fvTypes tys)) theta
mappM_ (check_smaller (sizeTypes tys)) theta
......
......@@ -21,6 +21,7 @@ module TcSimplify (
#include "HsVersions.h"
import {-# SOURCE #-} TcUnify( unifyType )
import TypeRep ( Type(..) )
import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
......@@ -41,7 +42,8 @@ import Inst ( lookupInst, LookupInstResult(..),
import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
lclEnvElts, tcMetaTy )
import InstEnv ( lookupInstEnv, classInstances, pprInstances )
import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars,
checkAmbiguity, checkInstTermination )
import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType,
mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
......@@ -49,6 +51,7 @@ import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType,
import TcIface ( checkWiredInTyCon )
import Id ( idType, mkUserLocal )
import Var ( TyVar )
import TyCon ( TyCon )
import Name ( Name, getOccName, getSrcLoc )
import NameSet ( NameSet, mkNameSet, elemNameSet )
import Class ( classBigSig, classKey )
......@@ -2225,11 +2228,12 @@ a,b,c are type variables. This is required for the context of
instance declarations.
\begin{code}
tcSimplifyDeriv :: [TyVar]
tcSimplifyDeriv :: TyCon
-> [TyVar]
-> ThetaType -- Wanted
-> TcM ThetaType -- Needed
tcSimplifyDeriv tyvars theta
tcSimplifyDeriv tc tyvars theta
= tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
-- The main loop may do unification, and that may crash if
-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
......@@ -2238,6 +2242,7 @@ tcSimplifyDeriv tyvars theta
simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
ASSERT( null frees ) -- reduceMe never returns Free
doptM Opt_GlasgowExts `thenM` \ gla_exts ->
doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
let
tv_set = mkVarSet tvs
......@@ -2247,15 +2252,7 @@ tcSimplifyDeriv tyvars theta
= let pred = dictPred dict -- reduceMe squashes all non-dicts
in isEmptyVarSet (tyVarsOfPred pred)
-- Things like (Eq T) are bad
|| (not undecidable_ok && not (isTyVarClassPred pred))
-- The returned dictionaries should be of form (C a b)
-- (where a, b are type variables).
-- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
-- but note that risks non-termination in the 'deriving' context-inference
-- fixpoint loop. It is useful for situations like
-- data Min h a = E | M a (h a)
-- which gives the instance decl
-- instance (Eq a, Eq (h a)) => Eq (Min h a)
|| (not gla_exts && not (isTyVarClassPred pred))
simpl_theta = map dictPred ok_insts
weird_preds = [pred | pred <- simpl_theta
......@@ -2269,11 +2266,19 @@ tcSimplifyDeriv tyvars theta
rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
-- This reverse-mapping is a Royal Pain,
-- but the result should mention TyVars not TcTyVars
head_ty = TyConApp tc (map TyVarTy tvs)
in
addNoInstanceErrs Nothing [] bad_insts `thenM_`
mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
checkAmbiguity tvs simpl_theta tv_set `thenM_`
-- Check instance termination as for user-declared instances.
-- unless we had -fallow-undecidable-instances (which risks
-- non-termination in the 'deriving' context-inference fixpoint
-- loop).
ifM (gla_exts && not undecidable_ok)
(checkInstTermination simpl_theta [head_ty]) `thenM_`
returnM (substTheta rev_env simpl_theta)
where
doc = ptext SLIT("deriving classes for a data type")
......
......@@ -1933,8 +1933,9 @@ 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.
Furthermore, the assertions in the context of the instance declaration
must be of the form <literal>C a</literal> where <literal>a</literal>
is a type variable that occurs in the head.
</para>
<para>
The <option>-fglasgow-exts</option> flag loosens these restrictions
......@@ -1963,7 +1964,7 @@ corresponding type in the instance declaration.
</para></listitem>
</orderedlist>
These restrictions ensure that context reduction terminates: each reduction
step makes the problem smaller
step makes the problem smaller by at least one
constructor. For example, the following would make the type checker
loop if it wasn't excluded:
<programlisting>
......@@ -1989,34 +1990,52 @@ For example, these are OK:
</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 ...
instance C a => C a where ...
-- (C b b) has more more occurrences of b than the head
instance C b b => Foo [b] where ...
</programlisting>
</para>
<para>
A couple of useful idioms are these. First,
if one allows overlapping instance declarations then it's quite
The same restrictions apply to instances generated by
<literal>deriving</literal> clauses. Thus the following is accepted:
<programlisting>
data MinHeap h a = H a (h a)
deriving (Show)
</programlisting>
because the derived instance
<programlisting>
instance (Show a, Show (h a)) => Show (MinHeap h a)
</programlisting>
conforms to the above rules.
</para>
<para>
A useful idiom permitted by the above rules is as follows.
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>
</para>
</sect3>
Second, sometimes you might want to use the following to get the
effect of a "class synonym":
<sect3 id="undecidable-instances">
<title>Undecidable instances</title>
<para>
Sometimes even the rules of <xref linkend="instance-rules"/> are too onerous.
For example, 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>
......@@ -2024,17 +2043,9 @@ 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.
For example, with functional dependencies (<xref
linkend="functional-dependencies"/>)
it is tempting to introduce type variables in the context that do not appear in
The restrictions on functional dependencies (<xref
linkend="functional-dependencies"/>) are particularly troublesome.
It is tempting to introduce type variables in the context that do not appear in
the head, something that is excluded by the normal rules. For example:
<programlisting>
class HasConverter a b | a -> b where
......
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