Skip to content

Commit

Permalink
Update Liquid Haskell to build with ghc-9.6.3
Browse files Browse the repository at this point in the history
  • Loading branch information
@facundominguez
facundominguez committed Dec 5, 2023
1 parent d2351b0 commit 97a2016
Show file tree
Hide file tree
Showing 29 changed files with 83 additions and 63 deletions.
2 changes: 1 addition & 1 deletion cabal.project
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
with-compiler: ghc-9.4.7
with-compiler: ghc-9.6.3

packages: .
./liquid-fixpoint
Expand Down
2 changes: 1 addition & 1 deletion liquid-fixpoint
Submodule liquid-fixpoint updated 12 files
+2 −1 .github/workflows/cabal.yml
+2 −0 liquid-fixpoint.cabal
+1 −0 src/Language/Fixpoint/Defunctionalize.hs
+1 −0 src/Language/Fixpoint/Parse.hs
+1 −0 src/Language/Fixpoint/Solver/Instantiate.hs
+1 −0 src/Language/Fixpoint/Solver/Interpreter.hs
+1 −0 src/Language/Fixpoint/Solver/Monad.hs
+1 −0 src/Language/Fixpoint/Solver/PLE.hs
+1 −1 src/Language/Fixpoint/Solver/Rewrite.hs
+0 −1 src/Language/Fixpoint/SortCheck.hs
+1 −1 stack.yaml
+10 −17 stack.yaml.lock
4 changes: 2 additions & 2 deletions liquidhaskell-boot/liquidhaskell-boot.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ library
, aeson
, binary
, bytestring >= 0.10
, Cabal < 3.9
, Cabal < 3.11
, cereal
, cmdargs >= 0.10
, containers >= 0.5
Expand All @@ -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
Expand Down
36 changes: 21 additions & 15 deletions liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ it easy to discover breaking changes in the GHC API.
-}

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}

module Liquid.GHC.API (
Expand All @@ -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)
Expand Down Expand Up @@ -102,7 +102,6 @@ import GHC as Ghc
, isDictonaryId
, isExternalName
, isFamilyTyCon
, isFunTyCon
, isGoodSrcSpan
, isLocalId
, isNewTyCon
Expand Down Expand Up @@ -216,7 +215,8 @@ import GHC.Builtin.Types as Ghc
, typeSymbolKind
)
import GHC.Builtin.Types.Prim as Ghc
( eqPrimTyCon
( isArrowTyCon
, eqPrimTyCon
, eqReprPrimTyCon
, primTyCons
)
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions liquidhaskell-boot/src-ghc/Liquid/GHC/API/Extra.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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 }

Expand Down
1 change: 1 addition & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Relational.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Logging.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,14 @@ putLogMsg :: GHC.Logger
-> PJ.Doc
-> IO ()
putLogMsg logger sev srcSpan _mbStyle =
GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag) srcSpan . GHC.text . PJ.render
GHC.putLogMsg logger (GHC.logFlags logger) (GHC.MCDiagnostic sev GHC.WarningWithoutFlag Nothing) srcSpan . GHC.text . PJ.render

putWarnMsg :: GHC.Logger -> GHC.SrcSpan -> PJ.Doc -> IO ()
putWarnMsg logger srcSpan doc =
putLogMsg logger GHC.SevWarning srcSpan (Just GHC.defaultErrStyle) doc

addTcRnUnknownMessage :: GHC.SrcSpan -> PJ.Doc -> GHC.TcRn ()
addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc
addTcRnUnknownMessage srcSpan = GHC.addErrAt srcSpan . GHC.mkTcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc

addTcRnUnknownMessages :: [(GHC.SrcSpan, PJ.Doc)] -> GHC.TcRn ()
addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.TcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
addTcRnUnknownMessages = GHC.addErrs . map (fmap (GHC.mkTcRnUnknownMessage . GHC.mkPlainError [] . fromPJDoc))
20 changes: 9 additions & 11 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
Expand All @@ -25,12 +26,8 @@ import qualified Data.List as L
import Debug.Trace

import Prelude hiding (error)
import Liquid.GHC.API as Ghc hiding ( L
, sourceName
, showPpr
, panic
, showSDoc
)
import Liquid.GHC.API as Ghc hiding
(L, line, sourceName, showPpr, panic, showSDoc)
import qualified Liquid.GHC.API as Ghc (GenLocated (L), showSDoc, panic)


Expand Down Expand Up @@ -89,7 +86,7 @@ stringTyVar s = mkTyVar name liftedTypeKind

-- FIXME: reusing uniques like this is really dangerous
stringVar :: String -> Type -> Var
stringVar s t = mkLocalVar VanillaId name Many t vanillaIdInfo
stringVar s t = mkLocalVar VanillaId name ManyTy t vanillaIdInfo
where
name = mkInternalName (mkUnique 'x' 25) occ noSrcSpan
occ = mkVarOcc s
Expand Down Expand Up @@ -195,7 +192,7 @@ showPpr = Ghc.showPprQualified
showSDoc :: Ghc.SDoc -> String
showSDoc = Ghc.showSDocQualified

myQualify :: Ghc.PrintUnqualified
myQualify :: Ghc.NamePprCtx
myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }
-- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 }

Expand Down Expand Up @@ -403,7 +400,7 @@ lookupRdrName hsc_env mod_name rdr_name = do
-- XXX [gre] -> return (Just (gre_name gre))
[] -> return Nothing
_ -> Ghc.panic "lookupRdrNameInModule"
Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (Ghc.mkPtrString "Could not determine the exports of the module"), ppr mod_name]
Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (Ghc.mkPtrString# "Could not determine the exports of the module"#), ppr mod_name]
err' -> throwCmdLineErrorS dflags $ cannotFindModule hsc_env mod_name err'
where dflags = hsc_dflags hsc_env
throwCmdLineErrorS dflags' = throwCmdLineError . Ghc.showSDoc dflags'
Expand Down Expand Up @@ -458,7 +455,7 @@ tyConTyVarsDef c
-- none = tracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c)

noTyVars :: TyCon -> Bool
noTyVars c = Ghc.isPrimTyCon c || isFunTyCon c || Ghc.isPromotedDataCon c
noTyVars c = Ghc.isPrimTyCon c || Ghc.isPromotedDataCon c

--------------------------------------------------------------------------------
-- | Symbol Instances
Expand Down Expand Up @@ -879,7 +876,8 @@ elabRnExpr rdr_expr = do

logger <- getLogger
diag_opts <- initDiagOpts <$> getDynFlags
liftIO $ printMessages logger diag_opts ds_msgs
print_config <- initDsMessageOpts <$> getDynFlags
liftIO $ printMessages logger print_config diag_opts ds_msgs

case me of
Nothing -> failM
Expand Down
2 changes: 1 addition & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ instance Unoptimise DynFlags where
unoptimise df = updOptLevel 0 df
{ debugLevel = 1
, ghcLink = LinkInMemory
, backend = Interpreter
, backend = interpreterBackend
, ghcMode = CompManager
}

Expand Down
2 changes: 1 addition & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do
eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
-- now look up the assumptions
liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod
FoundMultiple{} -> failWithTc $ TcRnUnknownMessage $ mkPlainError [] $
FoundMultiple{} -> failWithTc $ mkTcRnUnknownMessage $ mkPlainError [] $
cannotFindModule hscEnv assumptionsModName res
_ -> return Nothing

Expand Down
Loading

0 comments on commit 97a2016

Please sign in to comment.