Merge pull request ucsd-progsys#2247 from ucsd-progsys/fd/ghc-9.6.3

Update liquidhaskell to build with GHC 9.6.3
tbidne · Dec 8, 2023 · 187201e · 187201e
2 parents b3a5ac9 + dd7d42d
commit 187201e
Show file tree

Hide file tree

Showing 55 changed files with 358 additions and 250 deletions.
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -60,7 +60,7 @@ commands:
             chmod +x ./x86_64-linux-ghcup
             ./x86_64-linux-ghcup install ghc << parameters.ghc_version >>
             ./x86_64-linux-ghcup set ghc << parameters.ghc_version >>
-            ./x86_64-linux-ghcup install cabal 3.6.2.0
+            ./x86_64-linux-ghcup install cabal 3.10.1.0
             export PATH=~/.ghcup/bin:$PATH
             echo 'export PATH=~/.ghcup/bin:$PATH' >> $BASH_ENV
             << parameters.cabal_update_command >>
@@ -127,15 +127,18 @@ commands:
           command: |
             stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> clean
             mkdir -p /tmp/junit/stack
-            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> run test-driver
-            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test tests:tasty
+            # the -package-db and -package arguments help work around https://github.com/commercialhaskell/stack/issues/6251
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build liquidhaskell-boot
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build liquidhaskell --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell-boot\""
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> run test-driver -- -- --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell\""
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test tests:tasty --ghc-options="\"-package-db $(stack path --snapshot-pkg-db)\"" --ghc-options="\"-package-db $(stack path --local-pkg-db)\"" --ghc-options="\"-package liquidhaskell\""
             stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> test -j1 liquidhaskell-boot << parameters.extra_build_flags >>
           no_output_timeout: 30m
       - run:
           name: Generate haddock
           command: |
             # stack haddock liquidhaskell --flag liquidhaskell:-devel --no-haddock-deps --haddock-arguments="--no-print-missing-docs --odir=$CIRCLE_ARTIFACTS"
-            # skip if extra_build_flags are set
+            # skip if extra_build_flags are set--ghc-options
             [ ! -z "<< parameters.extra_build_flags >>" ] || stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> haddock << parameters.extra_build_flags >> liquidhaskell  --no-haddock-deps --haddock-arguments="--no-print-missing-docs"
       - run:
           name: Dist
@@ -158,7 +161,7 @@ jobs:
       image: ubuntu-2004:202107-02
     steps:
       - cabal_build_and_test:
-          ghc_version: "9.4.7"
+          ghc_version: "9.6.3"
 
 workflows:
   version: 2

