GADT + Newtype deriving = Erroneous errors

[Stefan O'Rear]

On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
> Stefan O'Rear wrote:
> > This code causes GHC to incorrectly fail - the case *is* reachable.
> > (I invented this technique in an attempt to directly access the
> > internal System FC newtype coercion; it promised until a few minutes
> > ago to solve all the EnumMap performance concerns.)
> > 
> > stefan at stefans:/tmp$ cat A.lhs
> >> {-# OPTIONS_GHC -fglasgow-exts #-}
> >>
> >> data IsIntT x where IsIntT :: IsIntT Int
> >>
> >> class IsIntC a where isInt :: IsIntT a
> >> instance IsIntC Int where isInt = IsIntT
> >>
> >> newtype Foo = Foo Int deriving(IsIntC)
> >>
> >> x :: IsIntT Foo -> Int
> >> x IsIntT = (Foo 2) + 2
> 
> IsIntT Foo is a concrete type.
> IsIntT has concrete type IsInt Int.
> These types cannot possibly match.

Sure they can.  This is an attempt to torture-test GHC.  Using newtype
deriving, I have constructed a non-bottom value of type IsIntT Foo.
Thus, the value is evidence of the fact that the newtype is isomorphic
to the base type.  In the language of GHC HEAD, it is a value-level
reification of the coercion used to implement the newtype in System FC
(although the same bogus error occurs with 6.4.2, 6.6, 6.7.20070213,
6.7.20070223, and 6.7.20070323).  GHC seems to be making the
(unwaranted!) assumption that distinct concrete types can never be
unified - but they CAN, and the compiler is failing my torture test.
(BTW, why is the inaccessible alternative an error rather than a
warning?)

> Note that (Foo 2) + 2 is an attempt to add a Foo and an Int, which cannot
> possibly compile.  So I replaced it with just a 2.

Why not?  They are the same type, and I have Curry-Howard proof of this fact.

Stefan