On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek <jan.stola...@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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
