Build Liquid Haskell with ghc-9.8.1 by facundominguez · Pull Request #2248 · ucsd-progsys/liquidhaskell

facundominguez · 2023-12-11T22:20:28Z

No description provided.

facundominguez · 2023-12-11T22:44:50Z

At the moment Liquid Haskell builds, but tests are failing still. I've found differences in desugaring that affect the tests. One of them was the desugaring of ($), which I fixed in 951c19d. The last failure I found is in tests/pos/Map0.hs.

This test has a functions like

deleteFindMax t
  = case t of
      Bin _ k x l Tip -> (k, x, l)
      Bin _ k x l r -> let (km3, vm, rm) = deleteFindMax r in (km3, vm, (balance k x l rm))
      Tip           -> (error ms, error ms, Tip)
  where ms = "Map.deleteFindMax : can not return the maximal element of an empty Map"

which in ghc-9.6 used to be desugared to

deleteFindMax
  = \ @a_a1aW @b_a1aX ->
      letrec {
        deleteFindMax_a1aC
          = \ t_a14r ->
              let {
                ms_a14s
                  = break<17>()
                    unpackCString#
                      "Map.deleteFindMax : can not return the maximal element of an empty Map"# } in
              break<24>(t_a14r,ms_a14s)
              case t_a14r of {
                Tip -> break<23>(ms_a14s) (error ms_a14s, error ms_a14s, Tip);
                Bin _ k_a14t x_a14u l_a14v ds_d2ih ->
                  case ds_d2ih of {
                    __DEFAULT ->
                      break<22>(x_a14u,k_a14t,l_a14v,ds_d2ih)
                      let { ds_d2if = break<19>(ds_d2ih) deleteFindMax_a1aC ds_d2ih } in
                      let {
                        km3_a14A = case ds_d2if of { (km3_a1bc, _, _) -> km3_a1bc } } in
                      let { vm_a14B = case ds_d2if of { (_, vm_a1bd, _) -> vm_a1bd } } in
                      let { rm_a14C = case ds_d2if of { (_, _, rm_a1be) -> rm_a1be } } in
                      break<21>(x_a14u,k_a14t,l_a14v,vm_a14B,rm_a14C,km3_a14A)
                      (km3_a14A, vm_a14B,
                       break<20>(x_a14u,k_a14t,l_a14v,rm_a14C)
                       balance k_a14t x_a14u l_a14v rm_a14C);
                    Tip -> break<18>(x_a14u,k_a14t,l_a14v) (k_a14t, x_a14u, l_a14v)
                  }
              }; } in
      deleteFindMax_a1aC

With ghc-9.8.1 it is desugared to

deleteFindMax
  = \ @a_a1cJ @b_a1cK ->
      letrec {
        deleteFindMax_a1co
          = \ t_a15w ->
              let {
                ms_a15x
                  = unpackCString#
                      "Map.deleteFindMax : can not return the maximal element of an empty Map"# } in
              case t_a15w of {
                Tip -> (error ms_a15x, error ms_a15x, Tip);
                Bin _ k_a15y x_a15z l_a15A ds_d2kE ->
                  case ds_d2kE of {
                    __DEFAULT ->
                      let { ds_d2kC = deleteFindMax_a1co ds_d2kE } in
                      (case ds_d2kC of { (km3_a15F, _, _) -> km3_a15F },
                       case ds_d2kC of { (_, vm_a15G, _) -> vm_a15G },
                       balance
                         k_a15y
                         x_a15z
                         l_a15A
                         (case ds_d2kC of { (_, _, rm_a15H) -> rm_a15H }));
                    Tip -> (k_a15y, x_a15z, l_a15A)
                  }
              }; } in
      deleteFindMax_a1co

and Liquid Haskell produces errors like,

**** LIQUID: UNSAFE ************************************************************

tests/pos/Map0.hs:53:22: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV < ?a}
    .
    in the context
      ?a : a
    Constraint id 63
   |
53 |                LT -> balance kx x (delete k l) r
   |                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

tests/pos/Map0.hs:54:22: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV > ?a}
    .
    in the context
      ?a : a
    Constraint id 19
   |
54 |                GT -> balance kx x l (delete k r)
   |                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

