#10082: Church Booleans - xor -------------------------------------+------------------------------------- Reporter: honza889 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: Incorrect result | (amd64) at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by honza889: Old description:

When I use following implementation of Church Booleans, all is ok: {{{#!hs lTrue = \x y -> x lFalse = \x y -> y lNot = \t -> t lFalse lTrue lXor = \u v -> u (lNot v) (lNot lNot v) lXor' = \u v -> u (v lFalse lTrue) (v lTrue lFalse) }}}

But this simplified versions of lXor fails, if first parameter is lFalse: {{{#!hs lXor'' = \u v -> u (lNot v) (v) -- not work, bug in ghc? lXor''' = \u v -> u (lNot v) v -- not work, bug in ghc? }}}

{{{#!hs GHCi, version 7.10.0.20150123: http://www.haskell.org/ghc/ :? for help Prelude> :l lambda.hs [1 of 1] Compiling Main ( lambda.hs, interpreted ) Ok, modules loaded: Main. *Main> (lXor'' lFalse lFalse) 1 0

<interactive>:3:1: Non type-variable argument in the constraint: Num (t5 -> t4 -> t5) (Use FlexibleContexts to permit this) When checking that ‘it’ has the inferred type it :: forall t4 t5. Num (t5 -> t4 -> t5) => t5 -> t4 -> t5

<interactive>:3:24: Could not deduce (Num (t20 -> t30 -> t30)) arising from the literal ‘1’ from the context (Num (t5 -> t4 -> t5)) bound by the inferred type of it :: Num (t5 -> t4 -> t5) => t5 -> t4 -> t5 at <interactive>:3:1-26 The type variables ‘t20’, ‘t30’ are ambiguous In the third argument of ‘lXor''’, namely ‘1’ In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for ‘it’: it = (lXor'' lFalse lFalse) 1 0 }}}

Because both lXor implementations in first example works ok, I believe this is bug in ghc. But similar problem occure in older versions of ghc:

{{{#!hs GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude> :l lambda.hs [1 of 1] Compiling Main ( lambda.hs, interpreted ) Ok, modules loaded: Main. *Main> (lXor'' lFalse lFalse) 1 0

<interactive>:3:24: No instance for (Num (t20 -> t30 -> t30)) arising from the literal `1' Possible fix: add an instance declaration for (Num (t20 -> t30 -> t30)) In the third argument of lXor'', namely `1' In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for `it': it = (lXor'' lFalse lFalse) 1 0

<interactive>:3:26: No instance for (Num (t50 -> t40 -> t50)) arising from the literal `0' Possible fix: add an instance declaration for (Num (t50 -> t40 -> t50)) In the fourth argument of lXor'', namely `0' In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for `it': it = (lXor'' lFalse lFalse) 1 0 }}}

New description: When I use following implementation of Church Booleans, all is ok: {{{#!hs lTrue = \x y -> x lFalse = \x y -> y lNot = \t -> t lFalse lTrue lXor = \u v -> u (lNot v) (lNot lNot v) lXor' = \u v -> u (v lFalse lTrue) (v lTrue lFalse) }}} But this simplified versions of lXor fails, if first parameter is lFalse: {{{#!hs lXor'' = \u v -> u (lNot v) (v) -- not work, bug in ghc? lXor''' = \u v -> u (lNot v) v -- not work, bug in ghc? }}} {{{#!hs GHCi, version 7.10.0.20150123: http://www.haskell.org/ghc/ :? for help Prelude> :l lambda.hs [1 of 1] Compiling Main ( lambda.hs, interpreted ) Ok, modules loaded: Main. *Main> (lXor'' lFalse lFalse) 1 0 <interactive>:3:1: Non type-variable argument in the constraint: Num (t5 -> t4 -> t5) (Use FlexibleContexts to permit this) When checking that ‘it’ has the inferred type it :: forall t4 t5. Num (t5 -> t4 -> t5) => t5 -> t4 -> t5 <interactive>:3:24: Could not deduce (Num (t20 -> t30 -> t30)) arising from the literal ‘1’ from the context (Num (t5 -> t4 -> t5)) bound by the inferred type of it :: Num (t5 -> t4 -> t5) => t5 -> t4 -> t5 at <interactive>:3:1-26 The type variables ‘t20’, ‘t30’ are ambiguous In the third argument of ‘lXor''’, namely ‘1’ In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for ‘it’: it = (lXor'' lFalse lFalse) 1 0 }}} Because both lXor implementations in first example works ok and simplified implementation should be equivalent, I believe this is bug in ghc. But similar problem occure also in older versions of ghc: {{{#!hs GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude> :l lambda.hs [1 of 1] Compiling Main ( lambda.hs, interpreted ) Ok, modules loaded: Main. *Main> (lXor'' lFalse lFalse) 1 0 <interactive>:3:24: No instance for (Num (t20 -> t30 -> t30)) arising from the literal `1' Possible fix: add an instance declaration for (Num (t20 -> t30 -> t30)) In the third argument of lXor'', namely `1' In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for `it': it = (lXor'' lFalse lFalse) 1 0 <interactive>:3:26: No instance for (Num (t50 -> t40 -> t50)) arising from the literal `0' Possible fix: add an instance declaration for (Num (t50 -> t40 -> t50)) In the fourth argument of lXor'', namely `0' In the expression: (lXor'' lFalse lFalse) 1 0 In an equation for `it': it = (lXor'' lFalse lFalse) 1 0 }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10082#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler