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

[Derek Elkins]

On Wed, 2008-01-16 at 09:18 +0000, J.N. Oliveira wrote:
> On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
> 
> > 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
> 
> This is saying that  f  is injective. So perhaps the standard  
> interpretation leads implicitly to this class of functions.

Just like data constructors, type constructors are injective. f a
doesn't simplify and so essentially you have structural equality of the
type terms thus f a = f b is -equivalent- to a = b.  Obviously type
functions change this, just like normal value functions do at the value
level.