tests/pos/Map0.hs:55:22: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV > ?a}
    .
    in the context
      ?a : a
    Constraint id 45
   |
55 |                EQ -> glue kx l r
   |                      ^^^^^^^^^^^

The following rewriting of deleteFindMax causes Liquid Haskell to fail with ghc-9.6 as well:

deleteFindMax t
  = case t of
      Bin _ k x l Tip -> (k, x, l)
      Bin _ k x l r -> let ds = deleteFindMax r in
        (case ds of { (km3, vm, rm) -> km3 }
        , case ds of { (km3, vm, rm) -> vm }
        , balance k x l (case ds of { (km3, vm, rm) -> rm })
        )

      Tip           -> (error ms, error ms, Tip)
  where ms = "Map.deleteFindMax : can not return the maximal element of an empty Map"

Any insights welcome. Otherwise, it seems I'm headed for a good debugging session.

facundominguez · 2023-12-11T23:56:30Z

First stop, check that the output of A normalization is the same before and after the source edit. I think both desugarings should lead to very similar results there.

This workarounds haskell/cabal#9375

facundominguez · 2024-01-29T18:08:00Z

The last failure I found is in tests/pos/Map0.hs.

I created #2257 to follow up this. I found a way to recover the old behavior of the desugarer, but it would still be desirable to fix the bug to survive potential changes in the future.

I provided more details on the control of desugaring here.

ranjitjhala · 2024-01-29T18:17:40Z

This is fantastic — thanks a bunch @facundominguez — and my apologies for missing the question in this PR itself; I could have saved you a lot of time with the rewriting-to-case!

i think I have recalled the issue with the GHC desugaring - I’ll post that in the other issue…

facundominguez force-pushed the fd/ghc-9.8.1 branch 7 times, most recently from 3035758 to 29761a4 Compare January 29, 2024 16:03

facundominguez added 16 commits January 29, 2024 14:53

Fix build errors when building with ghc-9.8.1

125a6df

Fix location of readInteger and readInt in bytestring specs

c622e77

Update liquid-fixpoint

c5df8a5

Fix desugaring of ($)

b65d849

Avoid PartialTypeSignatures in tests/pos/GhcSort1.hs

d2d52dd

Insert breakpoints when desugaring to prevent too much inlining

1576dc7

Fix compilation of the vector-algorithms benchmark

f3f2ad5

Update build configuration to use ghc-9.8.1

abc4e18

Use ghc 9.8.1 in CI

277a224

Please hlint

6e9a7de

Factor out splitDollarApp for testing

3f80219

Test desugaring of dollar sign

a3fd16e

Add pointer to discussion of problems with numeric literals

389ad97

Enable breakpoints in GHC API tests, same as in LH desugaring

87c0410

Test that local bindings are not inlined during desugaring

0b489ac

Don't set -fplugin in ghc-options

5fbff05

This workarounds haskell/cabal#9375

facundominguez force-pushed the fd/ghc-9.8.1 branch from 29761a4 to 5fbff05 Compare January 29, 2024 17:56

facundominguez merged commit 77895fa into develop Jan 29, 2024

facundominguez deleted the fd/ghc-9.8.1 branch January 29, 2024 18:40

facundominguez added the Major GHC upgrade label May 16, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Build Liquid Haskell with ghc-9.8.1#2248

Build Liquid Haskell with ghc-9.8.1#2248
facundominguez merged 16 commits into
developfrom
fd/ghc-9.8.1

facundominguez commented Dec 11, 2023

Uh oh!

facundominguez commented Dec 11, 2023 •

edited

Loading

Uh oh!

facundominguez commented Dec 11, 2023 •

edited

Loading

Uh oh!

facundominguez commented Jan 29, 2024 •

edited

Loading

Uh oh!

ranjitjhala commented Jan 29, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

facundominguez commented Dec 11, 2023

Uh oh!

facundominguez commented Dec 11, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

facundominguez commented Dec 11, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

facundominguez commented Jan 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ranjitjhala commented Jan 29, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

facundominguez commented Dec 11, 2023 •

edited

Loading

facundominguez commented Dec 11, 2023 •

edited

Loading

facundominguez commented Jan 29, 2024 •

edited

Loading