Type family injectivity violation despite different kinds

181 views Asked by At

In the following example:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE PolyKinds #-}
newtype A a b = A (a, b)
type family F (x :: k) = (r :: k) | r -> x
type instance F (A a) = A a
type instance F (A a b) = A a b

In my current understanding, the first type instance deals with *->* kind, while the second instance deals with *.

So even if I'm using the same newtype A, I don't see any injectivity violation risk, as absolutely no A a ever matches a A a b since they don't even have the same kind.

However GHC 8.6.5 complains that the two type instances violate injectivity but why is that? Is there a workaround?

0

There are 0 answers