[Haskell-cafe] Deducing Show for GADTs

[Niklas Broberg]

On 6/28/06, David Roundy <droundy at darcs.net> wrote:
> On Wed, Jun 28, 2006 at 11:52:51AM +0200, Joel Bjrnson wrote:
> > Hi. I came a cross the following phenomena which, at least to me,
> > occurs kind of awkward. The code below:
> >
> > data MyData a  where
> >  DC1 :: (Show a ) => a -> MyData a
>
> GADTs don't yet work right with classes.  :( The above, however,
> doesn't need to be expressed as a GADT, I believe you can write
> something like:
>
> data MyData a = (forall a. Show a) => DC1 a
>
> which (this is untested) should do what you want.

Only if "what he wants" is something that type checks, but doesn't do
the same thing. ;-)
In Joel's definition of MyData, values constructed with DC1 applied to
a value of type b will have type MyData b. In your definition they
will have type MyData a, for any a. In other words, your definition
would be identical to the GADT

data MyData a where
 DC1 :: forall a b . (Show b) => b -> MyData a


As to Joel's question, this seems really really weird. In particular
since adding the completely useless wrapper type solves the problem.
In fact, giving DC1 any return type other than MyData a solves the
problem. This has to be a bug of some sort.

/Niklas