Commit dff0623d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Implement the final change to INCOHERENT from Trac #9242

The change here is to make INCOHERENT slightly more permissive:

  if the selected candidate is incoherent
  then ignore all unifying candidates

This allows us to move the {-# INCOHERENT #-} pragma from
  from   instance Typeable (f a)
  to     Typeable (n:Nat) and Typable (s:Symbol)
where it belongs, and where Trac #9242 said it should be.

I don't think this will affect anyone.

I've updated the user manual.
parent 7d52e628
......@@ -613,21 +613,28 @@ lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env
-> ClsInstLookupResult
-- ^ See Note [Rules for instance lookup]
lookupInstEnv (pkg_ie, home_ie) cls tys
= (safe_matches, all_unifs, safe_fail)
= (final_matches, final_unifs, safe_fail)
where
(home_matches, home_unifs) = lookupInstEnv' home_ie cls tys
(pkg_matches, pkg_unifs) = lookupInstEnv' pkg_ie cls tys
all_matches = home_matches ++ pkg_matches
all_unifs = home_unifs ++ pkg_unifs
pruned_matches = foldr insert_overlapping [] all_matches
(safe_matches, safe_fail) = if length pruned_matches == 1
then check_safe (head pruned_matches) all_matches
else (pruned_matches, False)
-- Even if the unifs is non-empty (an error situation)
-- we still prune the matches, so that the error message isn't
-- misleading (complaining of multiple matches when some should be
-- overlapped away)
(final_matches, safe_fail)
= case pruned_matches of
[match] -> check_safe match all_matches
_ -> (pruned_matches, False)
-- If the selected match is incoherent, discard all unifiers
final_unifs = case final_matches of
(m:_) | is_incoherent m -> []
_ -> all_unifs
-- NOTE [Safe Haskell isSafeOverlap]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- We restrict code compiled in 'Safe' mode from overriding code
......@@ -660,45 +667,53 @@ lookupInstEnv (pkg_ie, home_ie) cls tys
in (la && lb) || (nameModule na == nameModule nb)
---------------
is_incoherent :: InstMatch -> Bool
is_incoherent (inst, _) = overlapMode (is_flag inst) == Incoherent
---------------
insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
-- ^ Add a new solution, knocking out strictly less specific ones
-- See Note [Rules for instance lookup]
insert_overlapping new_item [] = [new_item]
insert_overlapping new_item (item:items)
| new_beats_old && old_beats_new = item : insert_overlapping new_item items
-- Duplicate => keep both for error report
| new_beats_old = insert_overlapping new_item items
-- Keep new one
| old_beats_new = item : items
-- Keep old one
| incoherent new_item = item : items -- note [Incoherent instances]
-- Keep old one
| incoherent item = new_item : items
-- Keep new one
| otherwise = item : insert_overlapping new_item items
-- Keep both
insert_overlapping new_item (old_item : old_items)
| new_beats_old -- New strictly overrides old
, not old_beats_new
, new_item `can_override` old_item
= insert_overlapping new_item old_items
| old_beats_new -- Old strictly overrides new
, not new_beats_old
, old_item `can_override` new_item
= old_item : old_items
-- Discard incoherent instances; see Note [Incoherent instances]
| is_incoherent old_item -- Old is incoherent; discard it
= insert_overlapping new_item old_items
| is_incoherent new_item -- New is incoherent; discard it
= old_item : old_items
-- Equal or incomparable, and neither is incoherent; keep both
| otherwise
= old_item : insert_overlapping new_item old_items
where
new_beats_old = new_item `beats` item
old_beats_new = item `beats` new_item
incoherent (inst, _) = overlapMode (is_flag inst) == Incoherent
new_beats_old = new_item `more_specific_than` old_item
old_beats_new = old_item `more_specific_than` new_item
-- `instB` can be instantiated to match `instA`
instA `moreSpecificThan` instB =
isJust (tcMatchTys (mkVarSet (is_tvs instB))
(is_tys instB) (is_tys instA))
(instA, _) `beats` (instB, _)
= overlap_ok && (instA `moreSpecificThan` instB)
where
{- Overlap permitted if either the more specific instance
is marked as overlapping, or the more general one is
marked as overlappable.
Latest change described in: Trac #9242.
Previous change: Trac #3877, Dec 10. -}
overlap_ok = hasOverlappingFlag (overlapMode (is_flag instA))
|| hasOverlappableFlag (overlapMode (is_flag instB))
-- or the two are equal
(instA,_) `more_specific_than` (instB,_)
= isJust (tcMatchTys (mkVarSet (is_tvs instB))
(is_tys instB) (is_tys instA))
(instA, _) `can_override` (instB, _)
= hasOverlappingFlag (overlapMode (is_flag instA))
|| hasOverlappableFlag (overlapMode (is_flag instB))
-- Overlap permitted if either the more specific instance
-- is marked as overlapping, or the more general one is
-- marked as overlappable.
-- Latest change described in: Trac #9242.
-- Previous change: Trac #3877, Dec 10.
\end{code}
Note [Incoherent instances]
......
......@@ -5025,38 +5025,30 @@ In general, as discussed in <xref linkend="instance-resolution"/>,
<emphasis>GHC requires that it be unambiguous which instance
declaration
should be used to resolve a type-class constraint</emphasis>.
This behaviour
can be modified by two flags: <option>-XOverlappingInstances</option>
<indexterm><primary>-XOverlappingInstances
</primary></indexterm>
and <option>-XIncoherentInstances</option>
<indexterm><primary>-XIncoherentInstances
</primary></indexterm>, as this section discusses. Both these
flags are dynamic flags, and can be set on a per-module basis, using
an <literal>LANGUAGE</literal> pragma if desired (<xref linkend="language-pragma"/>).</para>
GHC also provides a way to to loosen
the instance resolution, by
allowing more than one instance to match, <emphasis>provided there is a most
specific one</emphasis>. Moreover, it can be loosened further, by allowing more than one instance to match
irespective of whether there is a most specific one.
This section gives the details.
</para>
<para>
In addition, it is possible to specify the overlap behavior for individual
To control the choice of instance, it is possible to specify the overlap behavior for individual
instances with a pragma, written immediately after the
<literal>instance</literal> keyword. The pragma may be one of:
<literal>OVERLAPPING</literal>,
<literal>OVERLAPPABLE</literal>,
<literal>OVERLAPS</literal>,
or <literal>INCOHERENT</literal>. An explicit pragma on an instance
takes precedence over the default specified with a flag or
a <literal>LANGUAGE</literal> pragma.
<literal>{-# OVERLAPPING #-}</literal>,
<literal>{-# OVERLAPPABLE #-}</literal>,
<literal>{-# OVERLAPS #-}</literal>,
or <literal>{-# INCOHERENT #-}</literal>.
</para>
<para>
The <option>-XOverlappingInstances</option> flag instructs GHC to loosen
the instance resolution described in <xref linkend="instance-resolution"/>, by
allowing more than one instance to match, <emphasis>provided there is a most
specific one</emphasis>. The <option>-XIncoherentInstances</option> flag
further loosens the resolution, by allowing more than one instance to match,
irespective of whether there is a most specific one.
The <option>-XIncoherentInstances</option> flag implies the
<option>-XOverlappingInstances</option> flag, but not vice versa.
The matching behaviour is also influenced by two module-level language extension flags: <option>-XOverlappingInstances</option>
<indexterm><primary>-XOverlappingInstances
</primary></indexterm>
and <option>-XIncoherentInstances</option>
<indexterm><primary>-XIncoherentInstances
</primary></indexterm>. These flags are now deprecated (since GHC 7.10) in favour of
the fine-grained per-instance pragmas.
</para>
<para>
......@@ -5064,15 +5056,13 @@ A more precise specification is as follows.
The willingness to be overlapped or incoherent is a property of
the <emphasis>instance declaration</emphasis> itself, controlled as follows:
<itemizedlist>
<listitem><para>An instance is <emphasis>incoherent</emphasis> if it has an <literal>INCOHERENT</literal> pragma, or if it appears in a module compiled with <literal>-XIncoherentInstances</literal>.
<listitem><para>An instance is <emphasis>incoherent</emphasis> if: it has an <literal>INCOHERENT</literal> pragma; or if the instance has no pragma and it appears in a module compiled with <literal>-XIncoherentInstances</literal>.
</para></listitem>
<listitem><para>An instance is <emphasis>overlappable</emphasis> if it has an <literal>OVERLAPPABLE</literal> or <literal>OVERLAPS</literal> pragma, or if it appears in a module compiled with <literal>-XOverlappingInstances</literal>, or if the instance is incoherent.
<listitem><para>An instance is <emphasis>overlappable</emphasis> if: it has an <literal>OVERLAPPABLE</literal> or <literal>OVERLAPS</literal> pragma; or if the instance has no pragma and it appears in a module compiled with <literal>-XOverlappingInstances</literal>; or if the instance is incoherent.
</para></listitem>
<listitem><para>An instance is <emphasis>overlapping</emphasis> if it has an <literal>OVERLAPPING</literal> or <literal>OVERLAPS</literal> pragma, or if it appears in a module compiled with <literal>-XOverlappingInstances</literal>, or if the instance is incoherent.
<listitem><para>An instance is <emphasis>overlapping</emphasis> if: it has an <literal>OVERLAPPING</literal> or <literal>OVERLAPS</literal> pragma; or if the instance has no pragma and it appears in a module compiled with <literal>-XOverlappingInstances</literal>; or if the instance is incoherent.
</para></listitem>
</itemizedlist>
The <option>-XOverlappingInstances</option> language extension is now deprecated in favour
per-instance pragmas.
</para>
<para>
......@@ -5086,13 +5076,6 @@ that is, the target constraint is a substitution instance of I. These
instance declarations are the <emphasis>candidates</emphasis>.
</para></listitem>
<listitem><para>
Find all <emphasis>non-candidate</emphasis> instances
that <emphasis>unify</emphasis> with the target constraint.
Such non-candidates instances might match when the target constraint is further
instantiated. If all of them are incoherent, proceed; if not, the search fails.
</para></listitem>
<listitem><para>
Eliminate any candidate IX for which both of the following hold:
......@@ -5101,22 +5084,37 @@ Eliminate any candidate IX for which both of the following hold:
that is, IY is a substitution instance of IX but not vice versa.
</para></listitem>
<listitem><para>
Either IX is <emphasis>overlappable</emphasis> or IY is
<emphasis>overlapping</emphasis>.
Either IX is <emphasis>overlappable</emphasis>, or IY is
<emphasis>overlapping</emphasis>. (This "either/or" design, rather than a "both/and" design,
allow a client to deliberately override an instance from a library, without requiring a change to the library.)
</para></listitem>
</itemizedlist>
</para>
</listitem>
<listitem><para>
If exactly one non-incoherent candidate remains, pick it. If all
remaining candidates are incoherent, pick an arbitary
one. Otherwise fail.
If exactly one non-incoherent candidate remains, select it. If all
remaining candidates are incoherent, select an arbitary
one. Otherwise the search fails (i.e. when more than one surviving candidate is not incoherent).
</para></listitem>
<listitem><para>
If the selected candidate (from the previous step) is incoherent, the search succeeds, returning that candidate.
</para></listitem>
<listitem><para>
If not, find all instances that <emphasis>unify</emphasis> with the target
constraint, but do not <emphasis>match</emphasis> it.
Such non-candidate instances might match when the target constraint is further
instantiated. If all of them are incoherent, the search succeeds, returning the selected candidate;
if not, the search fails.
</para></listitem>
</itemizedlist>
Notice that these rules are not influenced by flag settings in the client module, where
the instances are <emphasis>used</emphasis>.
These rules make it possible for a library author to design a library that relies on
overlapping instances without the library client having to know.
overlapping instances without the client having to know.
</para>
<para>
Errors are reported <emphasis>lazily</emphasis> (when attempting to solve a constraint), rather than <emphasis>eagerly</emphasis>
......
......@@ -263,30 +263,15 @@ type Typeable7 (a :: * -> * -> * -> * -> * -> * -> * -> *) = Typeable a
{-# DEPRECATED Typeable7 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-- | Kind-polymorphic Typeable instance for type application
instance {-# INCOHERENT #-} (Typeable s, Typeable a) => Typeable (s a) where
instance (Typeable s, Typeable a) => Typeable (s a) where
-- See Note [The apparent incoherence of Typable]
typeRep# = \_ -> rep -- Note [Memoising typeOf]
where !ty1 = typeRep# (proxy# :: Proxy# s)
!ty2 = typeRep# (proxy# :: Proxy# a)
!rep = ty1 `mkAppTy` ty2
{- Note [The apparent incoherence of Typable] See Trac #9242
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason we have INCOHERENT here is because we also have instances
instance Typeable (x::Nat)
instance Typeable (y::Symbol)
If we have
[Wanted] Typeable (a :: Nat)
we should pick the (x::Nat) instance, even though the instance
matching rules would worry that 'a' might later be instantiated to
(f b), for some f and b. But we type theorists know that there are no
type constructors f of kind blah -> Nat, so this can never happen and
it's safe to pick the second instance.
Note [Memoising typeOf]
~~~~~~~~~~~~~~~~~~~~~~~
{- Note [Memoising typeOf]
~~~~~~~~~~~~~~~~~~~~~~~~~~
See #3245, #9203
IMPORTANT: we don't want to recalculate the TypeRep once per call with
......@@ -462,7 +447,19 @@ lifted types with infinitely many inhabitants. Indeed, `Nat` is
isomorphic to (lifted) `[()]` and `Symbol` is isomorphic to `[Char]`.
-}
instance KnownNat n => Typeable (n :: Nat) where
{- Note [The apparent incoherence of Typable] See Trac #9242
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason we have INCOHERENT on Typeable (n:Nat) and Typeable (s:Symbol)
because we also have an instance Typable (f a). Now suppose we have
[Wanted] Typeable (a :: Nat)
we should pick the (x::Nat) instance, even though the instance
matching rules would worry that 'a' might later be instantiated to
(f b), for some f and b. But we type theorists know that there are no
type constructors f of kind blah -> Nat, so this can never happen and
it's safe to pick the second instance. -}
instance {-# INCOHERENT #-} KnownNat n => Typeable (n :: Nat) where
-- See Note [The apparent incoherence of Typable]
-- See #9203 for an explanation of why this is written as `\_ -> rep`.
typeRep# = \_ -> rep
......@@ -480,7 +477,7 @@ instance KnownNat n => Typeable (n :: Nat) where
mk a b c = a ++ " " ++ b ++ " " ++ c
instance KnownSymbol s => Typeable (s :: Symbol) where
instance {-# INCOHERENT #-} KnownSymbol s => Typeable (s :: Symbol) where
-- See Note [The apparent incoherence of Typable]
-- See #9203 for an explanation of why this is written as `\_ -> rep`.
typeRep# = \_ -> rep
......
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module Tcfail218_Help where
class C a b where foo :: (a,b)
instance C [Int] b where foo = undefined
......@@ -243,10 +243,7 @@ test('tcfail214', normal, compile_fail, [''])
test('tcfail215', normal, compile_fail, [''])
test('tcfail216', normal, compile_fail, [''])
test('tcfail217', normal, compile_fail, [''])
test('tcfail218',
extra_clean(['Tcfail218_Help.o','Tcfail218_Help.hi']),
multimod_compile_fail, ['tcfail218','-v0'])
test('tcfail218', normal, compile_fail, [''])
test('SilentParametersOverlapping', normal, compile_fail, [''])
test('FailDueToGivenOverlapping', normal, compile_fail, [''])
test('LongWayOverlapping', normal, compile_fail, [''])
......
{-# LANGUAGE IncoherentInstances, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
import Tcfail218_Help
module Tcfail218 where
instance C [a] b where foo = undefined
instance C a Int where foo = undefined
class C a b where foo :: (a,b)
-- Should fail, as a more specific, unifying but not matching, non-incoherent instance exists.
x :: ([a],b)
instance C [Int] Bool where foo = undefined
instance C [a] b where foo = undefined
instance {-# INCOHERENT #-} C a Int where foo = undefined
x :: ([a],Bool)
-- Needs C [a] b.
-- Should fail, as a more specific, unifying but not matching
-- non-incoherent instance exists, namely C [Int] Bool
x = foo
main = return ()
-- Needs C [a] Int.
-- Should succeed, because two instances match, but one is incoherent
y :: ([a],Int)
y = foo
tcfail218.hs:10:5:
Overlapping instances for C [a] b arising from a use of ‘foo’
tcfail218.hs:16:5:
Overlapping instances for C [a] Bool arising from a use of ‘foo’
Matching instances:
instance [incoherent] C [a] b -- Defined at tcfail218.hs:5:10
instance C [Int] b -- Defined at Tcfail218_Help.hs:7:10
(The choice depends on the instantiation of ‘a, b
instance C [a] b -- Defined at tcfail218.hs:8:29
instance C [Int] Bool -- Defined at tcfail218.hs:7:29
(The choice depends on the instantiation of ‘a’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
In the expression: foo
......
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