Bump version of liquid-vector to 0.13.1.0

README.md

@@ -339,33 +339,17 @@ patter synonym to deal with changes in type constructors.
 Currently, no. Only one version of GHC is supported and that is the one
 that can be tested with `./scripts/test/test_plugin.sh`.
 
-# GHC Plugin Development FAQs
-
-## Why is the GHC.Interface using slightly different types than the GHC.Plugin module?
-
-Mostly for backward-compatibility and for historical reasons. Types like [BareSpec][] used to be type alias
-rather than `newtype`s, and things were slightly renamed to reflect better purpose when the support for the
-plugin was added. While doing so we also added a compatibility layer in the form of some `optics` that can be used
-to map back and forth (sometimes in a partial way) between old and new data structures. When in doubt,
-**consider the GHC.Plugin as the single source of truth, and prefer whichever data structure the latter is
-using**.
-
 [GHC.API]:             liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
 [Plugin]:              liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
 [GHC.Plugin]:          liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
 [GHC.Interface]:       liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
 [SpecFinder]:          liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
-[BareSpec]:            liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L362
 [LiftedSpec]:          liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L559
 [TargetSrc]:           liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L158
-[Ghc monad]:           https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:Ghc
-[HscEnv]:              https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:HscEnv
-[DynFlags]:            https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:DynFlags
-[GhcMonad]:            https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:GhcMonad
 [typechecking phase]:  liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L211-L226
 [ghcide]:              https://github.com/haskell/ghcide
 [findRelevantSpecs]:   liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L65
