Innocent edit causes tests/pos/Map0.hs to fail

[facundominguez]

tests/pos/Map0.hs has a function

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"

If we rewrite this function to

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"

then 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
   |                      ^^^^^^^^^^^

This bug is relevant because it happens when attempting to upgrade to GHC 9.8.1, where
the desugaring of the original deleteFindMax changes to the failing version.

I haven't been able to find a smaller example, and I don't know yet how to locate the flawed code quickly.

[ranjitjhala]

I'll have to page this back in: it has to do with some strange interaction with

• tuples,
• abstract refinements,
• inference/fusion.

Does it work if you rewrite the line as:

Bin _ k x l r -> 
  case deleteFindMax r of 
    (km3, vm, rm) -> (km3, vm, (balance k x l rm))                              

[As an aside to @nikivazou] The thing that really bugs me about this example is that it relies completely on inference: I believe there is no way to even write down the "correct" type for deleteFindMax that LH will parse. This is bad because, you should always be able to explicitly specify the correct type...

[facundominguez]

Does it work if you rewrite the line as:

Yes, it does still pass verification if the let is rewritten with a single case.

[facundominguez]

tests/pos/DepTriples.hs is a much smaller example and it fails in the same way. Here's the original:

module DepTriples where

{-@ type INCR3 = (Int, Int, Int)<{\a b -> a < b}, {\b a c -> b < c }>@-}

{-@ assume incr3 :: INCR3 @-}
incr3 :: (Int, Int, Int)
incr3 = undefined

{-@ uincr3 :: INCR3 @-}
uincr3 :: (Int, Int, Int)
uincr3 = let (x, y, z) = incr3
          in (x + 1, y + 1, z +1 )

Now rewrite uincr3 to see LH fail:

uincr3 = let (x, y, z) = incr3 in
          in (case incr3 of (x1, _, _) -> x1 + 1, y + 1, z +1 )

[ranjitjhala]

@facundominguez -- here's what I believe is going on. Consider an even smaller example:

{-@ type INCR2 = (Int, Int)<{\a b -> a < b}>@-}

{-@ foo :: Int -> INCR2 @-}
incr2 :: Int -> (Int, Int)
incr2 x = (x, x + 1)

{-@ type TRUE = {b: Bool | b} @-} 

{-@ test_fails :: Int -> TRUE @-}
test_fails :: Int -> Bool
test_fails a = 
  let p = incr2 a 
       x = case p of 
                (v1,_) -> v1     -- x gets the type x: Int 
       y = case p of 
                (_, v2) -> v2   -- y gets type of `v2`, i.e. 
                                        -- exists `v1:Int. {v:Int | v1 < v}` 
                                        -- but **don't know** that `x` is `v1`!
  in
     x < y       -- LH doesn't know that `x` is less than `y` !
     
{-@ test_ok :: Int -> TRUE @-}
test_ok :: Int -> Bool
test_ok a = 
  let p = incr2 a 
  case p of 
      (x, y) -> x < y   -- `x` gets type `x:Int` and `y` gets type `{v:Int | x < v}`

In brief, when you have "dependent tuples", you need to "unpack" the tuples at one place to recover the relationships between fields. Otherwise, if you "unpack" the components separately, you lose the connection. I expect this is probably a well known (?) phenomenon with "dependent pattern matching" but I'm not familiar enough with the literature to know what to cite/point at! @nikivazou do you know? This is the kind of thing Michael Greenberg would know...

[facundominguez]

That is an interesting clue, but I have to say that verification passes for test_fails and test_ok both with ghc-9.8.1 and ghc-9.6.3.

Also, the desugaring of the original test/pos/DepTriple.hs unpacks each field individually, and LH is happy with that:

