Update liquidhaskell to build with GHC 9.6.3

.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

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

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

cabal.project

@@ -1,4 +1,4 @@
-with-compiler: ghc-9.4.7
+with-compiler: ghc-9.6.3
 
 packages: .
           ./liquid-fixpoint

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

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,16 +136,16 @@ library
                     , filepath             >= 1.3
                     , fingertree           >= 0.1
                     , exceptions           < 0.11
-                    , ghc                  ^>= 9.4
+                    , ghc                  ^>= 9.6
                     , ghc-boot
                     , ghc-paths            >= 0.1
                     , ghc-prim
                     , gitrev
                     , hashable             >= 1.3 && < 1.5
                     , hscolour             >= 1.22
-                    , liquid-fixpoint      == 0.9.2.5
+                    , liquid-fixpoint      == 0.9.4.7
                     , mtl                  >= 2.1
-                    , optparse-applicative < 0.18
+                    , optparse-applicative < 0.19
                     , githash
                     , megaparsec           >= 8
                     , pretty               >= 1.1

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

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 }
 

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

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

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

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -183,11 +183,35 @@ makeSymMap src = Misc.group [ (sym, (m, x))
 
 makeTyThingMap :: GhcSrc -> TyThingMap
 makeTyThingMap src =
+  addListTyConName $
   Misc.group [ (x, (m, t))  | t         <- srcThings src
                             , tSym      <- Mb.maybeToList (tyThingSymbol t)
                             , let (m, x) = qualifiedSymbol tSym
                             , not (isLocal m)
              ]
+  where
+    -- We add the TyThing for the List constructor here. Otherwise, we
+    -- lookups in the TyThingMap will fail for "List" and not for "[]".
+    addListTyConName m =
+      case M.lookup "[]" m of
+        Nothing -> m
+        Just ps -> M.insertWith (++) "List" (filterListTyCon ps) m
+
+    -- The TyCon name in the TyThing for @"[]"@ must be @"[]"@ apparently.
+    --
+    -- listTyCon uses "List", and that made later checks fail for some tests,
+    -- so we cannot just return @[("GHC.Types", ATyCon listTyCon)]@
+    --
+    -- Returning the TyCon that GHC yields for @"[]"@ has later tests fail,
+    -- because that TyCon has no associated data constructors.
+    --
+    -- The solution we adopted for now is to return listTyCon, and use
+    -- the name from the TyThing that GHC returned.
+    filterListTyCon ps =
+      [ (mn, Ghc.ATyCon tc') | (mn, Ghc.ATyCon tc) <- ps
+          , "GHC.Types" == mn
+          , let tc' = Ghc.listTyCon { Ghc.tyConName = Ghc.tyConName tc }
+      ]
 
 tyThingSymbol :: Ghc.TyThing -> Maybe F.Symbol
 tyThingSymbol (Ghc.AnId     x) = Just (F.symbol x)

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs

@@ -49,6 +49,7 @@ module Language.Haskell.Liquid.Constraint.Env (
 import Prelude hiding (error)
 -- import Outputable
 -- import FastString (fsLit)
+import Control.Monad (foldM, msum)
 import Control.Monad.State
 
 -- import           GHC.Err.Located hiding (error)

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -27,6 +27,7 @@ import qualified Language.Haskell.Liquid.GHC.Resugar           as Rs
 import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
 import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
 import Text.PrettyPrint.HughesPJ ( text )
+import           Control.Monad ( foldM, forM, forM_, when, void )
 import           Control.Monad.State
 import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe)
 import           Data.Either.Extra                             (eitherToMaybe)

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs

@@ -15,6 +15,7 @@ module Language.Haskell.Liquid.Constraint.Init (
     ) where
 
 import           Prelude                                       hiding (error, undefined)
+import           Control.Monad (foldM, forM)
 import           Control.Monad.State
 import           Data.Maybe                                    (isNothing, fromMaybe, catMaybes, mapMaybe)
 import qualified Data.HashMap.Strict                           as M

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs

@@ -13,7 +13,7 @@
 
 module Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop) where
 
-import           Control.Monad.State
+import           Control.Monad (foldM, forM_)
 import           Data.Bifunctor                                 ( Bifunctor(bimap) )
 import qualified Data.HashMap.Strict                            as M
 import qualified Data.List                                      as L

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs

@@ -19,8 +19,8 @@ import qualified Data.List                          as L
 import qualified Data.HashSet                       as S
 import qualified Data.Traversable                   as T
 import qualified Data.HashMap.Strict                as M
-import           Control.Applicative (liftA2)
-import           Control.Monad.State ( gets, forM, foldM )
+import           Control.Monad ( foldM, forM )
+import           Control.Monad.State ( gets )
 import           Text.PrettyPrint.HughesPJ ( (<+>), text )
 import qualified Language.Haskell.Liquid.GHC.Misc                    as GM
 import qualified Language.Fixpoint.Types            as F