{-@ LIQUID "--expect-any-error" @-} module ConstraintsAppend () where {-@ LIQUID "--no-termination" @-} import Language.Haskell.Liquid.Prelude {-@ type OList a = [a]<{\x v -> v >= x}> @-} {-@ app :: forall
Bool, q :: a -> Bool, r :: a -> Bool>. {x::a
|- a <: a ) -> OList (a <: {v:a| x <= v}}
{a
<: a
) -> OList a