liquidhaskell-boot 0.9.4.7.0 → 0.9.6.3
raw patch · 28 files changed
+111/−72 lines, 28 filesdep ~Cabaldep ~ghcdep ~liquid-fixpoint
Dependency ranges changed: Cabal, ghc, liquid-fixpoint, optparse-applicative
Files
- liquidhaskell-boot.cabal +6/−6
- src-ghc/Liquid/GHC/API.hs +21/−15
- src-ghc/Liquid/GHC/API/Extra.hs +3/−3
- src/Language/Haskell/Liquid/Bare/DataType.hs +1/−0
- src/Language/Haskell/Liquid/Bare/Misc.hs +2/−1
- src/Language/Haskell/Liquid/Bare/Plugged.hs +1/−1
- src/Language/Haskell/Liquid/Bare/Resolve.hs +24/−0
- src/Language/Haskell/Liquid/Constraint/Env.hs +1/−0
- src/Language/Haskell/Liquid/Constraint/Generate.hs +1/−0
- src/Language/Haskell/Liquid/Constraint/Init.hs +1/−0
- src/Language/Haskell/Liquid/Constraint/Relational.hs +1/−1
- src/Language/Haskell/Liquid/Constraint/Termination.hs +2/−2
- src/Language/Haskell/Liquid/GHC/Logging.hs +3/−3
- src/Language/Haskell/Liquid/GHC/Misc.hs +9/−11
- src/Language/Haskell/Liquid/GHC/Plugin.hs +1/−1
- src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +1/−1
- src/Language/Haskell/Liquid/GHC/TypeRep.hs +10/−4
- src/Language/Haskell/Liquid/Transforms/ANF.hs +2/−1
- src/Language/Haskell/Liquid/Transforms/Rec.hs +1/−1
- src/Language/Haskell/Liquid/Transforms/Rewrite.hs +1/−0
- src/Language/Haskell/Liquid/Types/Bounds.hs +4/−1
- src/Language/Haskell/Liquid/Types/Equality.hs +1/−0
- src/Language/Haskell/Liquid/Types/Errors.hs +4/−1
- src/Language/Haskell/Liquid/Types/RefType.hs +2/−2
- src/Language/Haskell/Liquid/Types/Types.hs +4/−4
- src/Language/Haskell/Liquid/UX/CmdLine.hs +1/−6
- src/Language/Haskell/Liquid/UX/DiffCheck.hs +2/−6
- src/Language/Haskell/Liquid/WiredIn.hs +1/−1
liquidhaskell-boot.cabal view
@@ -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
src-ghc/Liquid/GHC/API.hs view
@@ -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
src-ghc/Liquid/GHC/API/Extra.hs view
@@ -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 }
src/Language/Haskell/Liquid/Bare/DataType.hs view
@@ -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
src/Language/Haskell/Liquid/Bare/Misc.hs view
@@ -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
src/Language/Haskell/Liquid/Bare/Plugged.hs view
@@ -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
src/Language/Haskell/Liquid/Bare/Resolve.hs view
@@ -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)
src/Language/Haskell/Liquid/Constraint/Env.hs view
@@ -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)
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -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)
src/Language/Haskell/Liquid/Constraint/Init.hs view
@@ -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
src/Language/Haskell/Liquid/Constraint/Relational.hs view
@@ -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
src/Language/Haskell/Liquid/Constraint/Termination.hs view
@@ -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
src/Language/Haskell/Liquid/GHC/Logging.hs view
@@ -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))
src/Language/Haskell/Liquid/GHC/Misc.hs view
@@ -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
src/Language/Haskell/Liquid/GHC/Plugin.hs view
@@ -190,7 +190,7 @@ unoptimise df = updOptLevel 0 df { debugLevel = 1 , ghcLink = LinkInMemory- , backend = Interpreter+ , backend = interpreterBackend , ghcMode = CompManager }
src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs view
@@ -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
src/Language/Haskell/Liquid/GHC/TypeRep.hs view
@@ -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
src/Language/Haskell/Liquid/Transforms/ANF.hs view
@@ -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
src/Language/Haskell/Liquid/Transforms/Rec.hs view
@@ -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] -- --------------------------------------------------------------
src/Language/Haskell/Liquid/Transforms/Rewrite.hs view
@@ -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
src/Language/Haskell/Liquid/Types/Bounds.hs view
@@ -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
src/Language/Haskell/Liquid/Types/Equality.hs view
@@ -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
src/Language/Haskell/Liquid/Types/Errors.hs view
@@ -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))
src/Language/Haskell/Liquid/Types/RefType.hs view
@@ -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)
src/Language/Haskell/Liquid/Types/Types.hs view
@@ -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
src/Language/Haskell/Liquid/UX/CmdLine.hs view
@@ -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
src/Language/Haskell/Liquid/UX/DiffCheck.hs view
@@ -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
src/Language/Haskell/Liquid/WiredIn.hs view
@@ -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