ucsd-progsys/liquidhaskell

drop autosize (was: autosize causes LH to forget field refinements)

Open

#1,942 建立於 2022年2月17日

在 GitHub 查看
 (4 留言) (0 反應) (0 負責人)Haskell (1,306 star) (157 fork)batch import
good first issue

描述

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.

貢獻者指南

drop autosize (was: autosize causes LH to forget field refinements) · ucsd-progsys/liquidhaskell#1942 | Good First Issue