-[core binds]:          https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC-Core.html#t:CoreBind
+[core binds]:          https://hackage.haskell.org/package/ghc-9.4.7/docs/GHC-Core.html#t:CoreBind
 [configureGhcTargets]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L254
 [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483
 [processModule]:       liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509

docs/mkDocs/docs/install.md

@@ -19,7 +19,8 @@ LiquidHaskell itself is installed&enabled by adding it as a dependency in your p
 
 Depending on your version of GHC, you might want to use a build of LiquidHaskell from github or from Hackage.
 
-* `ghc-9.2.8`: use LiquidHaskell from github
+* `ghc-9.4.7`: use LiquidHaskell from github
+* `ghc-9.2.8`: use liquidhaskell-0.9.2.8.0 from Hackage
 * `ghc-9.2.5`: use liquidhaskell-0.9.2.5.0 from Hackage
 * `ghc-9.0.2`: use liquidhaskell-0.9.0.2.1 and liquid-base-0.4.15.1.0 from Hackage
 * `ghc-8.10.7`: use liquidhaskell-0.8.10.7 and liquid-base-0.4.15.0.0 from Hackage

liquid-platform/liquid-platform.cabal

@@ -28,7 +28,7 @@ executable liquidhaskell
     build-depends:      base       >= 4.15.1.0 && < 5
                       , containers >= 0.6.4.1  && < 0.7
                       , liquid-prelude    >= 0.9.2.8
-                      , liquid-vector     >= 0.12.3.1.2
+                      , liquid-vector     >= 0.13.1.0
                       , liquidhaskell     >= 0.9.2.8
                       , liquidhaskell-boot >= 0.9.2.8
                       , filepath

liquid-vector/liquid-vector.cabal

@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-vector
-version:            0.12.3.1.2
+version:            0.13.1.0
 synopsis:           LiquidHaskell specs for the vector package
 description:        LiquidHaskell specs for the vector package.
 license:            BSD3
@@ -19,7 +19,7 @@ library
   exposed-modules:    Data.Vector_LHAssumptions
   hs-source-dirs:     src
   build-depends:      base          < 5
-                    , vector               >= 0.12.3.1 && < 0.14
+                    , vector               >= 0.13.1.0 && < 0.14
                     , liquidhaskell        >= 0.9.2.8
   default-language:   Haskell2010
   default-extensions: PackageImports

liquidhaskell-boot/ghc-api-tests/GhcApiTests.hs

@@ -7,6 +7,8 @@ import           Liquid.GHC.API
     , Expr(..)
     , Alt(..)
     , AltCon(..)
+    , LitNumType(..)
+    , Literal(..)
     , apiCommentsParsedSource
     , occNameString
     , pAT_ERROR_ID
@@ -17,13 +19,16 @@ import           Test.Tasty.HUnit
 import           Test.Tasty.Runners.AntXML
 
 import qualified GHC as GHC
+import qualified GHC.Builtin.Names as GHC
+import qualified GHC.Builtin.Types as GHC
 import qualified GHC.Core as GHC
 import qualified GHC.Data.EnumSet as EnumSet
 import qualified GHC.Data.FastString as GHC
 import qualified GHC.Data.StringBuffer as GHC
 import qualified GHC.Parser as Parser
 import qualified GHC.Parser.Lexer as GHC
-import qualified GHC.Types.Name.Occurrence as GHC
+import qualified GHC.Types.Id as GHC
+import qualified GHC.Types.Name as GHC
 import qualified GHC.Types.SrcLoc as GHC
 import qualified GHC.Unit.Module.ModGuts as GHC
 import qualified GHC.Utils.Error as GHC
@@ -41,6 +46,7 @@ testTree =
     testGroup "GHC API"
       [ testCase "apiComments" testApiComments
       , testCase "caseDesugaring" testCaseDesugaring
+      , testCase "numericLiteralDesugaring" testNumLitDesugaring
       ]
 
 -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in
@@ -132,27 +138,61 @@ testCaseDesugaring = do
             -> e3 == pAT_ERROR_ID
           _ -> False
 
-    coreProgram <- compileToCore inputSource
+    coreProgram <- compileToCore "CaseDesugaring" inputSource
     unless (isExpectedDesugaring coreProgram) $
       fail $ unlines $
         "Unexpected desugaring:" : map showPprQualified coreProgram
-  where
-    compileToCore inputSource = do
-      now <- getCurrentTime
-      GHC.runGhc (Just libdir) $ do
-        df1 <- GHC.getSessionDynFlags
-        GHC.setSessionDynFlags df1
-        let target = GHC.Target {
-                     GHC.targetId           = GHC.TargetFile "CaseDesugaring.hs" Nothing
-                   , GHC.targetUnitId       = GHC.homeUnitId_ df1
-                   , GHC.targetAllowObjCode = False
-                   , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)
-                   }
-        GHC.setTargets [target]
-        void $ GHC.load GHC.LoadAllTargets
-
-        dsMod <- GHC.getModSummary (GHC.mkModuleName "CaseDesugaring")
-               >>= GHC.parseModule
-               >>= GHC.typecheckModule
-               >>= GHC.desugarModule
-        return $ GHC.mg_binds $ GHC.dm_core_module dsMod
+
+-- | Tests that numeric literal expressions desugar as Liquid Haskell expects.
+testNumLitDesugaring :: IO ()
+testNumLitDesugaring = do
+    let inputSource = unlines
+          [ "module NumLitDesugaring where"
+          , "f :: Num a => a"
+          , "f = 1"
+          ]
+
+        fBind (GHC.NonRec b _e) =
+          occNameString (GHC.occName b) == "f"
+        fBind _ = False
+
+        -- Expected desugaring:
+        --
+        -- NumLitDesugaring.f
+        --      = \@a dict -> fromInteger @a dict (GHC.Num.Integer.IS 1#)
+        --
+        isExpectedDesugaring p = case find fBind p of
+          Just (GHC.NonRec _ e0)
+            | Lam _a (Lam _dict (App fromIntegerApp (App (Var vIS) lit))) <- e0
+            , App (App (Var vFromInteger) _aty) _numDict <- fromIntegerApp
+            , GHC.idName vFromInteger  == GHC.fromIntegerName
+            , GHC.nameStableString (GHC.idName vIS) == GHC.nameStableString GHC.integerISDataConName
+            , Lit (LitNumber LitNumInt 1) <- lit
+            -> True
+          _ -> False
+
+    coreProgram <- compileToCore "NumLitDesugaring" inputSource
+    unless (isExpectedDesugaring coreProgram) $
+      fail $ unlines $
+        "Unexpected desugaring:" : map showPprQualified coreProgram
+
+compileToCore :: String -> String -> IO [GHC.CoreBind]
+compileToCore modName inputSource = do
+    now <- getCurrentTime
+    GHC.runGhc (Just libdir) $ do
+      df1 <- GHC.getSessionDynFlags
+      GHC.setSessionDynFlags df1
+      let target = GHC.Target {
+                   GHC.targetId           = GHC.TargetFile (modName ++ ".hs") Nothing
+                 , GHC.targetUnitId       = GHC.homeUnitId_ df1
+                 , GHC.targetAllowObjCode = False
+                 , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)
+                 }
+      GHC.setTargets [target]
+      void $ GHC.load GHC.LoadAllTargets
+
+      dsMod <- GHC.getModSummary (GHC.mkModuleName modName)
+             >>= GHC.parseModule
+             >>= GHC.typecheckModule
+             >>= GHC.desugarModule
+      return $ GHC.mg_binds $ GHC.dm_core_module dsMod

stack.yaml

@@ -27,7 +27,6 @@ extra-deps:
 - smtlib-backends-process-0.3
 - git: https://github.com/qnikst/ghc-timings-report
   commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
-- vector-0.12.3.1
 # for tests
 - strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
 

