[Haskell-cafe] Injective type families for GHC

[adam vogt]

On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:
>> I don't know how realistic this is but a constraint (HLength x ~
>> HLength y) would ideally have the same result as SameLength x y.
> I'm not sure if I understand that part. HLength is not injective. How would injectivity help here?

I agree it's not injective. But my impression is that injective TFs
pretty much allow ghc to replace a constraint

 TF a b ~ result

with

 (TF_getResult a b ~ result, TF_getB result a ~ b)

Where instances of:

type family TF a b | result a -> b, a b -> result -- or whatever the
notation actually is

define instances of ordinary type families TF_getB and TF_getResult.

So it's a move in the same direction to replace (HLength x ~ HLength
y) with SameLength x y. While I don't know how the code for SameLength
might be derived from the definition of HLength, that substitution
seems safe so long as (HLength x ~ HLength y) is still checked. I can
see that substitution happening in a type checker plugin, but it would
be nice if it was part of the language.

Regards,
Adam