Merge pull request #2417 from ucsd-progsys/NumDef

define nums

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs

@@ -27,6 +27,8 @@ coreToLogic = unlines
   , "define GHC.Types.True                 = (true)"
   , "define GHC.Internal.Real.div x y      = (x / y)"
   , "define GHC.Internal.Real.mod x y      = (x mod y)"
+  , "define GHC.Internal.Num.fromInteger x = (x)"
+  , "define GHC.Num.Integer.IS x           = (x)"
   , "define GHC.Classes.not x              = (~ x)"
   , "define GHC.Internal.Base.$ f x        = (f x)"
   , ""

tests/pos/NumRefl.hs

@@ -0,0 +1,27 @@
+{-
+
+Without the 
+  define GHC.Internal.Num.fromInteger x = (x)
+  define GHC.Num.Integer.IS             = (x)
+
+this program crashes with: 
+
+    Illegal type specification for `NumRefl.toNum`
+    NumRefl.toNum :: forall p .
+                     (Num<[]> p) =>
+                     lq1:() -> {VV : p | VV == NumRefl.toNum lq1
+                                         && VV == (-GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 1))}
+    Sort Error in Refinement: {VV : p##aMJ | VV == NumRefl.toNum lq1
+                                             && VV == (-GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 1))}
+    The sort @(176) is not numeric
+
+Because the resule type (Num p) => p cannot be decided to be a numeric type.
+-}
+
+module NumRefl where
+
+{-@ reflect toNum @-}
+toNum :: Num p => () -> p
+toNum _ = -1
+
+

tests/tests.cabal

@@ -1859,7 +1859,8 @@ executable unit-pos-3
       buildable:      False
 
     other-modules:
-                      Streams
+                      NumRefl
+                    , Streams
                     , StrictPair0
                     , StrictPair1
                     , String00