Allow LH to understand integer literals using GHC.Num.Integer.IS

Fixes #2237

liquidhaskell.cabal

@@ -57,6 +57,7 @@ library
                       GHC.IO.Handle_LHAssumptions
                       GHC.List_LHAssumptions
                       GHC.Num_LHAssumptions
+                      GHC.Num.Integer_LHAssumptions
                       GHC.Maybe_LHAssumptions
                       GHC.Ptr_LHAssumptions
                       GHC.Real_LHAssumptions
@@ -80,6 +81,7 @@ library
                       liquidhaskell-boot   == 0.9.2.8.0,
                       bytestring           == 0.11.4.0,
                       containers           == 0.6.5.1,
+                      ghc-bignum,
                       ghc-prim
   default-language:   Haskell98
   ghc-options:        -Wall -fplugin=LiquidHaskellBoot

src/GHC/Num/Integer_LHAssumptions.hs

@@ -0,0 +1,12 @@
+{-# LANGUAGE MagicHash #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+module GHC.Num.Integer_LHAssumptions() where
+
+import GHC.Types
+import GHC.Num.Integer
+import GHC.Types_LHAssumptions()
+
+
+{-@
+assume GHC.Num.Integer.IS :: x:GHC.Prim.Int# -> {v: GHC.Num.Integer | v = (x :: int) }
+@-}

tests/pos/T2237.hs

@@ -0,0 +1,12 @@
+{-# LANGUAGE MagicHash #-}
+-- | Tests that LH can reason with literals using the IS data constructor
+module T2237 () where
+
+import Language.Haskell.Liquid.Prelude (liquidError, liquidAssertB)
+import qualified GHC.Num.Integer
+
+data Foo a = F a
+
+{-@ flibInt :: (Num a, Ord a) => a -> Bool @-}
+flibInt x     = prop1 x (F (x + fromInteger (GHC.Num.Integer.IS 1#)))
+prop1 x (F y) = liquidAssertB (x < y)

tests/tests.cabal

@@ -1615,6 +1615,7 @@ executable unit-pos-1
                     , T2093
                     , T2096
                     , T2235
+                    , T2237
                     , T385
                     , T531
                     , T595a