Marking Pred(S n) = n as injective
Should Pred
be injective? Please close the ticket if this is a known limitation
{-# Language DataKinds, TypeFamilyDependencies #-}
data N = O | S N
type family
Pred n = res | res -> n where
Pred(S n) = n
fails with
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n -- Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’
|
7 | Pred(S n) = n
| ^^^^^^^^^^^^^
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |