Opened 2 years ago

Closed 2 years ago

#6002 closed bug (fixed)

GHC 7.4+ thinks class instance is incoherent, 7.0.4 disagrees

Reported by: heisenbug Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: polykinds/T6002 Blocked By:
Blocking: Related Tickets:

Description

Load this file into GHCi:

http://omega.googlecode.com/svn/mosaic/TypeMachinery.lhs?r=1086

With v7.4 (and HEAD) I get:

GHCi, version 7.5.20120410: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling TypeMachinery    ( TypeMachinery.lhs, interpreted )

TypeMachinery.lhs:78:23:
    Overlapping instances for Show (Nat' (Plus n n1))
      arising from a use of `Hide'
    Matching instances:
      instance Show (Nat' a) -- Defined at TypeMachinery.lhs:24:3
    There exists a (perhaps superclass) match:
      from the context (Show (Nat' n))
        bound by a pattern with constructor
                   Hide :: forall (a :: * -> *) n. Show (a n) => a n -> Hidden a,
                 in an equation for `+'
        at TypeMachinery.lhs:78:5-10
      or from (Show (Nat' n1))
        bound by a pattern with constructor
                   Hide :: forall (a :: * -> *) n. Show (a n) => a n -> Hidden a,
                 in an equation for `+'
        at TypeMachinery.lhs:78:14-19
    (The choice depends on the instantiation of `n, n1'
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: Hide
    In the expression: Hide $ plus a b
    In an equation for `+': (Hide a) + (Hide b) = Hide $ plus a b
Failed, modules loaded: none.

With 7.0.4 all compiles (and runs) correctly.

Change History (5)

comment:1 Changed 2 years ago by simonpj

  • Difficulty set to Unknown

This is a very delicate case.
Suppose we have these definitions.

  data Nat a = ... 
  instance Show (Nat a) where ...

  data Hidden a where
    Hide :: Show (Nat a) => Nat a -> Hidden a

  type family Plus m n :: *
  plus :: Nat a -> Nat b -> Nat (Plus a b)

and typecheck this function

  f (Hide a) (Hide b) = Hide (plus a b)

So we have

  Given:  d1 :: Show (Nat a1)
          d2 :: Show (Nat a2)

  Wanted: dw :: Show (Nat (Plus a1 a2))

Now, if Plus a1 a2 evaluated to a1, we would satisfy dw with d1; and similarly
if it evaluated to a2. Otherwise we should use the top-level instance.

The trouble is that it's hard to perform negative reasoning: we rightly refrain from
using the top level instance for Show (Nat a), in case the (Plus a1 a2) does later evaluate, and it's hard
to get to the point where we say "ok, it definitely doesn't evaluate to a1 or a2,
so use the top-level instance".

I'm not sure how to "fix" this; it does seem tricky to solve type
class constraints coherently, in the presence of (a) existentials
and (b) type functions.

I was going to say that a workaround is to use -XIncoherentInstances; but in fact
that does not currently work, although it should. I'll fix that part.

comment:2 Changed 2 years ago by heisenbug

I tried IncoherentInstances but the error message changed instead of disappearing.

I ask myself, how did this work in 7.0.4? Are we checking constraints more aggressively recently?

Also I have a user-defined kinds version here, maybe the inference logic would be simpler when no phantom types are involved? http://omega.googlecode.com/svn/mosaic/TypeMachinery.kinds.lhs

Thanks for looking into this!

comment:3 Changed 2 years ago by simonpj

Reminder: I said "I was going to say that a workaround is to use -XIncoherentInstances; but in fact that does not currently work, although it should. I'll fix that part."

I don't know why 7.0.4 accepted it. But HEAD's rejection is for a good reason, as I explain above.

Nothing to do with phantom types; the issue here, as I say above, is what the type-function application (Plus a1 a2) might evaluate to.

comment:4 Changed 2 years ago by simonpj@…

commit 6bf815982df88468035593a07b0be593d1326af2

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri Apr 13 12:54:44 2012 +0100

    Allow overlaps when -XIncoherentInstances is in force
    
    This change allows a top-level instance to be used even if there is
    a (potentially) overlapping local given.  Which isn't fab, but it is
    what IncoherentInstances is *for*.
    
    This fixes the bug part of Trac #6002.

 compiler/typecheck/TcInteract.lhs |   18 ++++++++++--------
 1 files changed, 10 insertions(+), 8 deletions(-)

comment:5 Changed 2 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to polykinds/T6002

I've added a test that -XIncoherentInstances makes the code be accepted, so I'll close the ticket.

Simon

Note: See TracTickets for help on using tickets.