Opened 3 years ago

Closed 3 years ago

#5516 closed bug (invalid)

Universally quantified GADT context leads to overlapping instance

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

Description

This example from comment:8:ticket:2893 works in GHC 7.0.3, but fails in GHC master 7.3.20110927:

{-# LANGUAGE GADTs, Rank2Types, FlexibleContexts #-}

class Foo a where
    foo :: a -> String

instance Foo [b] where
    foo = show . length

data FooDict a where
    FooDict :: Foo a => FooDict a

f :: (forall b. FooDict [b]) -> String
f FooDict = foo "Hello" ++ foo [1, 2, 3]

use_foo :: String
use_foo = f FooDict

with this error:

foo.hs:13:28:
    Overlapping instances for Foo [t0]
      arising from a use of `foo'
    Matching instances: instance Foo [b] -- Defined at foo.hs:6:10
    Matching givens (or their superclasses):
      (Foo [b_a])
        bound by a pattern with constructor
                   FooDict :: forall a. Foo a => FooDict a,
                 in an equation for `f'
        at foo.hs:13:3-9
    (The choice depends on the instantiation of `t0')
    In the second argument of `(++)', namely `foo [1, 2, 3]'
    In the expression: foo "Hello" ++ foo [1, 2, 3]
    In an equation for `f': f FooDict = foo "Hello" ++ foo [1, 2, 3]

Change History (4)

comment:1 Changed 3 years ago by batterseapower

FYI Simon pointed out that my example from 2893 wasn't actually making use of the GADT-carried dictionary. Instead, it was just using the top level instance decl.

The story is that GHC can infer polymorphic evidence but not make use of it, even with this sort of GADT trick. If you explicitly scrutinise the polymorphic GADT at a monomorphic type GHC *can* make use of the evidence, however.

comment:2 Changed 3 years ago by simonpj

I'm not sure what the issue is here. Is there a bug? Can we just close this?

Simon

comment:3 Changed 3 years ago by andersk

Even if GHC is unable to use the polymorphic evidence, I feel like its presence should not cause an error when the code would otherwise have worked. If that’s true, this is a regression from 7.0. But probably nobody writes code like this, so I guess the question is whether there’s now a good reason to disallow it.

comment:4 Changed 3 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

The issue is that there genuinely are two places where the (Foo [t]) constraint could be satisfied:

  • From the FooDict constructor
  • From the instance declaration

And which to use depends on how t is instantiated. So this is a dodgy situation and I'm content that it flags an error. If we have real use cases where it becomes painful we can look again.

Simon

Note: See TracTickets for help on using tickets.