Injective type families imply nominal injectivity, but NOT representational injectivity.
ClosedPublic

Authored by ezyang on Feb 26 2017, 11:10 PM.

Details

Summary

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
ezyang created this revision.Feb 26 2017, 11:10 PM

I wonder: is there a test case that would expose this bug?

Representational injectivity on type families says that if T a ~R T b, then a ~N b (N because type families are always nominal, at the moment.) This suggested that the following code might type check:

type family F a = result | result -> a

f :: Coercible (F a) (F b) => a -> b
f x = x

But in fact injective type families are never used for decomposition (i.e., replace this with F a ~ F b, it still won't type check), see https://ghc.haskell.org/trac/ghc/ticket/10833 so this seems to be a moot point.

This revision was automatically updated to reflect the committed changes.