liquidhaskell icon indicating copy to clipboard operation
liquidhaskell copied to clipboard

Liquid errors trump Haskell 98 errors

Open yanhasu opened this issue 3 years ago • 1 comments

Liquid Haskell occasionally replaces helpful GHC error massages with mysterious 'elaborate solver' errors.

For example, the following code contains a 'normal' type error (I forgot some parentheses):

module BugReport where

{-@ prop_bug :: {b:Bool | b} @-}
prop_bug :: Bool
prop_bug = not 1 + 2 > 100

When I delete the liquid type annotation, GHC tells me:

* No instance for (Num Bool) arising from a use of `+'
* In the first argument of `(>)', namely `not 1 + 2'
  In the expression: not 1 + 2 > 100
  In an equation for `prop_bug': prop_bug = not 1 + 2 > 100

as expected.

However, if I run the code as-is, Liquid Haskell complains:

**** LIQUID: ERROR :1:1-1:1: Error
  elaborate solver elabBE 85 "lq_anf$##7205759403792840661##dcf3" {lq_tmp$x##405 : bool | [(lq_tmp$x##405 = lq_anf$##7205759403792840660##dcf2)]} failed on:
      lq_tmp$x##405 == lq_anf$##7205759403792840660##dcf2
  with error
      The sort bool is not numeric
  because
Cannot unify bool with int in expression: lq_tmp$x##405 == lq_anf$##7205759403792840660##dcf2 
  because
Elaborate fails on lq_tmp$x##405 == lq_anf$##7205759403792840660##dcf2
  in environment
      lq_anf$##7205759403792840660##dcf2 := int

      lq_tmp$x##405 := bool 

and the original GHC error does not appear at all.

I'm using Liquid Haskell as a GHC plugin, through a cabal v2-repl on top of the tutorial repository.

yanhasu avatar Jun 29 '21 14:06 yanhasu

Oops that’s nasty - thanks for pointing it out, will fix ASAP!

ranjitjhala avatar Jun 29 '21 15:06 ranjitjhala