Implement the final change to INCOHERENT from Trac #9242
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 8 Aug 2014 07:35:14 +0000 (08:35 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 8 Aug 2014 08:04:31 +0000 (09:04 +0100)
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.

compiler/types/InstEnv.lhs
docs/users_guide/glasgow_exts.xml
libraries/base/Data/Typeable/Internal.hs
testsuite/tests/typecheck/should_fail/Tcfail218_Help.hs [deleted file]
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail218.hs
testsuite/tests/typecheck/should_fail/tcfail218.stderr

index aba2d3d..708fef1 100644 (file)
@@ -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]
index 00f4315..de0d494 100644 (file)
@@ -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>
@@ -5087,13 +5077,6 @@ 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:
 
 <itemizedlist>
@@ -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> 
index 7c12cea..b67f88c 100644 (file)
@@ -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
diff --git a/testsuite/tests/typecheck/should_fail/Tcfail218_Help.hs b/testsuite/tests/typecheck/should_fail/Tcfail218_Help.hs
deleted file mode 100644 (file)
index e5ee76d..0000000
+++ /dev/null
@@ -1,7 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-
-module Tcfail218_Help where
-
-class C a b where foo :: (a,b)
-
-instance C [Int] b where foo = undefined
index cf2af30..b528047 100644 (file)
@@ -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, [''])
index ed05459..9a5f4ce 100644 (file)
@@ -1,12 +1,22 @@
-{-# 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
+
index 7978004..efb6c4c 100644 (file)
@@ -1,10 +1,10 @@
 
-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