#13797: Mark negation injective -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple InjectiveFamilies | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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 [https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies#Futureplansandid... "generalized injectivity"]? {{{#!hs type family (a :: Nat) - (b :: Nat) = (res :: Nat) | a b -> res, res a -> b, res b -> a where {- built in -} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13797 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler