Facundo Domínguez
Facundo Domínguez
Fixed by #2339.
`resolveLogicNames` calls to `emapSpecM`, which computes the local variables at each location. As I understand it, `v` in this example is a local variable bound by `v :: Int`. However,...
Hello @trinhtuanlong. Which is your GHC version? I tried your example and had to add an annotation: ``` {-@ data Vec2 a = Vec2 { x :: a, y ::...
The way I think about it, the constraint only assumes that `plen ptr >= size (deref ptr)`. To prove that `plen ptr > 0`, we would need in addition the...
I don't think this code is going to work. ```Haskell let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a) ``` `sizeOf (undefined :: Vec2 a)` has...
The method `pokeByteOff` is used by the default implementation of the method `pokeElemOff`. Strengthening the specification of the former must be causing the error in the later. Adding an implementation...
They do the same thing. But when type checking `const a b` the constraint that Liquid Haskell produces includes in the hypotheses the refinement types of both `a` and `b`....
> but somehow sizeOf anything works? Looking at the constraints that LH is producing, `sizeOf undefined` is introducing `false` as an hypothesis, which allows to any statement to be admitted....
Ensuring the instances are correct is going to require either messing with the instance specifications as you were trying before, or moving the body of the methods to top level...
We don't need to parse error messages anymore. But if LH is ignoring `-ddump-json`, maybe it means that LH is failing to use some intended mechanism to report the errors...