[SOLVED] Are these examples correct or the tutorial has an error?

Are these examples correct or the tutorial has an error?

I am reading this tutorial and I am not sure that I understand correctly the text (or that it is correct at whole). There is an example:

The following predicates are valid because they encode modus ponens: if you know that a implies b and you know that a is true, then it must be the case that b is also true:

{-@ ex6 :: Bool -> Bool -> TRUE @-}
ex6 a b = (a && (a ==> b)) ==> b

{-@ ex7 :: Bool -> Bool -> TRUE @-}
ex7 a b = a ==> (a ==> b) ==> b

and ex6 is fine, but ex7 is not, it fails for a = false and b = false. And LH repot it as:

Error: Liquid Type Mismatch

 88 | ex7 a b = a ==> (a ==> b) ==> b
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Bool | v <=> ((a => (a => b)) => b)}

   not a subtype of Required type
     VV : {VV : GHC.Types.Bool | VV}

   In Context
     a : GHC.Types.Bool

     b : GHC.Types.Bool

Also I don't understand their definition of the implication: "You should read p ==> q as if p is true then q must also be true". It does not sound correctly, because it asserts only one case: T -> T = T. What do I miss here? May be tutorial has error in "ex7"?

Solution

I suspect in the example, they have made (==>) right associative, while in your tests you left it at the default, which is left associative. Compare:

> infixl 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
False
> infixr 9 ==>; False ==> x = True; True ==> x = x
> False ==> (False ==> False) ==> False
True

The Report has further details.