[Haskell] Should the following program be accepted by ghc?

[Martin Sulzmann]

[Whoever replies next pl move discussion to haskell-cafe]

Bruno Oliveira writes:
 > Hello,
 > 
 > I have been playing with ghc6.8.1 and type families and the following 
 > program is accepted without any type-checking error:
 > 
 > > data a :=: b where
 > >    Eq :: a :=: a
 > 
 > > decomp :: f a :=: f b -> a :=: b
 > > decomp Eq = Eq
 > 
 > However, I find this odd because if you interpret "f" as a function and 
 > ":=:" as equality, then this is saying that
 > 
 > if f a = f b then a = b
 > 
 > but clearly this does not hold in general. For example:
 > 
 > f 1 = 0
 > f 2 = 0
 > 
 > So, we have that "f 1 = f 2" but this does not imply that "1 = 2".
 > 
 > Ofcourse, that before ghc6.8, we add no type-level functions so maybe it 
 > was ok to consider the program above. 

Correct. The decomposition law

f a = f b ==> a = b

applies only to ordinary type constructors (eg list [] etc).
See the System FC paper for more details.

There's a (silent) constraint imposed on the program

 > > decomp :: f a :=: f b -> a :=: b
 > > decomp Eq = Eq

saying that f can only be instantiated with an ordinary type constructor.

As far as I know, GHC obeys this restriction (Manuel, Simon and Tom
who have implemented type families may be able to tell you more).

 > However, with open type functions 
 > the following program is problematic and crashes ghc in style:
 > 
 > > type family K a
 > 
 > > c :: K a :=: K b -> a :=: b
 > > c Eq = Eq
 > 
 > with the following error message:
 > 
 > ghc-6.8.1: panic! (the 'impossible' happened)
 >    (GHC version 6.8.1 for i386-apple-darwin):
 >          Coercion.splitCoercionKindOf
 >      base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv]
 >      <pred>main:Bug.K{tc rom} a{tv aoS} [sk]
 >              ~
 >            main:Bug.K{tc rom} b{tv aoT} [sk]
 > 
 > It seems to me that the "decomp" should be rejected in the first place? 
 > Maybe the fact that "decomp" is accepted is a bug in the compiler?


As said above, you are not allowed to instantiate f with a type family
constructor. Therefore, decomp is fine.

The above program text "crashes" becaue we canNOT deduce that

 K a = K b ==> a =b

The decomposition law does NOT apply to type family constructors.

Indeed, ghc shouldn't crash here and instead provide a more helpful
error message.

Martin


 > Any comments?
 > 
 > Cheers,
 > 
 > Bruno Oliveira
 > _______________________________________________
 > Haskell mailing list
 > Haskell at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell