panic with abstract refinement in local signature

ucsd-progsys / liquidhaskell

Liquid Types For Haskell

BSD 3-Clause "New" or "Revised" License

1.19k stars 139 forks source link

panic with abstract refinement in local signature #1855

Open ranjitjhala opened 3 years ago

ranjitjhala commented 3 years ago

See http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1626278397_36999.hs

{-@ type UList a = [a]<{\x y -> x /= y}> @-}

reverse :: [a] -> [a]
reverse         = go seed
  where
    {-@ seed :: UList a @-}
    seed = []
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

Due to @jllang https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/111

facundominguez commented 4 months ago

I cannot reproduce this in latest LH. It does require to move seed to the top level in order to give it a spec.