Closed jstolarek closed 9 years ago
Suppose I say:
type family F a b (c :: k) = r | r -> a b
type family Fa a b (c :: k) = r | r -> a b c where
Fa a b c = [F a b c]
I get:
Type family equation violates injectivity annotation.
Injective type variable ‘c’ does not appear on injective position.
Injective kind variable ‘k’ is not inferable from the RHS type variables.
In the RHS of type family equation:
forall (k :: BOX) a b (c :: k). Fa a b c = [F a b c]
In the equations for closed type family ‘Fa’
In the type family declaration for ‘Fa’
The quantified type family equation is not indented, unlike equations without forall. Thus I want a third fix:
After converting Fa
to an open type family the equation is printed without forall quantifier - another inconsistency.
After changes in 00680ef86417907960e87f28c58b0024db2ffe10 there is no more inconsistency because makeInjectivityErrors
now works for CoAxBranch
(previously it was polymorphic to work with FamInst
as well). The difference in pretty printing is exactly the difference between pprinting CoAxBranch
and FamInst
.
Currently pretty printing equations of open and closed type family equations is inconsistent:
I want two fixes: