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