When importing ProofCombinators for inductive propositions, using v as a binder in refinements causes error

[michaelborkowski]

When we're using the inductive proposition helpers from ProofCombinators.hs:

-------------------------------------------------------------------------------
-- | Convenient Syntax for Inductive Propositions 
-------------------------------------------------------------------------------

{-@ measure prop :: a -> b           @-}
{-@ type Prop E = {v:_ | prop v = E} @-}

that variable v in the refinement of Prop E above will conflict with with any binder v used in dependent refinements that mention Prop. Here's an example:

{-# LANGUAGE GADTs #-}

module STLC where

import Language.Haskell.Liquid.ProofCombinators

data Expr = N Int                -- 0, 1, 2, ...
          | Add Expr Expr        -- e1 + e2
  deriving (Eq, Show)

data Value = VNum Int            --
  deriving (Eq, Show)

data BStepP where
    BStep :: Expr -> Value -> BStepP

data BStep where
    ENum :: Int -> BStep
    EAdd :: Expr -> Int -> BStep -> Expr -> Int -> BStep -> Int -> BStep

{-@ data BStep where
    ENum :: v:Int -> Prop(BStep (N v) (VNum v))
 |  EAdd :: e1:Expr -> v1:Int -> Prop(BStep e1 (VNum v1))
              -> e2:Expr -> v2:Int -> Prop(BStep e2 (VNum v2))
              -> { v:Int | v == v1 + v2 } -> Prop(BStep (Add e1 e2) (VNum v)) @-}

This fails with an error on ENum and an error on EAdd. For instance, here v is both of type STLC.BStep and being bound to Int:

 /home/michael/liquidmeta/PropTest.hs:18:5-24: Error: Illegal type specification for `STLC.ENum`

 18 |     ENum :: Int -> BStep
          ^^^^^^^^^^^^^^^^^^^^

     STLC.ENum :: GHC.Types.Int -> {v : STLC.BStep | prop v == BStep (N v) (VNum v)}
     Sort Error in Refinement: {v : STLC.BStep | prop v == STLC.BStep (STLC.N v) (STLC.VNum v)}
     The sort STLC.BStep is not numeric
  because
Cannot unify int with STLC.BStep in expression: STLC.N v

The code passes as safe when all uses of v are changed to n or something.

[ranjitjhala]

This is the thing we talked about last week, right?

On Fri, Jan 24, 2020 at 12:23 PM Michael Borkowski notifications@github.com wrote:

When we're using the inductive proposition helpers from ProofCombinators.hs:

---

-- | Convenient Syntax for Inductive Propositions

{-@ measure prop :: a -> b @-} {-@ type Prop E = {v:_ | prop v = E} @-}

that variable v in the refinement of Prop E above will conflict with with any binder v used in dependent refinements that mention Prop. Here's an example:

{-# LANGUAGE GADTs #-}

module STLC where

import Language.Haskell.Liquid.ProofCombinators

data Expr = N Int -- 0, 1, 2, ... | Add Expr Expr -- e1 + e2 deriving (Eq, Show)

data Value = VNum Int -- deriving (Eq, Show)

data BStepP where BStep :: Expr -> Value -> BStepP

data BStep where ENum :: Int -> BStep EAdd :: Expr -> Int -> BStep -> Expr -> Int -> BStep -> Int -> BStep

{-@ data BStep where ENum :: v:Int -> Prop(BStep (N v) (VNum v)) | EAdd :: e1:Expr -> v1:Int -> Prop(BStep e1 (VNum v1)) -> e2:Expr -> v2:Int -> Prop(BStep e2 (VNum v2)) -> { v:Int | v == v1 + v2 } -> Prop(BStep (Add e1 e2) (VNum v)) @-}

This fails with an error on ENum and an error on EAdd. For instance, here v is both of type STLC.BStep and being bound to Int:

/home/michael/liquidmeta/PropTest.hs:18:5-24: Error: Illegal type specification for STLC.ENum

18 | ENum :: Int -> BStep ^^^^^^^^^^^^^^^^^^^^

 STLC.ENum :: GHC.Types.Int -> {v : STLC.BStep | prop v == BStep (N v) (VNum v)}
 Sort Error in Refinement: {v : STLC.BStep | prop v == STLC.BStep (STLC.N v) (STLC.VNum v)}
 The sort STLC.BStep is not numeric

because Cannot unify int with STLC.BStep in expression: STLC.N v

The code passes as safe when all uses of v are changed to n or something.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1592?email_source=notifications&email_token=AAMS4OEUJHPLOUNMHQBFSODQ7NEZ3A5CNFSM4KLLTPOKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IITU54Q, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OCN2FRZC5VZDJ2WOBTQ7NEZ3ANCNFSM4KLLTPOA .

[michaelborkowski]

Yes, that's the one.

The workaround for now is to define our own Prop and prop and use a variable in place of v that is unlikely to be repeated. However a different name needs to be chosen for our prop because we can't hide prop when importing ProofCombinators (because prop is only defined in an annotation).