Excessive constraints generated by lemma applications

[rybla]

Consider this schema:

{-@ measure r :: Int -> Bool @-}

{-@ assume lem :: x:{Int | r x} -> {r (x + 1)} @-}
lem :: Int -> ()
lem _ = ()

with :: a -> b -> a
with a _ = a

{-@
test :: x:{Int | r x} -> {r (x + N)}
@-}
test :: Int -> ()
test x = 
  lem x `with`
  lem (x + 1) `with`
  ...
  lem (x + (N - 1))

where N is some constant integer greater than 1.

I noticed that the number of constraints generated by this simple schema seems excessive. Here is some data, where "lemma applications" corresponds to the N above:

Lemma application constraint generation.pdf

Visual summary:

The data covers a few variants:

"with TH" indicates that the imports

import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Language.Haskell.TH.Syntax

were included at the beginning of the file.

"without TH" indicates that those imports were not included at the beginning of the file.

"monomorphic with" indicates that with was retyped to be with :: a -> a -> a.

So, why are so many constraints being generated (20,000+ for just 10 applications of the simple lemma!) and why does it depend on importing the TH modules (which are not used in the code) and whether with is monomorphic or not?

[facundominguez]

I can't reproduce very well with develop. I only get near 700 and 800 constraints at most in all cases. Are you testing with the latest liquidhaskell on hackage maybe?

Also, Proof is not in scope in the example. I replaced it with ().

If I use

with :: () -> () -> ()

then I get only 19 constraints checked.

Polymorphism is known to cause some explosions elsewhere.

[ranjitjhala]

Good point -- Henry, can you let us know what git commit you're using? Thanks!

…

On Sun, Feb 20, 2022 at 2:13 PM Facundo Domínguez ***@***.***> wrote: I can't reproduce very well with develop. I only get near 700 and 800 constraints at most in all cases. Are you testing with the latest liquidhaskell on hackage maybe? Also, Proof is not in scope in the example. I replaced it with (). If I use with :: () -> () -> () then I get only 19 constraints checked. Polymorphism is known to cause some explosions elsewhere <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rE5vpOR0OdQv0iI5U7wZOAgRnpD8RBZf00_2vfxdDiM7bAMoYdxsRjHKqTler7T7&s=YUEQ4MppSCb-XPLIJ3iOjuy_DmEsGFuWIcYRKeeJ9Uo&e=> . — Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1944-23issuecomment-2D1046331894&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rE5vpOR0OdQv0iI5U7wZOAgRnpD8RBZf00_2vfxdDiM7bAMoYdxsRjHKqTler7T7&s=3UG-8-bTCA87q42ba4x5HOtrZ6ql-paydetBpuOcD0k&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OD4ZQ4KMCVJVUPALZDU4FROZANCNFSM5O44JSKA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rE5vpOR0OdQv0iI5U7wZOAgRnpD8RBZf00_2vfxdDiM7bAMoYdxsRjHKqTler7T7&s=cVLv-WVHprwPaH5DJWjYvOtF6IybE3UwY73BhUsrHl4&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=rE5vpOR0OdQv0iI5U7wZOAgRnpD8RBZf00_2vfxdDiM7bAMoYdxsRjHKqTler7T7&s=VMJYPUSrhXexl5yOQn5qLjG9OWFUGDZJjksmnzdEMks&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=rE5vpOR0OdQv0iI5U7wZOAgRnpD8RBZf00_2vfxdDiM7bAMoYdxsRjHKqTler7T7&s=ThHCq6U8XLBHEnwdoiC9oFAcjY8QM0m4GKih5hoyQGI&e=>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[rybla]

Yeah I think its the polymorphism that is responsible for the constraint explosions.

[rybla]

I am using liquidhaskell == 0.8.10.7

[rybla]

Any idea about the TH imports?