search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 133 forks source link

Crash on holes inside Abstract Refinement Types #1525

Open nikivazou opened 5 years ago

nikivazou commented 5 years ago

e.g.,

φ :: (a -> a -> Bool) 
  -> (a, a -> Bool)
  -> a -> (a, Bool)

{-@
φ :: p:(a -> a -> Bool) 
  -> (x::a, y:a -> {p x y})
  -> z:a -> (w::a, {p w z})
@-}
φ p (x, pxy) = \y -> (x, pxy y)

crashes with 

 17 | φ p (x, pxy) = \y -> (x, pxy y)
      ^

     (Another Broken Test!!!) splitc unexpected:
rHole
  <:
rHole
facundominguez commented 3 months ago

In the latest LH I get a different error

    Illegal type specification for `Main.φ`
    Main.φ :: forall a .
              p:(lq_tmp$db##0:a -> lq_tmp$db##1:a -> GHC.Types.Bool) -> lq_tmp$db##3:(a, (y:a -> GHC.Types.Bool))<\x VV -> y:a -> {VV : _ | p x y}> -> z:a -> (a, GHC.Types.Bool)<\w VV -> {VV : GHC.Types.Bool | p w z}>
    Sort Error in Refinement: {VV : bool | p w z}
    Unbound symbol p --- perhaps you meant: z, w ?
    Just
  |
8 | φ :: p:(a -> a -> Bool) 
  |