type family Gc (a :: k) (b :: k) = r | r -> k where
Gc a b = Int
It should be rejected with an error message:
T6018failclosed12.hs:7:5:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferable from the RHS type variables.
In the RHS of type family equation:
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
In the equations for closed type family ‘Gc’
In the type family declaration for ‘Gc’
But it gets accepted. Even more surprisingly open type family variant is rejected:
type family Gc (a :: k) (b :: k) = r | r -> k
type instance Gc a b = Int
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferable from the RHS type variables.
In the RHS of type family equation:
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
@simonpj this happened after your refactoring. I'm looking into this at the moment but please tell if you have any ideas what might have changed here.
Consider this definition:
It should be rejected with an error message:
But it gets accepted. Even more surprisingly open type family variant is rejected:
@simonpj this happened after your refactoring. I'm looking into this at the moment but please tell if you have any ideas what might have changed here.