Class measure example

[vikraman]

Here is a minimal example of a VerifiedEq instance using class measure, which does not work:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1513490381_19482.hs

{-@ LIQUID "--higherorder"                         @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

module VerifiedEq where

import Language.Haskell.Liquid.ProofCombinators

{-@ class measure eq :: forall a. a -> a -> Bool @-}

{-@ class VerifiedEq a where
      eq :: a -> a -> Bool
      refl :: x:a -> {eq x x}
      sym :: x:a -> y:a -> {eq x y ==> eq y x}
      trans :: x:a -> y:a -> z:a -> {eq x y && eq y z ==> eq x z}
@-}

class VerifiedEq a where
  eq :: a -> a -> Bool
  refl :: a -> Proof
  sym :: a -> a -> Proof
  trans :: a -> a -> a -> Proof

{-@ reflect eqInt @-}
eqInt :: Int -> Int -> Bool
eqInt x y = x == y

{-@ eqIntRefl :: x:Int -> {eqInt x x} @-}
eqIntRefl :: Int -> Proof
eqIntRefl _ = ()

{-@ eqIntSym :: x:Int -> y:Int -> {eqInt x y ==> eqInt y x} @-}
eqIntSym :: Int -> Int -> Proof
eqIntSym _ _ = ()

{-@ eqIntTrans :: x:Int -> y:Int -> z:Int -> {eqInt x y && eqInt y z ==> eqInt x z} @-}
eqIntTrans :: Int -> Int -> Int -> Proof
eqIntTrans _ _ _ = ()

instance VerifiedEq Int where
  {-@ instance measure eq :: Int -> Int -> Bool
      eq x y = x == y
  @-}
  eq    = eqInt
  refl  = eqIntRefl
  sym   = eqIntSym
  trans = eqIntTrans

The error is:

LiquidHaskell v0.8.2.0 Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

VerifiedEq.hs:44:10: Error: Cannot parse specification:

 41 |       eq x y = x == y
               ^

     unexpected "x"
     expecting measurePatP

Here is the full example, with a product instance that also fails to parse:

https://github.com/iu-parfunc/verified-instances/blob/0be45fc26d84fe294506e9553048a1413dae0962/src/GHC/Classes/VerifiedEq.hs

/cc @RyanGlScott

[vikraman]

I realized that you're already investigating this, so #1194, #1195, #1196 are related.

[kosmikus]

I don't see the direct relationship to the other issues mentioned. It seems that the primary parsing problem in this issue is that a pattern in a measure (measurePatP) is not allowed to be a plain variable, but must essentially be a constructor application. I am not sure whether this restriction is fully justified.