stack.yaml.lock

@@ -36,13 +36,6 @@ packages:
   original:
     commit: 45ef3498e35897712bde8e002ce18df6d55f8b15
     git: https://github.com/qnikst/ghc-timings-report
-- completed:
-    hackage: vector-0.12.3.1@sha256:39141f312871b7c793a63be76635999e84d442aa3290aec59f30638ec0bf23a7,8218
-    pantry-tree:
-      sha256: c4f50de0598ce416df3a8f01ad7f23d8f1282ef3c5c531d67afe15b1e14a5d8d
-      size: 3842
-  original:
-    hackage: vector-0.12.3.1
 - completed:
     hackage: strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
     pantry-tree:

tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Optimal.hs

@@ -66,8 +66,8 @@ sort2ByOffset cmp a off = sort2ByIndex cmp a off (off + 1)
   @-}
 sort2ByIndex :: (PrimMonad m, MVector v e)
              => Comparison e -> v (PrimState m) e -> Int -> Int -> m ()
-sort2ByIndex cmp a i j = UNSAFE_CHECK(checkIndex) "sort2ByIndex" i (length a)
-                       $ UNSAFE_CHECK(checkIndex) "sort2ByIndex" j (length a)  $  do
+sort2ByIndex cmp a i j = UNSAFE_CHECK(checkIndex) i (length a)
+                       $ UNSAFE_CHECK(checkIndex) j (length a)  $  do
   a0 <- unsafeRead a i
   a1 <- unsafeRead a j
   case cmp a0 a1 of
@@ -99,9 +99,9 @@ sort3ByOffset cmp a off = sort3ByIndex cmp a  off  (off + 1) (off + 2)
   @-}
 sort3ByIndex :: (PrimMonad m, MVector v e)
              => Comparison e -> v (PrimState m) e -> Int -> Int -> Int -> m ()
-sort3ByIndex cmp a i j k = UNSAFE_CHECK(checkIndex) "sort3ByIndex" i (length a)
-                         $ UNSAFE_CHECK(checkIndex) "sort3ByIndex" j (length a)
-                         $ UNSAFE_CHECK(checkIndex) "sort3ByIndex" k (length a) $ do
+sort3ByIndex cmp a i j k = UNSAFE_CHECK(checkIndex) i (length a)
+                         $ UNSAFE_CHECK(checkIndex) j (length a)
+                         $ UNSAFE_CHECK(checkIndex) k (length a) $ do
   a0 <- unsafeRead a i
   a1 <- unsafeRead a j
   a2 <- unsafeRead a k
@@ -151,10 +151,10 @@ sort4ByOffset cmp a off = sort4ByIndex cmp a off (off + 1) (off + 2) (off + 3)
   @-}
 sort4ByIndex :: (PrimMonad m, MVector v e)
              => Comparison e -> v (PrimState m) e -> Int -> Int -> Int -> Int -> m ()
-sort4ByIndex cmp a i j k l = UNSAFE_CHECK(checkIndex) "sort4ByIndex" i (length a)
-                           $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" j (length a)
-                           $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" k (length a)
-                           $ UNSAFE_CHECK(checkIndex) "sort4ByIndex" l (length a) $ do
+sort4ByIndex cmp a i j k l = UNSAFE_CHECK(checkIndex) i (length a)
+                           $ UNSAFE_CHECK(checkIndex) j (length a)
+                           $ UNSAFE_CHECK(checkIndex) k (length a)
+                           $ UNSAFE_CHECK(checkIndex) l (length a) $ do
   a0 <- unsafeRead a i
   a1 <- unsafeRead a j
   a2 <- unsafeRead a k

tests/benchmarks/vector-algorithms-0.5.4.2/include/vector.h

@@ -11,7 +11,7 @@ import qualified Data.Vector.Internal.Check as Ck
 #define ERROR(f)  (Ck.f __FILE__ __LINE__)
 #define ASSERT (Ck.assert __FILE__ __LINE__)
 #define ENSURE (Ck.f __FILE__ __LINE__)
-#define CHECK(f) (Ck.f __FILE__ __LINE__)
+#define CHECK(f) (Ck.f)
 
 #define BOUNDS_ERROR(f) (ERROR(f) Ck.Bounds)
 #define BOUNDS_ASSERT (ASSERT Ck.Bounds)

tests/errors/SplitSubtype.hs

@@ -1,4 +1,4 @@
-{-@ LIQUID "--expect-error-containing=| VV > 5}" @-}
+{-@ LIQUID "--expect-error-containing=> 5}" @-}
 module SplitSubtype where
 
 {-@ foo :: {v:Int | v > 0 && v > 5 && v < 10 } -> Int @-}