drop autosize (was: autosize causes LH to forget field refinements)

[andrewthad]

Liquid Haskell accepts this program:

{-@
data Term
  = Var ({ i:Int | 0 <= i })
  | Let Term Term
  | Lit Int
@-}
data Term
  = Var Int -- de bruijn index
  | Let Term Term
  | Lit Int

{-@ freeVarBound :: Term -> { i:Int | 0 <= i } @-}
freeVarBound :: Term -> Int
freeVarBound t = case t of
  Var v -> v + 1
  Lit _ -> 0
  Let a b ->
    let a' = freeVarBound a
        b' = freeVarBound b - 1
     in if a' > b' then a' else b'

However, if I add

{-@ autosize Term @-}

Then, Liquid Haskell rejects the program with:

src/Tester.hs:25:12: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v' : GHC.Types.Int | v' == v + (1 : int)}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | 0 <= VV}
    .
    in the context
      v : GHC.Types.Int
    Constraint id 6
   |
25 |   Var v -> v + 1
   |            ^^^^^

It seems like the refinement of the field inside of Var is discarded by LH when the autosize is used.

[ranjitjhala]

Aha - I’ve seen this too, @nikivazou any idea? Personally I think we should drop auto size as we have the structural checker…

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

Liquid Haskell accepts this program:

{-@ data Term = Var ({ i:Int | 0 <= i }) | Let Term Term | Lit Int @-} data Term = Var Int -- de bruijn index | Let Term Term | Lit Int

{-@ freeVarBound :: Term -> { i:Int | 0 <= i } @-} freeVarBound :: Term -> Int freeVarBound t = case t of Var v -> v + 1 Lit _ -> 0 Let a b -> let a' = freeVarBound a b' = freeVarBound b - 1 in if a' > b' then a' else b'

However, if I add

{-@ autosize Term @-}

Then, Liquid Haskell rejects the program with:

src/Tester.hs:25:12: error: Liquid Type Mismatch . The inferred type VV : {v' : GHC.Types.Int	v' == v + (1 : int)} . is not a subtype of the required type VV : {VV : GHC.Types.Int	0 <= VV} . in the context v : GHC.Types.Int Constraint id 6
25	Var v -> v + 1
^^^^^

It seems like the refinement of the field inside of Var is discarded by LH when the autosize is used.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1942&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6IU82JVISfKw0_9MqcNOU6og5xYEtVRfOo1oPg1hT72MGHMHKrCbrr06CBYGY0sH&s=BoxLIKAwsGJnTPTLxqx7S8VCr2cYZxENYu7vVcrVPps&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OC5U3ZXFJILKAOLJOTU3TZE3ANCNFSM5OUVO3AA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6IU82JVISfKw0_9MqcNOU6og5xYEtVRfOo1oPg1hT72MGHMHKrCbrr06CBYGY0sH&s=n1Uu1rl7rGlQm6YXg7u46aOjkEBUmxnew7Y3GpgivUk&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=6IU82JVISfKw0_9MqcNOU6og5xYEtVRfOo1oPg1hT72MGHMHKrCbrr06CBYGY0sH&s=Eqs9QABge7UeRmvsNhFLNSWyXZZAlIslWWRcj5qyV5A&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=6IU82JVISfKw0_9MqcNOU6og5xYEtVRfOo1oPg1hT72MGHMHKrCbrr06CBYGY0sH&s=V4OqSJYDNr-DhfO88Rzm1Tq9ZMTD4DTKBQp3A4gthTE&e=.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

[nikivazou]

Yeah, I agree!

The autosize was developed before the structural checker. Now most functions just pass the termination checker and for the rest the user has to manually define the (no-auto)size

[andrewthad]

Ah, that makes sense. Yeah, it seems like it would be good to just get rid of autosize. I didn't even realize that the structural checker existed. Perhaps, if you get rid of autosize, leave a mention of it in the Spec Reference document, explaining it has been removed and that the structural checker does something similar but is better. Speaking of which, the structural checker is not currently described by the Spec Reference document.

[nikivazou]

Correct, we should add it in the documentation... But, the structural is the default! The "semantic" will only be used if you explicitly give / [...] annotations.