liquidhaskell
liquidhaskell copied to clipboard
Liquid errors trump Haskell 98 errors
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.
Oops that’s nasty - thanks for pointing it out, will fix ASAP!