[Haskell] Should the following program be accepted by ghc?
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Wed Jan 16 00:02:43 EST 2008
[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
More information about the Haskell
mailing list