Reflection doesn't behave as measures

[pacastega]

The function inferType below can be declared as a measure, which makes both foo and bar pass. When declaring it as reflect only foo passes. Enabling --ple-with-undecided-guards makes both pass again.

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
-- {-@ LIQUID "--ple-with-undecided-guards" @-}
module Test where

data Ty = TInt | TBool
data Expr = CONST Int | TRUE | FALSE

{-@ reflect inferType @-}
-- {-@ measure inferType @-}

inferType :: Expr -> Ty
inferType (CONST _) = TInt
inferType TRUE = TBool
inferType FALSE = TBool

{-@ type IntExpr = {e:Expr | inferType e = TInt} @-}

-- passes
{-@ foo :: IntExpr @-}
foo :: Expr
foo = CONST 42

-- fails
{-@ bar :: [IntExpr] @-}
bar :: [Expr]
bar = [CONST 42]

[ranjitjhala]

Ah @facundominguez this is the example of plugging in KVar solutions before PLE that you were alluding to?

[facundominguez]

From the prettified output, this is the failing constraint:

constraint:
  lhs {VV : Test.Expr | [$k_##728[VV##1348:=VV][VV##727:=VV][VV##F:=VV][lq_tmp$x##1349:=VV][lq_tmp$x##719:=VV##1343][lq_tmp$x##723:=lq_anf$##dFK][lq_tmp$x##724:=lq_anf$##dFL][lq_tmp$x##729:=VV]]}
  rhs {VV : Test.Expr | [((Test.inferType VV) = Test.TInt)]}
  id 12 tag [1]
  // META constraint id 12 : Test.hs:28:1-16
  environment:
    // elided some likely irrelevant bindings
    
    lq_anf$##dFK :
      {lq_tmp$x : Test.Expr |
         [(is$Test.CONST lq_tmp$x);
          (~ ((is$Test.FALSE lq_tmp$x)));
          (~ ((is$Test.TRUE lq_tmp$x)));
          (lq_tmp$x = (Test.CONST (GHC.Types.I# 42)));
          ((Test.CONST##lqdc##$select##Test.CONST##1 lq_tmp$x) =
             (GHC.Types.I# 42))]}
    
    lq_anf$##dFL :
      {lq_tmp$x : [Test.Expr] |
         [(is$36$GHC.Types.$91$$93$ lq_tmp$x);
          (~ ((is$36$GHC.Types.$58$ lq_tmp$x)));
          (lq_tmp$x = GHC.Types.$91$$93$);
          ((GHC.Types_LHAssumptions.len lq_tmp$x) = 0);
          ((GHC.Types_LHAssumptions.len lq_tmp$x) >= 0)]}
    
    _lq_anf$##dFJ :
      {lq_tmp$x : int |
         [(lq_tmp$x = (GHC.Types.I# 42)); (lq_tmp$x = (42  :  int))]}

It looks like an instance of ucsd-progsys/liquid-fixpoint#780 in that the solution to the kvar does hide information that PLE could use to unfold inferType in the RHS.

I think the fact that it passes with --ple-with-undecided-guards is accidental. With measures, PLE is superfluous in this example.

[nikivazou]

I think we should just treat reflected functions as measures when possible (i.e., when we reflect functions on one ADT argument to refine the data constructors).

(Also, I am not entirely sure what --ple-with-undecided-guards is doing)

[facundominguez]

--ple-with-undecided-guards is explained in the flag reference [link], but let me know if it is insufficient.

In this case, the flag causes more unfoldings to be inserted in bindings, and this might strengthen the hypotheses of any constraints that have the bindings, even those having kvars in the LHS.

[ranjitjhala]

I agree with the problem. Ultimately all three are the same to the user BUT are treated differently inside LH which is a real wart. 1. Can’t inline be already just replaced with reflect? 2. Measure -> reflect seems trickier, but I wonder if it’s possible by just strengthening the data constructor with its logical adt version? So Cons :: x:a -> xs:_ -> {v: _ | v = Cons x xs } After which PLE should work to recover the semantics of measures like Len etc? - Ranjit.

…

On Fri, Oct 31, 2025 at 4:21 AM Facundo Domínguez ***@***.***> wrote: *facundominguez* left a comment (ucsd-progsys/liquidhaskell#2582) <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3472601174__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eoGqTFP$> --ple-with-undecided-guards is explained in the flag reference [link] <https://urldefense.com/v3/__https://ucsd-progsys.github.io/liquidhaskell/options/*theorem-proving__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62VURH7_1$>, but let me know if it is insufficient. In this case, the flag causes more unfoldings to be inserted in bindings, and this might strengthen the hypotheses of any constraints that have the bindings, even those having kvars in the LHS. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3472601174__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eoGqTFP$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAPHRXFTQAYE6HMTML32NA23AVCNFSM6AAAAACKVNM2Y6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTINZSGYYDCMJXGQ__;!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eUzn6Yg$> . You are receiving this because you commented.Message ID: ***@***.***>

[ranjitjhala]

Or even Niki’s suggestion of “detecting” when something is a measure. One concern is that if ultimately there is a major conceptual difference in how the two are handled internally then “hiding” that difference at the syntax / surface level may be counterproductive… hence it may be good to really get to the bottom of WHY we have these two mechanisms and if reflect+PLE doesn’t subsume “measure”. One issue is the measures give “invariant” like Len >= 0 of which there is no equivalent as such in reflection ? - Ranjit.

…

On Fri, Oct 31, 2025 at 7:09 AM Ranjit Jhala ***@***.***> wrote: I agree with the problem. Ultimately all three are the same to the user BUT are treated differently inside LH which is a real wart. 1. Can’t inline be already just replaced with reflect? 2. Measure -> reflect seems trickier, but I wonder if it’s possible by just strengthening the data constructor with its logical adt version? So Cons :: x:a -> xs:_ -> {v: _ | v = Cons x xs } After which PLE should work to recover the semantics of measures like Len etc? - Ranjit. On Fri, Oct 31, 2025 at 4:21 AM Facundo Domínguez < ***@***.***> wrote: > *facundominguez* left a comment (ucsd-progsys/liquidhaskell#2582) > <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3472601174__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eoGqTFP$> > > --ple-with-undecided-guards is explained in the flag reference [link] > <https://urldefense.com/v3/__https://ucsd-progsys.github.io/liquidhaskell/options/*theorem-proving__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62VURH7_1$>, > but let me know if it is insufficient. > > In this case, the flag causes more unfoldings to be inserted in bindings, > and this might strengthen the hypotheses of any constraints that have the > bindings, even those having kvars in the LHS. > > — > Reply to this email directly, view it on GitHub > <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3472601174__;Iw!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eoGqTFP$>, > or unsubscribe > <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAPHRXFTQAYE6HMTML32NA23AVCNFSM6AAAAACKVNM2Y6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTINZSGYYDCMJXGQ__;!!Mih3wA!FWoZWMeNbHPUmttm5FyThONcZ8gpFpFuzu_gdGV5oT8lo05_gWvratdJif82XOmkyo9ptOmWJvEqhHr62eUzn6Yg$> > . > You are receiving this because you commented.Message ID: > ***@***.***> >

[nikivazou]

2. Measure -> reflect seems trickier, but I wonder if it’s possible by just
   strengthening the data constructor with its logical adt version? So

Cons :: x:a -> xs:_ -> {v: _ | v = Cons x xs }

After which PLE should work to recover the semantics of measures like Len
etc?

That will not always work. Say that foo is a measure on the data type List.
Then, PLE can recover the definition of foo only when a call to foo appears in the verification condition.
But, the current measure implementation will "unfold" foo's definition whenever the List's constructors appear.

So, I believe we need to keep both functionalities, just we do not have to expose them to the user.

• Ranjit.
  …

[ranjitjhala]

Good point: PLE is only “triggered” if foo appears but presumably there is a foo in the VC somewhere anyways otherwise what is the measure even doing? Can you construct an example where you want the measure style “automatic” instantiation but where foo is NOT in the VC and so will not be PLE-ed? - Ranjit.

…

On Fri, Oct 31, 2025 at 7:55 AM Niki Vazou ***@***.***> wrote: *nikivazou* left a comment (ucsd-progsys/liquidhaskell#2582) <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3473450156__;Iw!!Mih3wA!GRwiifB-eEkoJKOgXRkY__QMGNpFEPs-GfDLqXvq1rJbSJpA5PaQ-hhjszSpj8eGCdZTy7CK8e5mUFdxUbLSXcJb$> 2. Measure -> reflect seems trickier, but I wonder if it’s possible by just strengthening the data constructor with its logical adt version? So Cons :: x:a -> xs:_ -> {v: _ | v = Cons x xs } After which PLE should work to recover the semantics of measures like Len etc? That will not always work. Say that foo is a measure on the data type List . Then, PLE can recover the definition of foo only when a call to foo appears in the verification condition. But, the current measure implementation will "unfold" foo's definition whenever the List's constructors appear. So, I believe we need to keep both functionalities, just we do not have to expose them to the user. - Ranjit. … <#m_5772932007107744057_> — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2582*issuecomment-3473450156__;Iw!!Mih3wA!GRwiifB-eEkoJKOgXRkY__QMGNpFEPs-GfDLqXvq1rJbSJpA5PaQ-hhjszSpj8eGCdZTy7CK8e5mUFdxUbLSXcJb$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4ODC5BK2QTZGOZZ4MTL32NZ5BAVCNFSM6AAAAACKVNM2Y6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTINZTGQ2TAMJVGY__;!!Mih3wA!GRwiifB-eEkoJKOgXRkY__QMGNpFEPs-GfDLqXvq1rJbSJpA5PaQ-hhjszSpj8eGCdZTy7CK8e5mUFdxUabz7P7N$> . You are receiving this because you commented.Message ID: ***@***.***>

[facundominguez]

Absent an example of measure that cannot be treated with reflect, we could experiment changing the parser to treat {-@ measure f @-} as {-@ reflect f @-}, enable PLE by default and see how the tests fail.