ucsd-progsys/liquidhaskell
View on GitHubdrop autosize (was: autosize causes LH to forget field refinements)
Open
#1,942 opened on Feb 17, 2022
good first issue
Repository metrics
- Stars
- (1,306 stars)
- PR merge metrics
- (Avg merge 2d 18h) (12 merged PRs in 30d)
Description
Liquid Haskell accepts this program:
{-@
data Term
= Var ({ i:Int | 0 <= i })
| Let Term Term
| Lit Int
@-}
data Term
= Var Int -- de bruijn index
| Let Term Term
| Lit Int
{-@ freeVarBound :: Term -> { i:Int | 0 <= i } @-}
freeVarBound :: Term -> Int
freeVarBound t = case t of
Var v -> v + 1
Lit _ -> 0
Let a b ->
let a' = freeVarBound a
b' = freeVarBound b - 1
in if a' > b' then a' else b'
However, if I add
{-@ autosize Term @-}
Then, Liquid Haskell rejects the program with:
src/Tester.hs:25:12: error:
Liquid Type Mismatch
.
The inferred type
VV : {v' : GHC.Types.Int | v' == v + (1 : int)}
.
is not a subtype of the required type
VV : {VV : GHC.Types.Int | 0 <= VV}
.
in the context
v : GHC.Types.Int
Constraint id 6
|
25 | Var v -> v + 1
| ^^^^^
It seems like the refinement of the field inside of Var is discarded by LH when the autosize is used.