uincr3
  = break<3>()
    let { ds_d21N = break<1>() incr3 } in
    let { x_a111 = case ds_d21N of { (x_a11r, _, _) -> x_a11r } } in
    let { y_a112 = case ds_d21N of { (_, y_a11s, _) -> y_a11s } } in
    let { z_a113 = case ds_d21N of { (_, _, z_a11t) -> z_a11t } } in
    break<2>(z_a113,y_a112,x_a111)
    (+ $fNumInt x_a111 (I# 1#), + $fNumInt y_a112 (I# 1#),
     + $fNumInt z_a113 (I# 1#))

It only fails when one of the fields is inlined (e.g. x_a111) as in the example I provided.

[facundominguez]

In any case, thanks a lot for looking at this.

[ranjitjhala]

Aha, I found something... See this:

liquidhaskell/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs

Lines 199 to 259 in 77895fa

	--------------------------------------------------------------------------------
	-- | Rewriting Pattern-Match-Tuples --------------------------------------------
	--------------------------------------------------------------------------------
	{-
	let CrazyPat x1 ... xn = e in e'
	let t : (t1,...,tn) = "CrazyPat e ... (y1, ..., yn)"
	xn = Proj t n
	...
	x1 = Proj t 1
	in
	e'
	"crazy-pat"
	-}
	{- [NOTE] The following is the structure of a @PatMatchTup@
	let x :: (t1,...,tn) = E[(x1,...,xn)]
	yn = case x of (..., yn) -> yn
	…
	y1 = case x of (y1, ...) -> y1
	in
	E'
	GOAL: simplify the above to:
	E [ (x1,...,xn) := E' [y1 := x1,...,yn := xn] ]
	TODO: several tests (e.g. tests/pos/zipper000.hs) fail because
	the above changes the "type" the expression `E` and in "other branches"
	the new type may be different than the old, e.g.
	let (x::y::_) = e in
	x + y
	let t = case e of
	h1::t1 -> case t1 of
	(h2::t2) -> (h1, h2)
	DEFAULT -> error @ (Int, Int)
	DEFAULT -> error @ (Int, Int)
	x = case t of (h1, _) -> h1
	y = case t of (_, h2) -> h2
	in
	x + y
	is rewritten to:
	h1::t1 -> case t1 of
	(h2::t2) -> h1 + h2
	DEFAULT -> error @ (Int, Int)
	DEFAULT -> error @ (Int, Int)
	case e of
	h1 :: h2 :: _ -> h1 + h2
	DEFAULT -> error @ (Int, Int)
	which, alas, is ill formed.
	-}

I need to page the code in Rewrite back in -- but IIRC, this was a recurrent pattern so I added a core-to-core rewrite to undo the effects, perhaps that rewriting fails to get triggered in the situations you're seeing with the GHC update?

[ranjitjhala]

I confess the docs in that module could be significantly improved, sorry! :-(

However, looking at the git blame I see things like @nikivazou 's commit

90439ba

I would try to run the above tests with simplifyCore switched off (e.g. --no-simplify-core?) to see them fail? It looks like we had various ad-hoc bandaids to get around this dependent-tuple problem...

[facundominguez]

--no-simplify-core causes DepTriples.hs to fail verification, indeed. Your test_fails function still passes verification.

[facundominguez]

One thought I had today: maybe it would be best for the user if LH desugared

{-@ uincr3 :: INCR3 @-}
uincr3 :: (Int, Int, Int)
uincr3 = let (x, y, z) = incr3
          in (x + 1, y + 1, z +1 )

as

{-@ uincr3 :: INCR3 @-}
uincr3 :: (Int, Int, Int)
uincr3 = case incr3 of
          (x, y, z) -> (x + 1, y + 1, z +1 )

Yes, it changes the meaning of uincr3, but not in a way that LH can tell apart. This desugaring could be used only for verification, and GHC would continue to desugar lets correctly for compilation.

There is a simplifyPatTuple transformation that attempts to transform core lets into a case expression too. From eval_safe in ple/pos/STLC1.hs

eval_safe g s (EVar x) t (E_Var {}) gs
  = R_Res w t wt
  where
    (w, (_, wt)) = lookup_safe g s x t gs

the right hand side is desugared to

  let {
    ds_d3fQ
      = case lookup_safe ds_d3ei ds_d3ej x_a1Ki ds_d3el ds_d3en of
          { (w_a1Kl, ds_d3fV) ->
             case ds_d3fV of { (_, wt_a1Km) -> (w_a1Kl, wt_a1Km) }
          } } in
  let { w_a1Kl = case ds_d3fQ of { (w_a1Kl, _) -> w_a1Kl } } in
  let { wt_a1Km = case ds_d3fQ of { (_, wt_a1Km) -> wt_a1Km } } in
  R_Res w_a1Kl ds_d3el wt_a1Km

which is then transformed to

  case lookup_safe ds_d3ei ds_d3ej x_a1Ki ds_d3el ds_d3en of
          { (w_a1Kl, ds_d3fV) ->
             case ds_d3fV of { (_, wt_a1Km) -> R_Res w_a1Kl ds_d3el wt_a1Km }
          }

This transformation might indeed break types in some unhappy cases. But it is notable that it is already quite happy to change the evaluation order, the same as my proposed desugaring.

[facundominguez]

Aha, I found something... See this:

I finally understood that transformation and documented it in b8ca539.

I'm going to try to generalize it a bit and to make it preserve types. There are cases where the desugaring of GHC doesn't match what the transformation expects as input.