Upgrade Liquid Haskell to run with ghc 9.12

.circleci/config.yml

@@ -141,23 +141,23 @@ commands:
 jobs:
 
   # Not used in workflows below at the moment, because stack doesn't
-  # support GHC 9.10 yet.
+  # support GHC 9.12 yet.
   stack_900:
     machine:
       image: default
     steps:
         - stack_build_and_test:
             stack_yaml_file: "stack.yaml"
             extra_build_flags: "--flag liquidhaskell-boot:devel"
-  cabal_9101:
+  cabal_9121:
     machine:
       image: default
     steps:
       - cabal_build_and_test:
-          ghc_version: "9.10.1"
+          ghc_version: "9.12.1"
 
 workflows:
   version: 2
   build_stack_and_cabal:
     jobs:
-      - cabal_9101
+      - cabal_9121

cabal.project

@@ -1,4 +1,4 @@
-with-compiler: ghc-9.10.1
+with-compiler: ghc-9.12.1
 
 packages: .
           ./liquid-fixpoint
@@ -19,13 +19,18 @@ source-repository-package
 
 allow-newer:
   ghc-timings:base
-  ,blaze-svg:base
-  ,blaze-svg:mtl
-  ,colonnade:text
-  ,rest-rewrite:containers
-  ,Chart:lens
-  ,Chart-diagrams:lens
-  ,SVGFonts:containers
+
+  ,active:base
+  ,Chart-diagrams:time
+  ,diagrams-core:base
+  ,diagrams-lib:base
+  ,diagrams-postscript:base
+  ,diagrams-svg:base
+  ,dual-tree:base
+  ,fsnotify:text
+  ,monoid-extras:base
+  ,statestack:base
+  ,svg-builder:base
 
 package liquid-fixpoint
   flags: +devel

liquidhaskell-boot/liquidhaskell-boot.cabal

@@ -136,7 +136,7 @@ library
                     , filepath             >= 1.3
                     , fingertree           >= 0.1
                     , exceptions           < 0.11
-                    , ghc                  ^>= 9.10
+                    , ghc                  ^>= 9.12
                     , ghc-boot
                     , ghc-prim
                     , gitrev

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -36,12 +36,14 @@ import           GHC                  as Ghc
     , GhcMonad
     , GhcPs
     , GhcRn
+    , HsBndrKind(HsBndrNoKind)
+    , HsBndrVar(HsBndrVar)
     , HsDecl(SigD)
     , HsExpr(ExprWithTySig, HsOverLit, HsVar)
     , HsModule(hsmodDecls)
     , HsOuterTyVarBndrs(HsOuterImplicit)
     , HsSigType(HsSig)
-    , HsTyVarBndr(UserTyVar)
+    , HsTyVarBndr(HsTvb)
     , HsType(HsAppTy, HsForAllTy, HsQualTy, HsTyVar, HsWildCardTy)
     , HsArg(HsValArg)
     , HsWildCardBndrs(HsWC)
@@ -55,7 +57,7 @@ import           GHC                  as Ghc
     , LexicalFixity(Prefix)
     , Located
     , LocatedN
-    , ModIface_(mi_anns, mi_exports, mi_globals, mi_module)
+    , ModIface_(mi_anns, mi_exports, mi_module)
     , ModLocation(ml_hs_file)
     , ModSummary(ms_hspp_file, ms_hspp_opts, ms_location, ms_mod)
     , Module
@@ -118,7 +120,6 @@ import           GHC                  as Ghc
     , mkModuleName
     , mkSrcLoc
     , mkSrcSpan
-    , modInfoTopLevelScope
     , moduleName
     , moduleNameString
     , moduleUnit
@@ -272,7 +273,9 @@ import GHC.Core.Coercion              as Ghc
     , mkRepReflCo
     )
 import GHC.Core.Coercion.Axiom        as Ghc
-    ( coAxiomTyCon )
+    ( coAxiomTyCon
+    , isNewtypeAxiomRule_maybe
+    )
 import GHC.Core.ConLike               as Ghc
     ( ConLike(RealDataCon) )
 import GHC.Core.DataCon               as Ghc
@@ -319,14 +322,24 @@ import GHC.Core.Make                  as Ghc
     , mkCoreLets
     , pAT_ERROR_ID
     )