diff --git a/.github/workflows/cabal.yml b/.github/workflows/cabal.yml
@@ -0,0 +1,62 @@
+name: cabal
+
+on:
+  push:
+    - ci
+  pull_request:
+
+# NOTE: The setup-z3 action constructs the download filename from
+# z3-version-architecture-distribution. From z3-4.8.10 to z3-4.8.11, the z3
+# releases distribution name for use on ubuntu changed from ubuntu to
+# glibc-2.31.  SEE: https://github.com/Z3Prover/z3/releases
+jobs:
+  build:
+    name: ghc-${{ matrix.ghc }} z3-${{ matrix.z3 }}
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        cabal: ["3.10.1.0"]
+        ghc:
+          - "9.6.3"
+          - "9.4.7"
+          - "9.2.3"
+        z3:
+          - "4.10.2"
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: true
+
+      - name: Setup z3-4.10.2
+        uses: pavpanchekha/setup-z3@6b2d476d7a9227e0d8d2b94f73cd9fcba91b5e98
+        with:
+          version: ${{ matrix.z3 }}
+
+      - name: Workaround runner image issue
+        # https://github.com/actions/runner-images/issues/7061
+        run: sudo chown -R $USER /usr/local/.ghcup
+
+      - name: Setup GHC and cabal-install
+        uses: haskell/actions/setup@v2
+        with:
+          ghc-version: ${{ matrix.ghc }}
+          cabal-version: ${{ matrix.cabal }}
+
+      - name: Cache ~/.cabal/packages, ~/.cabal/store and dist-newstyle
+        uses: actions/cache@v3
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            dist-newstyle
+          key: ${{ runner.os }}-${{ matrix.ghc }}-cabal-${{ hashFiles('**/*.cabal', '**/cabal.project', '**/cabal.project.freeze') }}
+
+      - name: Update package list
+        run: cabal update
+
+      - name: Build
+        run: cabal build all --enable-tests
+
+      - name: Test
+        run: cabal test all --test-show-details=direct --test-option="--color=always"
diff --git a/README.md b/README.md
@@ -349,7 +349,7 @@ that can be tested with `./scripts/test/test_plugin.sh`.
 [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.4.7/docs/GHC-Core.html#t:CoreBind
+[core binds]:          https://hackage.haskell.org/package/ghc-9.6.3/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

diff --git a/benchmark-timings/benchmark-timings.cabal b/benchmark-timings/benchmark-timings.cabal
@@ -37,7 +37,7 @@ executable benchmark-timings
                     , aeson >= 1.5.6 && < 3
                     , cassava ^>=0.5.2
                     , bytestring >=0.10.12 && <0.12
-                    , optparse-applicative >=0.16.1 && <0.18
+                    , optparse-applicative >=0.16.1 && <0.19
     ghc-options:    -Wall
     hs-source-dirs:   app
     default-language: Haskell2010

diff --git a/cabal.project b/cabal.project
@@ -1,4 +1,4 @@
-with-compiler: ghc-9.4.7
+with-compiler: ghc-9.6.3
 
 packages: .
           ./liquid-fixpoint

diff --git a/docs/mkDocs/docs/install.md b/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.4.7`: use LiquidHaskell from github
+* `ghc-9.6.3`: use LiquidHaskell from github
+* `ghc-9.4.7`: use liquidhaskell-0.9.4.7.0 from Hackage
 * `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

diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal
@@ -126,7 +126,7 @@ library
                     , aeson
                     , binary
                     , bytestring           >= 0.10
-                    , Cabal                < 3.9
+                    , Cabal                < 3.11
                     , cereal
                     , cmdargs              >= 0.10
                     , containers           >= 0.5
@@ -136,7 +136,7 @@ library
                     , filepath             >= 1.3
                     , fingertree           >= 0.1
                     , exceptions           < 0.11
-                    , ghc                  ^>= 9.4
+                    , ghc                  ^>= 9.6
                     , ghc-boot
                     , ghc-paths            >= 0.1
                     , ghc-prim
@@ -145,7 +145,7 @@ library
                     , hscolour             >= 1.22
                     , liquid-fixpoint      == 0.9.4.7
                     , mtl                  >= 2.1
-                    , optparse-applicative < 0.18
+                    , optparse-applicative < 0.19
                     , githash
                     , megaparsec           >= 8
                     , pretty               >= 1.1

diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
@@ -10,6 +10,7 @@ it easy to discover breaking changes in the GHC API.
 
 -}
 
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 module Liquid.GHC.API (
@@ -19,8 +20,7 @@ module Liquid.GHC.API (
 import Liquid.GHC.API.Extra as Ghc
 
 import           GHC                  as Ghc
-    ( Backend(Interpreter)
-    , Class
+    ( Class
     , DataCon
     , DesugaredModule(DesugaredModule, dm_typechecked_module, dm_core_module)
     , DynFlags(backend, debugLevel, ghcLink, ghcMode)
@@ -102,7 +102,6 @@ import           GHC                  as Ghc
     , isDictonaryId
     , isExternalName
     , isFamilyTyCon
-    , isFunTyCon
     , isGoodSrcSpan
     , isLocalId
     , isNewTyCon
@@ -216,7 +215,8 @@ import GHC.Builtin.Types              as Ghc
     , typeSymbolKind
     )
 import GHC.Builtin.Types.Prim         as Ghc
-    ( eqPrimTyCon
+    ( isArrowTyCon
+    , eqPrimTyCon
     , eqReprPrimTyCon
     , primTyCons
     )
@@ -322,19 +322,22 @@ import GHC.Core.Reduction             as Ghc
     ( Reduction(Reduction) )
 import GHC.Core.Subst                 as Ghc (emptySubst, extendCvSubst)
 import GHC.Core.TyCo.Rep              as Ghc
-    ( AnonArgFlag(VisArg)
-    , ArgFlag(Required)
+    ( FunTyFlag(FTF_T_T)
+    , ForAllTyFlag(Required)
     , Coercion
         ( AppCo
         , AxiomRuleCo
         , AxiomInstCo
         , CoVarCo
         , ForAllCo
         , FunCo
+        , HoleCo
         , InstCo
         , KindCo
         , LRCo
-        , NthCo
+        , Refl
+        , GRefl
+        , SelCo
         , SubCo
         , SymCo
         , TransCo
@@ -355,12 +358,12 @@ import GHC.Core.TyCo.Rep              as Ghc
         , ft_res
         )
     , UnivCoProvenance(PhantomProv, ProofIrrelProv)
-    , binderVar
     , mkForAllTys
     , mkFunTy
     , mkTyVarTy
     , mkTyVarTys
     )
+import GHC.Core.TyCo.Compare          as Ghc (eqType, nonDetCmpType)
 import GHC.Core.TyCon                 as Ghc
     ( TyConBinder
     , TyConBndrVis(AnonTCB)
@@ -382,20 +385,18 @@ import GHC.Core.TyCon                 as Ghc
 import GHC.Core.Type                  as Ghc
     ( Specificity(SpecifiedSpec)
     , TyVarBinder
-    , pattern Many
-    , classifiesTypeWithValues
+    , isTYPEorCONSTRAINT
     , dropForAlls
     , emptyTvSubstEnv
-    , eqType
     , expandTypeSynonyms
     , irrelevantMult
     , isFunTy
     , isTyVar
     , isTyVarTy
+    , pattern ManyTy
     , mkTvSubstPrs
     , mkTyConApp
     , newTyConInstRhs
-    , nonDetCmpType
     , piResultTys
     , splitAppTys
     , splitFunTy_maybe
@@ -421,14 +422,16 @@ import GHC.Data.FastString            as Ghc
     , fsLit
     , mkFastString
     , mkFastStringByteString
-    , mkPtrString
+    , mkPtrString#
     , uniq
     , unpackFS
     )
 import GHC.Data.Pair                  as Ghc
     ( Pair(Pair) )
 import GHC.Driver.Config.Diagnostic as Ghc
-    ( initDiagOpts )
+    ( initDiagOpts
+    , initDsMessageOpts
+    )
 import GHC.Driver.Main                as Ghc
     ( hscDesugar
     , hscTcRcLookupName
@@ -460,6 +463,7 @@ import GHC.Plugins                    as Ghc ( deserializeWithData
 import GHC.Core.FVs                   as Ghc (exprFreeVarsList)
 import GHC.Core.Opt.OccurAnal         as Ghc
     ( occurAnalysePgm )
+import GHC.Driver.Backend             as Ghc (interpreterBackend)
 import GHC.Driver.Env                 as Ghc
     ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) )
 import GHC.Driver.Errors              as Ghc
@@ -477,7 +481,7 @@ import GHC.Iface.Load                 as Ghc
 import GHC.Rename.Expr                as Ghc (rnLExpr)
 import GHC.Rename.Names               as Ghc (renamePkgQual)
 import GHC.Tc.Errors.Types            as Ghc
-    ( TcRnMessage(TcRnUnknownMessage) )
+    ( mkTcRnUnknownMessage )
 import GHC.Tc.Gen.App                 as Ghc (tcInferSigma)
 import GHC.Tc.Gen.Bind                as Ghc (tcValBinds)
 import GHC.Tc.Gen.Expr                as Ghc (tcInferRho)
@@ -549,6 +553,7 @@ import GHC.Types.CostCentre           as Ghc
 import GHC.Types.Error                as Ghc
     ( Messages(getMessages)
     , MessageClass(MCDiagnostic)
+    , Diagnostic(defaultDiagnosticOpts)
     , DiagnosticReason(WarningWithoutFlag)
     , MsgEnvelope(errMsgSpan)
     , errorsOrFatalWarningsFound
@@ -653,6 +658,7 @@ import GHC.Types.Unique.Supply        as Ghc
     ( MonadUnique, getUniqueM )
 import GHC.Types.Var                  as Ghc
     ( VarBndr(Bndr)
+    , binderVar
     , mkLocalVar
     , mkTyVar
     , setVarName

diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs
@@ -82,7 +82,7 @@ tyConRealArity tc = go 0 (tyConKind tc)
   where
     go :: Int -> Kind -> Int
     go !acc k =
-      case asum [fmap (\(_, _, c) -> c) (splitFunTy_maybe k), fmap snd (splitForAllTyCoVar_maybe k)] of
+      case asum [fmap (\(_, _, _, c) -> c) (splitFunTy_maybe k), fmap snd (splitForAllTyCoVar_maybe k)] of
         Nothing -> acc
         Just ks -> go (acc + 1) ks
 
@@ -192,7 +192,7 @@ data ApiComment
 apiComments :: ParsedModule -> [Ghc.Located ApiComment]
 apiComments pm = apiCommentsParsedSource (pm_parsed_source pm)
 
-apiCommentsParsedSource :: Located HsModule -> [Ghc.Located ApiComment]
+apiCommentsParsedSource :: Located (HsModule GhcPs) -> [Ghc.Located ApiComment]
 apiCommentsParsedSource ps =
     let hs = unLoc ps
         go :: forall a. Data a => a -> [LEpaComment]
@@ -281,7 +281,7 @@ showSDocQualified = Ghc.renderWithContext ctx
     style = Ghc.mkUserStyle myQualify Ghc.AllTheWay
     ctx = Ghc.defaultSDocContext { sdocStyle = style }
 
-myQualify :: Ghc.PrintUnqualified
+myQualify :: Ghc.NamePprCtx
 myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }
 -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }
 

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -21,6 +21,7 @@ module Language.Haskell.Liquid.Bare.DataType
   ) where
 
 import qualified Control.Exception                      as Ex
+import           Control.Monad (forM, unless)
 import           Control.Monad.Reader
 import qualified Data.List                              as L
 import qualified Data.HashMap.Strict                    as M

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
@@ -17,6 +17,7 @@ import           Prelude                               hiding (error)
 
 import           Liquid.GHC.API       as Ghc  hiding (Located, showPpr)
 
+import           Control.Monad                         (zipWithM_)
 import           Control.Monad.Except                  (MonadError, throwError)
 import           Control.Monad.State
 import qualified Data.Maybe                            as Mb --(fromMaybe, isNothing)
@@ -152,7 +153,7 @@ mapTyVars _ hsT lqT
        throwError (err (F.pprint hsT) (F.pprint lqT))
 
 isKind :: Kind -> Bool
-isKind = classifiesTypeWithValues -- TODO:GHC-863 isStarKind k --  typeKind k
+isKind = isTYPEorCONSTRAINT -- TODO:GHC-863 isStarKind k --  typeKind k
 
 
 mapTyRVar :: MonadError Error m

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -140,7 +140,7 @@ plugMany allowTC embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes)
   where
     ((xs,_,ts,_), t) = bkArrow (val pT)
     pT               = plugHoles allowTC (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
-    hsT              = foldr (Ghc.mkFunTy Ghc.VisArg Ghc.Many) hsRes hsArgs'
+    hsT              = foldr (Ghc.mkFunTy Ghc.FTF_T_T Ghc.ManyTy) hsRes hsArgs'
     lqT              = foldr (uncurry (rFun' (classRFInfo allowTC))) lqRes lqArgs'
     hsArgs'          = [ Ghc.mkTyVarTy a               | a <- hsAs] ++ hsArgs
     lqArgs'          = [(F.dummySymbol, RVar a mempty) | a <- lqAs] ++ lqArgs