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 |