-import GHC.Core.Predicate             as Ghc (getClassPredTys_maybe, getClassPredTys, isEvVarType, isEqPrimPred, isEqPred, isClassPred, isDictId, mkClassPred)
+import GHC.Core.Predicate             as Ghc
+    ( getClassPredTys_maybe
+    , getClassPredTys
+    , isEvVarType
+    , isEqPred
+    , isClassPred
+    , isDictId
+    , isNomEqPred
+    , mkClassPred
+    )
 import GHC.Core.Reduction             as Ghc
     ( Reduction(Reduction) )
 import GHC.Core.Subst                 as Ghc (emptySubst, extendCvSubst)
 import GHC.Core.TyCo.Rep              as Ghc
-    ( FunTyFlag(FTF_T_T, FTF_C_T)
+    ( Coercion
+    , FunTyFlag(FTF_T_T, FTF_C_T)
     , ForAllTyFlag(Required)
-    , Coercion (AxiomInstCo, SymCo)
+    , Coercion (AxiomCo, SymCo)
     , TyLit(CharTyLit, NumTyLit, StrTyLit)
     , Type
         ( AppTy
@@ -452,7 +465,7 @@ import GHC.Plugins                    as Ghc ( Serialized(Serialized)
 import GHC.Core.FVs                   as Ghc
     ( exprFreeVars
     , exprFreeVarsList
-    , exprsOrphNames
+    , orphNamesOfExprs
     , exprSomeFreeVarsList
     )
 import GHC.Core.Opt.OccurAnal         as Ghc
@@ -478,7 +491,11 @@ import GHC.Hs                         as Ghc
 import GHC.HsToCore.Expr              as Ghc
     ( dsLExpr )
 import GHC.Iface.Binary               as Ghc
-    ( TraceBinIFace(QuietBinIFace), getWithUserData, putWithUserData )
+    ( CompressionIFace(SafeExtraCompression)
+    , TraceBinIFace(QuietBinIFace)
+    , getWithUserData
+    , putWithUserData
+    )
 import GHC.Iface.Errors.Ppr            as Ghc
     ( missingInterfaceErrorDiagnostic )
 import GHC.Iface.Load                 as Ghc

liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs

@@ -32,6 +32,7 @@ import Data.Data (Data, gmapQr, gmapT)
 import Data.Generics (extQ, extT)
 import Data.Foldable                  (asum)
 import Data.List                      (sortOn)
+import qualified Data.Map as Map
 import GHC.Builtin.Names ( dollarIdKey, minusName )
 import GHC.Core                       as Ghc
 import GHC.Core.Coercion              as Ghc
@@ -81,7 +82,7 @@ dataConSig dc
 
 -- | Extracts the direct imports of a module.
 directImports :: TcGblEnv -> [Module]
-directImports = moduleEnvKeys . imp_mods . tcg_imports
+directImports = Map.keys . imp_mods . tcg_imports
 
 -- | Abstraction of 'EpaComment'.
 data ApiComment
@@ -107,7 +108,7 @@ apiCommentsParsedSource ps =
 
     -- TODO: take into account anchor_op, which only matters if the source was
     -- pre-processed by an exact-print-aware tool.
-    toRealSrc (L a e) = L (RealSrcSpan (anchor a) strictNothing) e
+    toRealSrc (L a e) = L (RealSrcSpan (epaLocationRealSrcSpan a) strictNothing) e
 
     spanToLineColumn =
       fmap (\s -> (srcSpanStartLine s, srcSpanStartCol s)) . srcSpanToRealSrcSpan

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

@@ -36,7 +36,6 @@ import           Control.Monad.Free
 import           Data.Char                      ( isUpper )
 import           GHC.Types.Name.Occurrence
 import qualified Liquid.GHC.API as Ghc
-                                                (noExtField)
 import qualified Data.Maybe                    as Mb
 
 -- TODO: make elaboration monadic so typeclass names are unified to something
@@ -271,7 +270,7 @@ buildHsExpr result = go
     go = \case
       RFun bind _ tin tout _
         | isClassType tin -> go tout
-        | otherwise       -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] (go tout)
+        | otherwise       -> mkHsLam (noLocA [nlVarPat (varSymbolToRdrName bind)]) (go tout)
       RAllE _ _ t -> go t
       RAllT _ t _ -> go t
       REx _ _ t -> go t
@@ -690,7 +689,15 @@ specTypeToLHsType = \case
       | otherwise       -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout)
     RAllT (ty_var_value -> (RTV tv)) t _ -> noLocA $ HsForAllTy
       Ghc.noExtField
-      (mkHsForAllInvisTele noAnn [noLocA $ UserTyVar noAnn SpecifiedSpec (noLocA $ symbolToRdrNameNs tvName (F.symbol tv))])
+      (mkHsForAllInvisTele noAnn
+        [ noLocA $
+            Ghc.HsTvb
+              noAnn
+              Ghc.SpecifiedSpec
+              (Ghc.HsBndrVar Ghc.noExtField (noLocA $ symbolToRdrNameNs tvName (F.symbol tv)))
+              (Ghc.HsBndrNoKind Ghc.noExtField)
+        ]
+      )
       (specTypeToLHsType t)
     RAllP _ ty -> specTypeToLHsType ty
     RApp RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp
@@ -705,6 +712,6 @@ specTypeToLHsType = \case
       impossible Nothing "RExprArg should not appear here"
     RAppTy t t' _ -> nlHsFunTy (specTypeToLHsType t) (specTypeToLHsType t')
     RRTy _ _ _ t -> specTypeToLHsType t
-    RHole _ -> noLocA $ HsWildCardTy Ghc.noExtField
+    RHole _ -> noLocA $ HsWildCardTy Ghc.noAnn
     RExprArg _ ->
       todo Nothing "Oops, specTypeToLHsType doesn't know how to handle RExprArg"

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

@@ -122,7 +122,7 @@ makeEnv cfg ghcTyLookupEnv tcg instEnv localVars src lmap specs = RE
     globalSyms  = concatMap getGlobalSyms specs
     syms        = [ (F.symbol v, v) | v <- vars ]
     vars        = srcVars src
-    usedExternals = Ghc.exprsOrphNames $ map snd $ Ghc.flattenBinds $ _giCbs src
+    usedExternals = Ghc.orphNamesOfExprs $ map snd $ Ghc.flattenBinds $ _giCbs src
 
 
 getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol]

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

