Type family injectivity annotation is rejected with type variable rhs, even on non-endomorphism
In Injective Type Families for Haskell, the following explanation is given for rejecting bare type variables on RHS:
type family W1 a = r | r -> a type instance W1 [a] = a
To a mathematician this function certainly looks injective. But, surprisingly, it does not satisfy Definition 1! Here is a counterexample. Clearly we do have a proof of
(W1 [W1 Int ] ∼ W1 Int)
, simply by instantiating the type instance with[a |-> W1 Int]
. But ifW1
was injective in the sense of Definition 1, we could derive a proof of[W1 Int ] ∼ Int
, and that is plainly false!Similarly:
type family W2 a = r | r -> a type instance W2 [a] = W2 a
Again
W2
looks injective. But we can proveW2 [Int] ∼ W2 Int
, simply by instantiating the type instance; then by Definition 1, we could then conclude[Int] ∼ Int
, which is plainly false. So neitherW1
norW2
are injective, according to our definition. Note that the partiality ofW1
andW2
is critical for the failure case to occur.
In addition to exploiting partiality, the first example also requires W1
to be an endomorphism, and the second one depends on []
being an endomorphism.
So why is the following example still rejected, where the type family is not an endomorphism and not recursive; in fact, even total?
newtype Wrapper = Wrap Type
type family Unwrap (x :: Wrapper) = (r :: Type) | r -> x where
Unwrap (Wrap a) = a