Mark negation injective

{-# Language DataKinds, TypeOperators, TypeFamilyDependencies, UndecidableInstances #-}

import GHC.TypeLits

data N = O | S N

type family
  U (a :: Nat) = (res :: N) | res -> a where
  U 0 = O
  U n = S (U (n-1))

gives

olates injectivity annotation.
      Type variable ‘n’ cannot be inferred from the right-hand side.
      In the type family equation:
        U n = 'S (U (n - 1)) -- Defined at /tmp/a.hs:37:3
    • In the equations for closed type family ‘U’
      In the type family declaration for ‘U’
Failed, modules loaded: none.

I expect this to work, this depends on making (-) injective which depends on "generalized injectivity"?

type family
  (a :: Nat) - (b :: Nat) = (res :: Nat) | a b -> res, res a -> b, res b -> a where
  {- built in -}

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture