ucsd-progsys/liquidhaskell
Auf GitHub ansehendrop autosize (was: autosize causes LH to forget field refinements)
Open
#1.942 geöffnet am 17. Feb. 2022
good first issue
Repository-Metriken
- Stars
- (1.306 Stars)
- PR-Merge-Metriken
- (Durchschn. Merge 2T 18h) (12 gemergte PRs in 30 T)
Beschreibung
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.