diff --git a/liquidhaskell-boot.cabal b/liquidhaskell-boot.cabal --- a/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot -version: 0.9.4.7.0 +version: 0.9.6.3 synopsis: Liquid Types for Haskell description: This package provides a plugin to verify Haskell programs. But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell) @@ -13,7 +13,7 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Simple -tested-with: GHC == 9.4.7 +tested-with: GHC == 9.6.3 data-files: include/CoreToLogic.lg syntax/liquid.css @@ -126,7 +126,7 @@ , aeson , binary , bytestring >= 0.10 - , Cabal < 3.9 + , Cabal < 3.11 , cereal , cmdargs >= 0.10 , containers >= 0.5 @@ -136,16 +136,16 @@ , 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.4.7 + , liquid-fixpoint == 0.9.6.3 , mtl >= 2.1 - , optparse-applicative < 0.18 + , optparse-applicative < 0.19 , githash , megaparsec >= 8 , pretty >= 1.1 diff --git a/src-ghc/Liquid/GHC/API.hs b/src-ghc/Liquid/GHC/API.hs --- a/src-ghc/Liquid/GHC/API.hs +++ b/src-ghc/Liquid/GHC/API.hs @@ -10,6 +10,7 @@ -} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE PatternSynonyms #-} module Liquid.GHC.API ( @@ -19,8 +20,7 @@ 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 @@ , isDictonaryId , isExternalName , isFamilyTyCon - , isFunTyCon , isGoodSrcSpan , isLocalId , isNewTyCon @@ -216,7 +215,8 @@ , typeSymbolKind ) import GHC.Builtin.Types.Prim as Ghc - ( eqPrimTyCon + ( isArrowTyCon + , eqPrimTyCon , eqReprPrimTyCon , primTyCons ) @@ -322,8 +322,8 @@ ( 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 @@ -331,10 +331,13 @@ , CoVarCo , ForAllCo , FunCo + , HoleCo , InstCo , KindCo , LRCo - , NthCo + , Refl + , GRefl + , SelCo , SubCo , SymCo , TransCo @@ -355,12 +358,12 @@ , 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.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 @@ , 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.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.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.Error as Ghc ( Messages(getMessages) , MessageClass(MCDiagnostic) + , Diagnostic(defaultDiagnosticOpts) , DiagnosticReason(WarningWithoutFlag) , MsgEnvelope(errMsgSpan) , errorsOrFatalWarningsFound @@ -653,6 +658,7 @@ ( MonadUnique, getUniqueM ) import GHC.Types.Var as Ghc ( VarBndr(Bndr) + , binderVar , mkLocalVar , mkTyVar , setVarName diff --git a/src-ghc/Liquid/GHC/API/Extra.hs b/src-ghc/Liquid/GHC/API/Extra.hs --- a/src-ghc/Liquid/GHC/API/Extra.hs +++ b/src-ghc/Liquid/GHC/API/Extra.hs @@ -82,7 +82,7 @@ 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 @@ 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 @@ 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/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -21,6 +21,7 @@ ) 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/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs --- a/src/Language/Haskell/Liquid/Bare/Misc.hs +++ b/src/Language/Haskell/Liquid/Bare/Misc.hs @@ -17,6 +17,7 @@ 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 @@ 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/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs --- a/src/Language/Haskell/Liquid/Bare/Plugged.hs +++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs @@ -140,7 +140,7 @@ 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 diff --git a/src/Language/Haskell/Liquid/Bare/Resolve.hs b/src/Language/Haskell/Liquid/Bare/Resolve.hs --- a/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -183,11 +183,35 @@ 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) diff --git a/src/Language/Haskell/Liquid/Constraint/Env.hs b/src/Language/Haskell/Liquid/Constraint/Env.hs --- a/src/Language/Haskell/Liquid/Constraint/Env.hs +++ b/src/Language/Haskell/Liquid/Constraint/Env.hs @@ -49,6 +49,7 @@ import Prelude hiding (error) -- import Outputable -- import FastString (fsLit) +import Control.Monad (foldM, msum) import Control.Monad.State -- import GHC.Err.Located hiding (error) diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -27,6 +27,7 @@ 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) diff --git a/src/Language/Haskell/Liquid/Constraint/Init.hs b/src/Language/Haskell/Liquid/Constraint/Init.hs --- a/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -15,6 +15,7 @@ ) 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 diff --git a/src/Language/Haskell/Liquid/Constraint/Relational.hs b/src/Language/Haskell/Liquid/Constraint/Relational.hs --- a/src/Language/Haskell/Liquid/Constraint/Relational.hs +++ b/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 diff --git a/src/Language/Haskell/Liquid/Constraint/Termination.hs b/src/Language/Haskell/Liquid/Constraint/Termination.hs --- a/src/Language/Haskell/Liquid/Constraint/Termination.hs +++ b/src/Language/Haskell/Liquid/Constraint/Termination.hs @@ -19,8 +19,8 @@ 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 diff --git a/src/Language/Haskell/Liquid/GHC/Logging.hs b/src/Language/Haskell/Liquid/GHC/Logging.hs --- a/src/Language/Haskell/Liquid/GHC/Logging.hs +++ b/src/Language/Haskell/Liquid/GHC/Logging.hs @@ -34,14 +34,14 @@ -> 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)) diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs --- a/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TupleSections #-} @@ -25,12 +26,8 @@ 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) @@ -89,7 +86,7 @@ -- 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 @@ -195,7 +192,7 @@ showSDoc :: Ghc.SDoc -> String showSDoc = Ghc.showSDocQualified -myQualify :: Ghc.PrintUnqualified +myQualify :: Ghc.NamePprCtx myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames } -- { Ghc.queryQualifyName = \_ _ -> Ghc.NameNotInScope1 } @@ -403,7 +400,7 @@ -- 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' @@ -458,7 +455,7 @@ -- 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 @@ -879,7 +876,8 @@ 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 diff --git a/src/Language/Haskell/Liquid/GHC/Plugin.hs b/src/Language/Haskell/Liquid/GHC/Plugin.hs --- a/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -190,7 +190,7 @@ unoptimise df = updOptLevel 0 df { debugLevel = 1 , ghcLink = LinkInMemory - , backend = Interpreter + , backend = interpreterBackend , ghcMode = CompManager } diff --git a/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs b/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs --- a/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +++ b/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs @@ -92,7 +92,7 @@ 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 diff --git a/src/Language/Haskell/Liquid/GHC/TypeRep.hs b/src/Language/Haskell/Liquid/GHC/TypeRep.hs --- a/src/Language/Haskell/Liquid/GHC/TypeRep.hs +++ b/src/Language/Haskell/Liquid/GHC/TypeRep.hs @@ -115,8 +115,8 @@ = TyConAppCo (subst x tx r) c (subst x tx <$> cs) substCoercion x tx (AppCo c1 c2) = AppCo (subst x tx c1) (subst x tx c2) -substCoercion x tx (FunCo r cN c1 c2) - = FunCo r cN (subst x tx c1) (subst x tx c2) -- TODO(adinapoli) Is this the correct substitution? +substCoercion x tx (FunCo r afl afr cN c1 c2) + = FunCo r afl afr cN (subst x tx c1) (subst x tx c2) -- TODO(adinapoli) Is this the correct substitution? substCoercion x tx (ForAllCo y c1 c2) | symbol x == symbol y = ForAllCo y c1 c2 @@ -134,8 +134,8 @@ = TransCo (subst x tx c1) (subst x tx c2) substCoercion x tx (AxiomRuleCo ca cs) = AxiomRuleCo (subst x tx ca) (subst x tx <$> cs) -substCoercion x tx (NthCo r i c) - = NthCo r i (subst x tx c) +substCoercion x tx (SelCo i c) + = SelCo i (subst x tx c) substCoercion x tx (LRCo i c) = LRCo i (subst x tx c) substCoercion x tx (InstCo c1 c2) @@ -144,6 +144,12 @@ = KindCo (subst x tx c) substCoercion x tx (SubCo c) = SubCo (subst x tx c) +substCoercion _x _tx (Refl t) + = Refl t +substCoercion _x _tx (GRefl r t c) + = GRefl r t c +substCoercion _x _tx (HoleCo c) + = HoleCo c instance SubstTy Role where instance SubstTy (CoAxiom Branched) where diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs --- a/src/Language/Haskell/Liquid/Transforms/ANF.hs +++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs @@ -19,6 +19,7 @@ , DsM , panic) import qualified Liquid.GHC.API as Ghc +import Control.Monad (forM) import Control.Monad.State.Lazy import System.Console.CmdArgs.Verbosity (whenLoud) import qualified Language.Fixpoint.Types as F @@ -366,7 +367,7 @@ u <- getUniqueM let i = getKey u let sp = Sp.srcSpan (aeSrcSpan γ) - return (mkUserLocal (anfOcc i) u Ghc.Many t sp) + return (mkUserLocal (anfOcc i) u Ghc.ManyTy t sp) anfOcc :: Int -> OccName anfOcc = mkVarOccFS . GM.symbolFastString . F.intSymbol F.anfPrefix diff --git a/src/Language/Haskell/Liquid/Transforms/Rec.hs b/src/Language/Haskell/Liquid/Transforms/Rec.hs --- a/src/Language/Haskell/Liquid/Transforms/Rec.hs +++ b/src/Language/Haskell/Liquid/Transforms/Rec.hs @@ -208,7 +208,7 @@ let x' = setVarType var t return (ids'', x') where - mkType ids ty = foldl (\t x -> FunTy VisArg Many (varType x) t) ty ids -- FIXME(adinapoli): Is 'VisArg' OK here? + mkType ids ty = foldl (\t x -> FunTy FTF_T_T ManyTy (varType x) t) ty ids -- FIXME(adinapoli): Is 'VisArg' OK here? -- NOTE [Don't choose transform-rec binders as decreasing params] -- -------------------------------------------------------------- diff --git a/src/Language/Haskell/Liquid/Transforms/Rewrite.hs b/src/Language/Haskell/Liquid/Transforms/Rewrite.hs --- a/src/Language/Haskell/Liquid/Transforms/Rewrite.hs +++ b/src/Language/Haskell/Liquid/Transforms/Rewrite.hs @@ -27,6 +27,7 @@ import Liquid.GHC.API as Ghc hiding (showPpr, substExpr) import Language.Haskell.Liquid.GHC.TypeRep () import Data.Maybe (fromMaybe) +import Control.Monad (msum) import Control.Monad.State hiding (lift) import Language.Fixpoint.Misc ({- mapFst, -} mapSnd) import qualified Language.Fixpoint.Types as F diff --git a/src/Language/Haskell/Liquid/Types/Bounds.hs b/src/Language/Haskell/Liquid/Types/Bounds.hs --- a/src/Language/Haskell/Liquid/Types/Bounds.hs +++ b/src/Language/Haskell/Liquid/Types/Bounds.hs @@ -70,9 +70,12 @@ ppBsyms _ [] = "" ppBsyms k' xs = "\\" <+> pprintTidy k' xs <+> "->" +instance Functor (Bound a) where + fmap f (Bound s vs ps xs e) = Bound s vs ps xs (f e) + instance Bifunctor Bound where first f (Bound s vs ps xs e) = Bound s (f <$> vs) (Misc.mapSnd f <$> ps) (Misc.mapSnd f <$> xs) e - second f (Bound s vs ps xs e) = Bound s vs ps xs (f e) + second = fmap makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r) => RRBound RSort -> [RRType r] -> [F.Symbol] -> RRType r -> RRType r diff --git a/src/Language/Haskell/Liquid/Types/Equality.hs b/src/Language/Haskell/Liquid/Types/Equality.hs --- a/src/Language/Haskell/Liquid/Types/Equality.hs +++ b/src/Language/Haskell/Liquid/Types/Equality.hs @@ -8,6 +8,7 @@ import Language.Haskell.Liquid.Types import qualified Liquid.GHC.API as Ghc +import Control.Monad (liftM2, zipWithM) import Control.Monad.Writer.Lazy -- import Control.Monad import qualified Data.List as L diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs --- a/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/src/Language/Haskell/Liquid/Types/Errors.hs @@ -5,6 +5,8 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1. {-# OPTIONS_GHC -Wno-orphans #-} -- PPrint and aeson instances. @@ -1084,6 +1086,7 @@ sourceErrors s = concatMap errMsgErrors . bagToList . getMessages . srcErrorMessages where + errMsgErrors :: forall e t. Diagnostic e => MsgEnvelope e -> [TError t] errMsgErrors e = [ ErrGhc (errMsgSpan e) msg ] where - msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope e)) + msg = text s $+$ nest 4 (text $ showSDocQualified (pprLocMsgEnvelope (defaultDiagnosticOpts @e) e)) diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -1479,10 +1479,10 @@ toType useRFInfo (RFun _ RFInfo{permitTC = permitTC} t@(RApp c _ _ _) t' _) | useRFInfo && isErasable c = toType useRFInfo t' | otherwise - = FunTy VisArg Many (toType useRFInfo t) (toType useRFInfo t') + = FunTy FTF_T_T ManyTy (toType useRFInfo t) (toType useRFInfo t') where isErasable = if permitTC == Just True then isEmbeddedDict else isClass toType useRFInfo (RFun _ _ t t' _) - = FunTy VisArg Many (toType useRFInfo t) (toType useRFInfo t') + = FunTy FTF_T_T ManyTy (toType useRFInfo t) (toType useRFInfo t') toType useRFInfo (RAllT a t _) | RTV α <- ty_var_value a = ForAllTy (Bndr α Required) (toType useRFInfo t) toType useRFInfo (RAllP _ t) diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs --- a/src/Language/Haskell/Liquid/Types/Types.hs +++ b/src/Language/Haskell/Liquid/Types/Types.hs @@ -890,8 +890,8 @@ -- directly to any type and has semantics _independent of_ the data-type. data Ref τ t = RProp - { rf_args :: [(Symbol, τ)] - , rf_body :: t -- ^ Abstract refinement associated with `RTyCon` + { rf_args :: [(Symbol, τ)] -- ^ arguments. e.g. @h@ in the above example + , rf_body :: t -- ^ Abstract refinement associated with `RTyCon`. e.g. @v > h@ in the above example } deriving (Eq, Generic, Data, Typeable, Functor) deriving Hashable via Generically (Ref τ t) @@ -996,7 +996,7 @@ ------------------------------------------------------------------------------- instance TyConable RTyCon where - isFun = isFunTyCon . rtc_tc + isFun = isArrowTyCon . rtc_tc isList = (listTyCon ==) . rtc_tc isTuple = Ghc.isTupleTyCon . rtc_tc isClass = isClass . rtc_tc -- isClassRTyCon @@ -1012,7 +1012,7 @@ instance TyConable TyCon where - isFun = isFunTyCon + isFun = isArrowTyCon isList = (listTyCon ==) isTuple = Ghc.isTupleTyCon isClass c = isClassTyCon c || isEqual c -- c == eqPrimTyCon diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -27,8 +27,7 @@ -- * Canonicalize Paths in Config , canonicalizePaths - -- * Exit Function - , exitWithResult + -- * Collecting errors , addErrors -- * Reporting the output of the checking @@ -763,10 +762,6 @@ printHeader :: Moods -> Doc -> IO () printHeader mood d = colorPhaseLn mood "" (render d) ------------------------------------------------------------------------- -exitWithResult :: Config -> [FilePath] -> Output Doc -> IO () ------------------------------------------------------------------------- -exitWithResult cfg targets out = void $ reportResult writeResultStdout cfg targets out reportResultJson :: ACSS.AnnMap -> IO () reportResultJson annm = do diff --git a/src/Language/Haskell/Liquid/UX/DiffCheck.hs b/src/Language/Haskell/Liquid/UX/DiffCheck.hs --- a/src/Language/Haskell/Liquid/UX/DiffCheck.hs +++ b/src/Language/Haskell/Liquid/UX/DiffCheck.hs @@ -54,12 +54,8 @@ import Language.Fixpoint.Solver.Stats () import Language.Haskell.Liquid.Misc (mkGraph) import Language.Haskell.Liquid.GHC.Misc -import Liquid.GHC.API as Ghc hiding ( Located - , sourceName - , text - , panic - , showPpr - ) +import Liquid.GHC.API as Ghc hiding + (Located, line, sourceName, text, panic, showPpr) import Text.PrettyPrint.HughesPJ (text, render, Doc) import qualified Data.ByteString as B import qualified Data.ByteString.Lazy as LB diff --git a/src/Language/Haskell/Liquid/WiredIn.hs b/src/Language/Haskell/Liquid/WiredIn.hs --- a/src/Language/Haskell/Liquid/WiredIn.hs +++ b/src/Language/Haskell/Liquid/WiredIn.hs @@ -30,7 +30,7 @@ -- import Language.Fixpoint.Misc (mapSnd) import Language.Haskell.Liquid.GHC.Misc import qualified Liquid.GHC.API as Ghc -import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ArgFlag(..)) +import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ForAllTyFlag(Required)) import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Types.RefType import Language.Haskell.Liquid.Types.Variance