Opened 2 years ago

#13797 new bug

Mark negation injective

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: InjectiveFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# 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 -}

Change History (0)

Note: See TracTickets for help on using tickets.