@@ -698,11 +698,18 @@ unRRTy t              = t
 castTy  :: CGEnv -> Type -> CoreExpr -> Coercion -> CG SpecType
 castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
 --------------------------------------------------------------------------------
-castTy γ t e (AxiomInstCo ca _ _)
-  = fromMaybe <$> castTy' γ t e <*> lookupNewType (coAxiomTyCon ca)
-
-castTy γ t e (SymCo (AxiomInstCo ca _ _))
-  = do mtc <- lookupNewType (coAxiomTyCon ca)
+castTy γ t e (AxiomCo ca _)
+  = do
+    msp <- case isNewtypeAxiomRule_maybe ca of
+      Just (tc, _) -> lookupNewType tc
+      _ -> return Nothing
+    sp <- castTy' γ t e
+    return (fromMaybe sp msp)
+
+castTy γ t e (SymCo (AxiomCo ca _))
+  = do mtc <- case isNewtypeAxiomRule_maybe ca of
+         Just (tc, _) -> lookupNewType tc
+         _ -> return Nothing
        F.forM_ mtc (cconsE γ e)
        castTy' γ t e
 

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

@@ -186,21 +186,6 @@ availableTyThings tcGblEnv avails =
       mapM (lookupTyThing (Ghc.tcg_type_env tcGblEnv)) $
       concatMap availNames avails
 
-_dumpTypeEnv :: TypecheckedModule -> IO ()
-_dumpTypeEnv tm = do
-  print ("DUMP-TYPE-ENV" :: String)
-  print (showpp <$> tcmTyThings tm)
-
-tcmTyThings :: TypecheckedModule -> Maybe [Name]
-tcmTyThings
-  =
-  -- typeEnvElts
-  -- . tcg_type_env . fst
-  -- . md_types . snd
-  -- . tm_internals_
-  modInfoTopLevelScope
-  . tm_checked_module_info
-
 modSummaryHsFile :: ModSummary -> FilePath
 modSummaryHsFile modSummary =
   fromMaybe

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

@@ -751,7 +751,7 @@ isPredVar v = F.notracepp msg . isPredType . varType $ v
     msg     =  "isGoodCaseBind v = " ++ show v
 
 isPredType :: Type -> Bool
-isPredType = anyF [ isClassPred, isEqPred, isEqPrimPred ]
+isPredType = anyF [ isClassPred, isNomEqPred, isEqPred ]
 
 anyF :: [a -> Bool] -> a -> Bool
 anyF ps x = or [ p x | p <- ps ]
