Build Liquid Haskell with ghc-9.8.1

[facundominguez]

No description provided.

[facundominguez]

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]

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.

[facundominguez]

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]

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…