[GHC] #10082: Church Booleans - xor

[GHC]

#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