Min and Max cannot be reflected and cannot be used in measures

[andrewthad]

I read a blog post recently where max is used in a reflected function like this:

{-@ reflect freeVarBound @-}
{-@ freeVarBound :: UExp -> { i:Int | 0 <= i } @-}
freeVarBound :: UExp -> Int
freeVarBound (UVar v) = v + 1
freeVarBound (ULam body) = max 0 (freeVarBound body - 1)
freeVarBound (UApp e1 e2) = max (freeVarBound e1) (freeVarBound e2)

Here is a minimal example where I tried to do something similar:

module Tester
  ( foo                                                                      
  ) where

{-@ reflect foo @-}                                                             
{-@ foo :: { i:Int | 0 <= i } -> { j:Int | 0 <= j } -> { k:Int | 0 <= k } @-}                        
foo :: Int -> Int -> Int                                                                             
foo a b = min a b

This fails with:

src/Tester.hs:5:13: error:
    • Illegal type specification for `Tester.foo`
    Tester.foo :: i:{i : GHC.Types.Int | 0 <= i} -> j:{j : GHC.Types.Int | 0 <= j} -> {k : GHC.Types.Int | k == GHC.Classes.min i j
                                                                                                           && k == Tester.foo i j
                                                                                                           && 0 <= k}
    Sort Error in Refinement: {k : int | k == GHC.Classes.min i j
                                         && k == Tester.foo i j
                                         && 0 <= k}
    Unbound symbol GHC.Classes.min --- perhaps you meant: GHC.Classes.C:IP ?
    Just reflect
    • 
  |
5 | {-@ reflect foo @-}
  |             ^^^^

I'm compiling with GHC 8.10.7, and I have this in my cabal.project file:

packages: .

source-repository-package
    type: git
    location: https://github.com/andrewthad/liquid-base
    tag: ff98e2c14d97684baf5ec05cec7a14685af30687

source-repository-package
    type: git
    location: https://github.com/liquidhaskell/liquid-ghc-prim
    tag: b0d5765f328a527ac1ac41313c8a95e7491695d6

And my dependencies in the cabal file are:

  build-depends:
    , liquid-base ==4.14.3.0
    , liquid-ghc-prim ==0.6.1
    , liquidhaskell >= 0.8.10.7
    , rest-rewrite <0.2

[ranjitjhala]

Hi @andrewthad -- yes this is a bit of an annoyance. The trouble is that min and max are clashing with the names from the Prelude and we cannot retroactively reflect them. This should work if you

import Prelude hiding (min, max)

and then define and reflect them locally so

{-@ reflect min @-}
min x y  = if x <= y then x else y

{-@ reflect max @-}
max x y  = if x >= y then x else y

[andrewthad]

Thanks. That does work, and I've checked and found that stitch-lh actually does this same thing to get a usable version of max. One thing that's still unclear to me everything else in GHC.Classes.spec seems to be reflected just fine. (I've not actually checked on compare, but all the infix relational operators work fine). So, what's really going on? I'm guessing that LH has some of these other ones wired in. If you confirm this, I can PR some comments to GHC.Classes.spec explaining why everything happens as it does.

[ranjitjhala]

Yes, so things like <= and < and == and such are special cases that are handled natively by the SMT solver, but compare for example is not so you wouldn't be able to reflect that.

Does that make sense?

[andrewthad]

Yes, that makes perfect sense. I've PRed some documentation to GHC.Classes explaining the situation and the workarounds.

[ranjitjhala]

Thanks so much!!!

On Thu, Feb 17, 2022 at 6:13 AM Andrew Martin @.***> wrote:

Yes, that makes perfect sense. I've PRed some documentation to GHC.Classes explaining the situation and the workarounds.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1937-23issuecomment-2D1042992096&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=TXqh67Rn12dSeToh7tRnzJmcdz2oqzyKlrbQhst7eIAhbbLBZ6U6A9k1FUbcs82t&s=eoNJ5QHuSFN1XmyWMjlU-VgU1MRQJiTVTfvZ678ycrM&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OGZLDEPNL5OXSNFSMTU3T67LANCNFSM5OMGQQCA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=TXqh67Rn12dSeToh7tRnzJmcdz2oqzyKlrbQhst7eIAhbbLBZ6U6A9k1FUbcs82t&s=Bq4J1ydLU0HVSRyPaiD17qph4xCIAUM-yjHTycJCD-Q&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=TXqh67Rn12dSeToh7tRnzJmcdz2oqzyKlrbQhst7eIAhbbLBZ6U6A9k1FUbcs82t&s=dlenQGI3M9enQZjaaXco42RdtUZzS5f_9WAfzPocgMM&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=TXqh67Rn12dSeToh7tRnzJmcdz2oqzyKlrbQhst7eIAhbbLBZ6U6A9k1FUbcs82t&s=t5CmbHpbtyDPmynhXCCB_8XUucfAPjiLqnaN4Kz2Fho&e=.

You are receiving this because you commented.Message ID: @.***>

[facundominguez]

I would hope this issue has a nice resolution if this is implemented.