liquidhaskell icon indicating copy to clipboard operation
liquidhaskell copied to clipboard

Nonnegativity predicate in Integral class

Open amigalemming opened this issue 7 months ago • 1 comments

I try to define a data type that is refined by a nonnegativity constraint. Since the numeric type is polymorphic I tried this:

module Example.IntegralNonneg where

{-@ inline nonneg @-}
nonneg :: (Integral n) => n -> Bool
nonneg n = n >= 0

{-@ Segment :: (Integral n) => n -> {nn:n | nonneg nn} -> Segment n @-}
data Segment n = Segment {start, size :: n}

I get Liquid errors like this one:

src/Example/IntegralNonneg.hs:5:1: error:
    Illegal type specification for `Example.IntegralNonneg.nonneg`
    Example.IntegralNonneg.nonneg :: forall n .
                                     (Integral<[]> n) =>
                                     x##2:n -> {VV : GHC.Types.Bool | VV <=> x##2 >= GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 0)}
    Sort Error in Refinement: {VV : bool | VV <=> x##2 >= GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 0)}
    Unbound symbol GHC.Internal.Num.fromInteger --- perhaps you meant: GHC.Internal.Base.., GHC.Internal.Maybe.Just, GHC.Internal.Maybe.Nothing ?
    Just
  |
5 | nonneg n = n >= 0
  | ^^^^^^

So, it seems Liquid Haskell has no knowledge about the implicit Prelude.fromInteger in order to type check even the nonneg predicate. Is there a way to achieve what I want?

amigalemming avatar May 07 '25 19:05 amigalemming

Inlining a function that uses type classes could be problematic. This might be related to the bit-rotted support for type classes (#2450).

facundominguez avatar May 09 '25 18:05 facundominguez