@@ -921,12 +921,18 @@ withWiredIn m = discardConstraints $ do
   --   ) wiredIns
 
   sigs wiredIns = concatMap (\w ->
-      let inf = maybeToList $ (\(fPrec, fDir) -> Ghc.L locSpanAnn $ Ghc.FixSig Ghc.noAnn $ Ghc.FixitySig Ghc.NoNamespaceSpecifier [Ghc.L locSpanAnn (tcWiredInName w)] $ Ghc.Fixity Ghc.NoSourceText fPrec fDir) <$> tcWiredInFixity w in
-      let t =
+      let inf = maybeToList $ do
+            (fPrec, fDir) <- tcWiredInFixity w
+            return $
+              Ghc.L locSpanAnn $
+              Ghc.FixSig Ghc.noAnn $
+              Ghc.FixitySig Ghc.NoNamespaceSpecifier [Ghc.L locSpanAnn (tcWiredInName w)] $
+              Ghc.Fixity fPrec fDir
+          t =
             let ext' = [] in
             [Ghc.L locSpanAnn $ TypeSig Ghc.noAnn [Ghc.L locSpanAnn (tcWiredInName w)] $ HsWC ext' $ Ghc.L locSpanAnn $ HsSig Ghc.noExtField (HsOuterImplicit ext') $ tcWiredInType w]
       in
-      inf <> t
+         inf <> t
     ) wiredIns
 
   locSpan = UnhelpfulSpan (UnhelpfulOther "Liquid.GHC.Misc: WiredIn")
@@ -969,7 +975,16 @@ withWiredIn m = discardConstraints $ do
     aName <- toLoc <$> toName "a"
     let aTy = nameToTy aName
     let ty = toLoc $ HsForAllTy Ghc.noExtField
-             (mkHsForAllInvisTele Ghc.noAnn [toLoc $ UserTyVar Ghc.noAnn SpecifiedSpec aName]) $ mkHsFunTy aTy (mkHsFunTy aTy boolTy')
+             (mkHsForAllInvisTele Ghc.noAnn
+               [ toLoc $
+                   Ghc.HsTvb
+                   Ghc.noAnn
+                   Ghc.SpecifiedSpec
+                   (Ghc.HsBndrVar Ghc.noExtField aName)
+                   (Ghc.HsBndrNoKind Ghc.noExtField)
+               ]
+             )
+             $ mkHsFunTy aTy (mkHsFunTy aTy boolTy')
     return $ TcWiredIn n (Just (4, Ghc.InfixN)) ty
 
   -- TODO: This is defined as a measure in liquidhaskell GHC.Base_LHAssumptions. We probably want to insert all measures to the environment.
@@ -979,7 +994,15 @@ withWiredIn m = discardConstraints $ do
     aName <- toLoc <$> toName "a"
     let aTy = nameToTy aName
     let ty = toLoc $ HsForAllTy Ghc.noExtField
-               (mkHsForAllInvisTele Ghc.noAnn [toLoc $ UserTyVar Ghc.noAnn SpecifiedSpec aName]) $ mkHsFunTy (listTy aTy) intTy'
+               (mkHsForAllInvisTele Ghc.noAnn
+                 [ toLoc $
+                     Ghc.HsTvb
+                     Ghc.noAnn
+                     Ghc.SpecifiedSpec
+                     (Ghc.HsBndrVar Ghc.noExtField aName)
+                     (Ghc.HsBndrNoKind Ghc.noExtField)
+                 ]
+               ) $ mkHsFunTy (listTy aTy) intTy'
     return $ TcWiredIn n Nothing ty
 
 prependGHCRealQual :: FastString -> RdrName

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs

@@ -95,7 +95,7 @@ encodeLiquidLib :: LiquidLib -> IO B.ByteString
 encodeLiquidLib lib0 = do
     let (lib1, ns) = collectLHNames lib0
     bh <- GHC.openBinMem (1024*1024)
-    GHC.putWithUserData GHC.QuietBinIFace bh ns
+    GHC.putWithUserData GHC.QuietBinIFace GHC.SafeExtraCompression bh ns
     GHC.withBinBuffer bh $ \bs ->
       return $ Builder.toLazyByteString $ B.execPut (B.put lib1) <> Builder.fromByteString bs
 

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

@@ -4,7 +4,6 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE RankNTypes                #-}
 {-# LANGUAGE UndecidableInstances      #-}
-{-# LANGUAGE StandaloneDeriving        #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -45,9 +44,6 @@ eqType' (TyConApp c1 ts1) (TyConApp c2 ts2)
 eqType' _ _ 
   = False 
 
-
-deriving instance (Eq tyvar, Eq argf) => Eq (VarBndr tyvar argf)
-
 showTy :: Type -> String 
 showTy (TyConApp c ts) = "(RApp   " ++ showPpr c ++ " " ++ sep' ", " (showTy <$> ts) ++ ")"
 showTy (AppTy t1 t2)   = "(TAppTy " ++ (showTy t1 ++ " " ++ showTy t2) ++ ")"