liquidhaskell
liquidhaskell copied to clipboard
Nonnegativity predicate in Integral class
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?
Inlining a function that uses type classes could be problematic. This might be related to the bit-rotted support for type classes (#2450).