Improve the environment of error messages

[facundominguez]

One deficiency of error messages in LH is that they don't contain all of the relevant bindings to understand the error.

Suppose we are trying to verify

{-@ LIQUID "--save"                       @-}
{-@ LIQUID "--reflection"                 @-}

module Test where

{-@ reflect append @-}
append :: [a] -> [a] -> [a]
append [] ys = ys
append (x:xs) ys = x : append xs ys

{-@ append_empty_right :: xs:[a] -> { append xs [] == xs } @-}
append_empty_right :: [a] -> ()
append_empty_right [] = ()
append_empty_right (x:xs) =
    case append (x:xs) [] of
      [] -> append_empty_right xs
      _ -> append_empty_right xs

Liquid Haskell says:

[1 of 1] Compiling Test             ( Test.hs, Test.o )
...
Saving prettified Query: ./.liquid/Test.hs.fq.prettified
...

**** LIQUID: UNSAFE ************************************************************
Test.hs:13:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : () | v == GHC.Tuple.()}
    .
    is not a subtype of the required type
      VV : {VV##718 : () | Test.append ?a GHC.Types.[] == ?a}
    .
    in the context
      ?a : {?a : [a] | len ?a >= 0}
    Constraint id 12
   |
13 | append_empty_right [] = ()
   |

If we look at constraint 12 in the dump ./.liquid/Test.hs.fq.prettified we find:

constraint:
  lhs {VV : Tuple | [(VV = GHC.Tuple.$40$$41$)]}
  rhs {VV : Tuple | [((Test.append ds_d22E GHC.Types.$91$$93$) =
                        ds_d22E)]}
  id 12 tag [3]
  // META constraint id 12 : Test.hs:13:25-26
  environment:
    // elided some likely irrelevant bindings
    
    ds_d22E : {VV : [a##aLE] | [((len VV) >= 0)]}
    
    _lq_anf$ :
      {lq_tmp$x : [a##aLE] |
         [(is$36$GHC.Types.$91$$93$ lq_tmp$x);
          (~ ((is$36$GHC.Types.$58$ lq_tmp$x)));
          (lq_tmp$x = GHC.Types.$91$$93$);
          (lq_tmp$x = ds_d22E);
          ((len lq_tmp$x) = 0);
          ((len lq_tmp$x) >= 0)]}

Note how _lq_anf$ is missing in the error message, yet it gives the useful fact that ?a == [] (which is my translation of lq_tmp$x = ds_d22E and lq_tmp$x = GHC.Types.$91$$93$). With this, it should be clear that the SMT solver isn't able to solve Test.append [] [] == [], and that such hypothesis needs to be brought via PLE or a manual proof.

_lq_anf$, and any other binding whose predicate mentions variables "relevant" to the constraint should be printed in the error message. The code that collects the bindings for the file dump is here. This issue is about plugging it, or otherwise doing something similar in the error message.

[ranjitjhala]

Hmm i thought that code collected all the relevant binding - I think ANF things are perhaps aggressively getting filtered out to keep the environment small? See the “tidyXYZ” functions…

[facundominguez]

I can confirm that tidyError seems to be dropping the lq_anf... binding, as the binding shows up when skipping this function.

[facundominguez]

lq_anf... is discarded twice in tidyError.

The first time, it is discarded in sliceREnv. sliceREnv collects the symbols of transitive dependencies of the subtyping constraint, and lq_anf... is not a dependency in such a sense. In contrast, the prettified query is including all bindings that contain any symbols that appear in the subtyping constraint. It looks to me like we should be calling here relatedSymbols instead, or something similar.

The second time, it is discarded in isInline' because it is considered a singleton Reft by isSingletonReft. isInline' discards all conjuncts in the predicate of the binding if it is considered a singleton. Is there any motivation for this? Otherwise, we could just stop discarding them.

[facundominguez]

With #2350 the error message shows as:

Test.hs:13:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : () | v == GHC.Tuple.()}
    .
    is not a subtype of the required type
      VV : {VV##718 : () | Test.append ?a GHC.Types.[] == ?a}
    .
    in the context
      ?a : {?a : [a] | len ?a >= 0}

      ?b : {?b : [a] | ?b == ?a
                       && ?b == GHC.Types.[]
                       && len ?b == 0
                       && len ?b >= 0}
    Constraint id 12
   |
13 | append_empty_right [] = ()
   |

[ranjitjhala]

This is much better, thanks so much!