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.10.1.2 +version: 0.9.12.2 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.10.1 +tested-with: GHC == 9.12.2 source-repository head type: git @@ -136,13 +136,13 @@ , filepath >= 1.3 , fingertree >= 0.1 , exceptions < 0.11 - , ghc ^>= 9.10 + , ghc ^>= 9.12 , ghc-boot , ghc-prim , gitrev , hashable >= 1.3 && < 1.6 , hscolour >= 1.22 - , liquid-fixpoint == 0.9.6.3.2 + , liquid-fixpoint == 0.9.6.3.3 , mtl >= 2.1 , optparse-applicative < 0.19 , githash 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 @@ -36,12 +36,14 @@ , 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 @@ , 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 @@ , mkModuleName , mkSrcLoc , mkSrcSpan - , modInfoTopLevelScope , moduleName , moduleNameString , moduleUnit @@ -198,6 +199,9 @@ , intTy , intTyCon , intTyConName + , integerISDataCon + , integerIPDataCon + , integerINDataCon , liftedTypeKind , liftedTypeKindTyConName , listTyCon @@ -274,7 +278,9 @@ , 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 @@ -321,14 +327,24 @@ , 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 @@ -454,7 +470,7 @@ import GHC.Core.FVs as Ghc ( exprFreeVars , exprFreeVarsList - , exprsOrphNames + , orphNamesOfExprs , exprSomeFreeVarsList ) import GHC.Core.Opt.OccurAnal as Ghc @@ -480,7 +496,11 @@ 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 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 @@ -32,6 +32,7 @@ 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 @@ -- | 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 @@ -- 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 diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs --- a/src/Language/Haskell/Liquid/Bare/Elaborate.hs +++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs @@ -4,6 +4,7 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -36,7 +37,6 @@ 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 +271,7 @@ 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 @@ -571,8 +571,8 @@ fixExprToHsExpr :: S.HashSet F.Symbol -> F.Expr -> LHsExpr GhcPs fixExprToHsExpr _ (F.ECon c) = constantToHsExpr c fixExprToHsExpr env (F.EVar x) - | x == "GHC.Types.[]" = GM.notracePpr "Empty" $ nlHsVar (mkVarUnqual (mkFastString "[]")) - | x == "GHC.Types.:" = GM.notracePpr "Cons" $ nlHsVar (mkVarUnqual (mkFastString ":")) + | x == F.symbol (show '[]) = GM.notracePpr "Empty" $ nlHsVar (mkVarUnqual (mkFastString "[]")) + | x == F.symbol (show '(:)) = GM.notracePpr "Cons" $ nlHsVar (mkVarUnqual (mkFastString ":")) | otherwise = GM.notracePpr "Var" $ nlHsVar (symbolToRdrName env x) fixExprToHsExpr env (F.EApp e0 e1) = mkHsApp (fixExprToHsExpr env e0) (fixExprToHsExpr env e1) @@ -690,7 +690,15 @@ | 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 +713,6 @@ 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" diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs --- a/src/Language/Haskell/Liquid/Bare/Measure.hs +++ b/src/Language/Haskell/Liquid/Bare/Measure.hs @@ -1,5 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE TupleSections #-} -- | This module contains (most of) the code needed to lift Haskell entitites, @@ -59,6 +61,8 @@ import Control.Monad (mapM) import qualified Data.List as L +import GHC.Base (Int(I#)) + -------------------------------------------------------------------------------- makeHaskellMeasures :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec -> [Measure (Located BareType) (Located LHName)] @@ -408,7 +412,7 @@ -- List of wired DCs that cannot be found in the measure environment as they are -- eliminated in the translation from core. -- Written as a list of symbols because that's easier than trying to get the corresponding DCs from GHC. - wired = S.fromList $ F.symbol <$> ["GHC.Types.True", "GHC.Types.False", "GHC.Types.I#"] + wired = S.fromList $ F.symbol <$> [show 'True, show 'False, show 'I#] notWired dc = not $ GM.qualifiedNameSymbol (Ghc.getName dc) `S.member` wired -- Undefined ones are those that are not already defined in the measure environement and are not wired dcsUndefinedInLogic = S.filter notWired $ allDCInUnfoldings `S.difference` definedDCs 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 @@ -106,7 +106,7 @@ } where globalSyms = concatMap getGlobalSyms specs - usedExternals = Ghc.exprsOrphNames $ map snd $ Ghc.flattenBinds $ _giCbs src + usedExternals = Ghc.orphNamesOfExprs $ map snd $ Ghc.flattenBinds $ _giCbs src getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol] getGlobalSyms (_, spec) 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 @@ -697,11 +697,18 @@ 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 (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 (AxiomInstCo ca _ _)) - = do mtc <- lookupNewType (coAxiomTyCon ca) +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 diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs --- a/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -144,21 +144,6 @@ , lookupName name ] -_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 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 @@ -751,7 +751,7 @@ 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 @@ -- ) 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 @@ 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 @@ 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 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 @@ -219,14 +219,11 @@ -------------------------------------------------------------------------------- -- | LiquidHaskell requires the desugarer to keep source note ticks --- and to export everything. --- --- TODO: We shouldn't rely on exports to find out what's in a ModGuts --- https://github.com/ucsd-progsys/liquidhaskell/pull/2388#issuecomment-2411418479 +-- and to keep unused functions. desugarerDynFlags :: DynFlags -> DynFlags desugarerDynFlags df = (foldl gopt_unset df disabledOpts) { debugLevel = 1 -- To keep source note ticks - , backend = interpreterBackend -- To export everything + , backend = interpreterBackend -- To keep unused functions during desugaring } where disabledOpts = diff --git a/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs b/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs --- a/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs +++ b/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs @@ -95,7 +95,7 @@ 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 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 @@ -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 #-} @@ -44,9 +43,6 @@ = c1 == c2 && and (zipWith eqType' ts1 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) ++ ")" diff --git a/src/Language/Haskell/Liquid/LHNameResolution.hs b/src/Language/Haskell/Liquid/LHNameResolution.hs --- a/src/Language/Haskell/Liquid/LHNameResolution.hs +++ b/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -77,6 +77,7 @@ import qualified Data.HashMap.Strict as HM import Data.List (find, isSuffixOf, nubBy) import Data.List.Extra (dropEnd) +import qualified Data.Map as Map import Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList) import qualified Data.Text as Text import qualified GHC.Types.Name.Occurrence @@ -567,7 +568,7 @@ coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName))]] moduleAliases m = - case GHC.lookupModuleEnv impAvails m of + case Map.lookup m impAvails of Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys Nothing | thisModule == m -> @@ -579,7 +580,7 @@ concat $ maybeToList $ do pString <- dropLHAssumptionsSuffix m pMod <- findDependency pString - GHC.lookupModuleEnv impAvails pMod + Map.lookup pMod impAvails dropLHAssumptionsSuffix m = let mString = GHC.moduleNameString (GHC.moduleName m) @@ -591,7 +592,7 @@ findDependency ms = find ((ms ==) . GHC.moduleNameString . GHC.moduleName) $ - GHC.moduleEnvKeys impAvails + Map.keys impAvails imvAliases imv | GHC.imv_qualified imv = [GHC.imv_name imv] diff --git a/src/Language/Haskell/Liquid/Parse.hs b/src/Language/Haskell/Liquid/Parse.hs --- a/src/Language/Haskell/Liquid/Parse.hs +++ b/src/Language/Haskell/Liquid/Parse.hs @@ -6,6 +6,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -Wno-orphans #-} module Language.Haskell.Liquid.Parse @@ -97,8 +98,8 @@ initPStateWithList :: LHPState initPStateWithList = (initPState composeFun) - { empList = Just $ \lx -> EVar ("GHC.Types.[]" <$ lx) - , singList = Just (\lx e -> EApp (EApp (EVar ("GHC.Types.:" <$ lx)) e) (EVar ("GHC.Types.[]" <$ lx))) + { empList = Just $ \lx -> EVar (symbol (show '[]) <$ lx) + , singList = Just (\lx e -> EApp (EApp (EVar (symbol (show '(:)) <$ lx)) e) (EVar (symbol (show '[]) <$ lx))) } where composeFun = Nothing @@ -911,7 +912,7 @@ | DSize ([LocBareTypeParsed], LocSymbol) -- ^ 'data size' annotations, generating fancy termination metric | BFix () -- ^ fixity annotation | Define (Located LHName, ([Symbol], ExprV LocSymbol)) -- ^ 'define' annotation for specifying logic aliases - deriving (Data, Typeable) + deriving (Data) instance PPrint BPspec where pprintTidy = ppPspec diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -1,8 +1,10 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-x-partial #-} @@ -58,6 +60,9 @@ import Control.Monad.Reader import Language.Haskell.Liquid.UX.Config +import Data.Ratio +import GHC.Base ((+#), (-#), (*#)) + logicType :: (Reftable r) => Bool -> Type -> RRType r logicType allowTC τ = fromRTypeRep $ t { ty_binds = bs, ty_info = is, ty_args = as, ty_refts = rs} where @@ -404,33 +409,33 @@ | Just rel <- M.lookup f brels = PAtom rel <$> coreToLg e1 <*> coreToLg e2 go (Just f, [e]) - | f == symbol ("GHC.Classes.not" :: String) + | f == symbol (show 'not) = PNot <$> coreToLg e go (Just f, [e1, e2]) - | f == symbol ("GHC.Classes.||" :: String) + | f == symbol (show '(||)) = POr <$> mapM coreToLg [e1, e2] - | f == symbol ("GHC.Classes.&&" :: String) + | f == symbol (show '(&&)) = PAnd <$> mapM coreToLg [e1, e2] | f == symbol ("Language.Haskell.Liquid.Prelude.==>" :: String) = PImp <$> coreToLg e1 <*> coreToLg e2 | f == symbol ("Language.Haskell.Liquid.Prelude.<=>" :: String) = PIff <$> coreToLg e1 <*> coreToLg e2 - | f == symbol ("GHC.Base.const" :: String) + | f == symbol (show 'const) = coreToLg e1 go (Just f, [es]) - | f == symbol ("GHC.Internal.Data.Foldable.or" :: String) + | f == symbol (show 'or) = POr . deList <$> coreToLg es - | f == symbol ("GHC.Internal.Data.Foldable.and" :: String) + | f == symbol (show 'and) = PAnd . deList <$> coreToLg es go (_, _) = toLogicApp p deList :: Expr -> [Expr] deList (EApp (EApp (EVar cons) e) es) - | cons == symbol ("GHC.Types.:" :: String) + | cons == symbol (show '(:)) = e:deList es deList (EVar nil) - | nil == symbol ("GHC.Types.[]" :: String) + | nil == symbol (show '[]) = [] deList e = [e] @@ -450,9 +455,9 @@ makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr makeApp _ _ f [e] - | val f == symbol ("GHC.Internal.Num.negate" :: String) + | val f == symbol (show 'negate) = ENeg e - | val f == symbol ("GHC.Internal.Num.fromInteger" :: String) + | val f == symbol (show 'fromInteger) , ECon c <- e = ECon c | (modName, sym) <- GM.splitModuleName (val f) @@ -478,12 +483,12 @@ eAppWithMap lmap (symbol x) [] (EVar $ symbol x) brels :: M.HashMap Symbol Brel -brels = M.fromList [ (symbol ("GHC.Classes.==" :: String), Eq) - , (symbol ("GHC.Classes./=" :: String), Ne) - , (symbol ("GHC.Classes.>=" :: String), Ge) - , (symbol ("GHC.Classes.>" :: String) , Gt) - , (symbol ("GHC.Classes.<=" :: String), Le) - , (symbol ("GHC.Classes.<" :: String) , Lt) +brels = M.fromList [ (symbol (show '(==)), Eq) + , (symbol (show '(/=)), Ne) + , (symbol (show '(>=)), Ge) + , (symbol (show '(>)) , Gt) + , (symbol (show '(<=)), Le) + , (symbol (show '(<)) , Lt) ] -- bops is a map between GHC function names/symbols and binary operators @@ -492,28 +497,21 @@ -- they can come from GHC.Prim, GHC.Internal.Num, GHC.Internal.Real or -- be an instance of Num for Int. bops :: M.HashMap Symbol Bop -bops = M.fromList [ (numSymbol "+", Plus) +bops = M.fromList [ (symbol (show '(+)), Plus) , (numIntSymbol "+", Plus) - , (primSymbol "+#", Plus) - , (numSymbol "-", Minus) + , (symbol (show '(+#)), Plus) + , (symbol (show '(-)), Minus) , (numIntSymbol "-", Minus) - , (primSymbol "-#", Minus) - , (numSymbol "*", Times) + , (symbol (show '(-#)), Minus) + , (symbol (show '(*)), Times) , (numIntSymbol "*", Times) - , (primSymbol "*#", Times) - , (numSymbol "/", Div) - , (realSymbol "/", Div) - , (numSymbol "%", Mod) + , (symbol (show '(*#)), Times) + , (symbol (show '(/)), Div) + , (symbol (show '(%)), Mod) ] where - primSymbol :: String -> Symbol - primSymbol = symbol . (++) "GHC.Prim." - numSymbol :: String -> Symbol - numSymbol = symbol . (++) "GHC.Internal.Num." numIntSymbol :: String -> Symbol - numIntSymbol = numSymbol . (++) "$fNumInt_$c" - realSymbol :: String -> Symbol - realSymbol = symbol . (++) "GHC.Internal.Real." + numIntSymbol = symbol . (++) "GHC.Internal.Num.$fNumInt_$c" splitArgs :: Bool -> C.Expr t -> (C.Expr t, [C.Arg t]) splitArgs allowTC exprt = (exprt', reverse args) @@ -573,13 +571,11 @@ ignoreVar i = simpleSymbolVar i `elem` ["I#", "D#"] -- | Tries to determine if a 'CoreAlt' maps to one of the 'Integer' type constructors. --- We need the disjuction for GHC >= 9, where the Integer now comes from the \"ghc-bignum\" package, --- and it has different names for the constructors. isBangInteger :: [C.CoreAlt] -> Bool isBangInteger [Alt (C.DataAlt s) _ _, Alt (C.DataAlt jp) _ _, Alt (C.DataAlt jn) _ _] - = (symbol s == "GHC.Integer.Type.S#" || symbol s == "GHC.Num.Integer.IS") - && (symbol jp == "GHC.Integer.Type.Jp#" || symbol jp == "GHC.Num.Integer.IP") - && (symbol jn == "GHC.Integer.Type.Jn#" || symbol jn == "GHC.Num.Integer.IN") + = s == Ghc.integerISDataCon + && jp == Ghc.integerIPDataCon + && jn == Ghc.integerINDataCon isBangInteger _ = False isErasable :: Id -> Bool 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 @@ -49,7 +49,7 @@ , bparams :: [(LocSymbol, t)] -- ^ These are abstract refinements, for now , bargs :: [(LocSymbol, t)] -- ^ These are value variables , bbody :: e -- ^ The body of the bound - } deriving (Data, Typeable, Generic, Functor, Foldable, Traversable) + } deriving (Data, Generic, Functor, Foldable, Traversable) deriving B.Binary via Generically (Bound t e) type RBound = RRBound RSort diff --git a/src/Language/Haskell/Liquid/Types/DataDecl.hs b/src/Language/Haskell/Liquid/Types/DataDecl.hs --- a/src/Language/Haskell/Liquid/Types/DataDecl.hs +++ b/src/Language/Haskell/Liquid/Types/DataDecl.hs @@ -37,7 +37,6 @@ import Prelude hiding (error) import Control.DeepSeq -import Data.Typeable (Typeable) import Data.Generics (Data) import qualified Data.Binary as B import Data.Hashable @@ -66,14 +65,14 @@ , tycSFun :: Maybe (SizeFunV v) -- ^ Default termination measure , tycPropTy :: Maybe ty -- ^ Type of Ind-Prop , tycKind :: !DataDeclKind -- ^ User-defined or Auto-lifted - } deriving (Data, Typeable, Generic, Functor, Foldable, Traversable) + } deriving (Data, Generic, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (DataDeclP v ty) -- | The name of the `TyCon` corresponding to a `DataDecl` data DataName = DnName !(F.Located LHName) -- ^ for 'isVanillyAlgTyCon' we can directly use the `TyCon` name | DnCon !(F.Located LHName) -- ^ for 'FamInst' TyCon we save some `DataCon` name - deriving (Eq, Ord, Data, Typeable, Generic) + deriving (Eq, Ord, Data, Generic) instance Hashable DataName @@ -86,7 +85,7 @@ , dcTheta :: [ty] -- ^ The GHC ThetaType corresponding to DataCon.dataConSig , dcFields :: [(LHName, ty)] -- ^ field-name and field-Type pairs , dcResult :: Maybe ty -- ^ Possible output (if in GADT form) - } deriving (Data, Typeable, Generic, Eq, Functor, Foldable, Traversable) + } deriving (Data, Generic, Eq, Functor, Foldable, Traversable) instance Hashable ty => Hashable (DataCtorP ty) @@ -94,7 +93,7 @@ data DataDeclKind = DataUser -- ^ User defined data-definitions (should have refined fields) | DataReflected -- ^ Automatically lifted data-definitions (do not have refined fields) - deriving (Eq, Data, Typeable, Generic, Show) + deriving (Eq, Data, Generic, Show) deriving Hashable via Generically DataDeclKind data HasDataDecl @@ -173,7 +172,7 @@ , dcpIsGadt :: !Bool -- ^ Was this specified in GADT style (if so, DONT use function names as fields) , dcpModule :: !F.Symbol -- ^ Which module was this defined in , dcpLocE :: !F.SourcePos - } deriving (Generic, Data, Typeable) + } deriving (Generic, Data) -- | [NOTE:DataCon-Data] for each 'DataConP' we also -- store the type of the constructed data. This is 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 @@ -58,7 +58,6 @@ import GHC.Generics import Control.DeepSeq import qualified Control.Exception as Ex -import Data.Typeable (Typeable) import Data.Generics (Data) import qualified Data.Binary as B import qualified Data.Maybe as Mb @@ -195,7 +194,7 @@ = OTerm -- ^ Obligation that proves termination | OInv -- ^ Obligation that proves invariants | OCons -- ^ Obligation that proves subtyping constraints - deriving (Eq, Generic, Data, Typeable) + deriving (Eq, Generic, Data) deriving Hashable via Generically Oblig instance B.Binary Oblig @@ -493,7 +492,7 @@ , msg :: !Doc } -- ^ Sigh. Other. - deriving (Typeable, Generic , Functor ) + deriving (Generic , Functor ) errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t errDupSpecs d spans@(sp:_) = ErrDupSpecs sp d spans diff --git a/src/Language/Haskell/Liquid/Types/Names.hs b/src/Language/Haskell/Liquid/Types/Names.hs --- a/src/Language/Haskell/Liquid/Types/Names.hs +++ b/src/Language/Haskell/Liquid/Types/Names.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskellQuotes #-} module Language.Haskell.Liquid.Types.Names ( lenLocSymbol , anyTypeSymbol @@ -47,12 +48,14 @@ import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name import qualified Liquid.GHC.API as GHC +import GHC.Types (Any) + -- RJ: Please add docs lenLocSymbol :: Located Symbol lenLocSymbol = dummyLoc $ symbol ("autolen" :: String) anyTypeSymbol :: Symbol -anyTypeSymbol = symbol ("GHC.Prim.Any" :: String) +anyTypeSymbol = symbol (show ''Any) selfSymbol :: Symbol selfSymbol = symbol ("liquid_internal_this" :: String) diff --git a/src/Language/Haskell/Liquid/Types/RType.hs b/src/Language/Haskell/Liquid/Types/RType.hs --- a/src/Language/Haskell/Liquid/Types/RType.hs +++ b/src/Language/Haskell/Liquid/Types/RType.hs @@ -139,7 +139,6 @@ import Control.DeepSeq import Data.Traversable (forAccumM) -import Data.Typeable (Typeable) import Data.Generics (Data) import qualified Data.Binary as B import Data.Hashable @@ -162,7 +161,7 @@ newtype RFInfo = RFInfo {permitTC :: Maybe Bool } - deriving (Generic, Data, Typeable, Show, Eq) + deriving (Generic, Data, Show, Eq) defRFInfo :: RFInfo defRFInfo = RFInfo Nothing @@ -214,7 +213,7 @@ , tcpVarianceTs :: !VarianceInfo , tcpVariancePs :: !VarianceInfo , tcpSizeFun :: !(Maybe SizeFun) - } deriving (Generic, Data, Typeable) + } deriving (Generic, Data) instance F.Loc TyConP where srcSpan tc = F.SS (tcpLoc tc) (tcpLoc tc) @@ -241,7 +240,7 @@ data SizeFunV v = IdSizeFun -- ^ \x -> F.EVar x | SymSizeFun (F.Located v) -- ^ \x -> f x - deriving (Data, Typeable, Generic, Eq, Functor, Foldable, Traversable) + deriving (Data, Generic, Eq, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (SizeFunV v) instance NFData v => NFData (SizeFunV v) @@ -269,7 +268,7 @@ , ptype :: !t , parg :: !Symbol , pargs :: ![(t, Symbol, F.ExprV v)] - } deriving (Generic, Data, Typeable, Show, Functor) + } deriving (Generic, Data, Show, Functor) deriving B.Binary via Generically (PVarV v t) mapPVarV :: (v -> v') -> (t -> t') -> PVarV v t -> PVarV v' t' @@ -355,7 +354,7 @@ type Predicate = PredicateV Symbol newtype PredicateV v = Pr [UsedPVarV v] - deriving (Generic, Data, Typeable) + deriving (Generic, Data) deriving (B.Binary, Hashable) via Generically (PredicateV v) mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v' @@ -419,10 +418,10 @@ instance NFData r => NFData (UReft r) newtype BTyVar = BTV F.LocSymbol - deriving (Show, Generic, Data, Typeable) + deriving (Show, Generic, Data) deriving (B.Binary, Hashable) via Generically BTyVar -newtype RTyVar = RTV TyVar deriving (Generic, Data, Typeable) +newtype RTyVar = RTV TyVar deriving (Generic, Data) instance Eq BTyVar where (BTV x) == (BTV y) = x == y @@ -451,7 +450,7 @@ , btc_class :: !Bool -- ^ Is this a class type constructor? , btc_prom :: !Bool -- ^ Is Promoted Data Con? } - deriving (Generic, Data, Typeable) + deriving (Generic, Data) deriving (B.Binary, Hashable) via Generically BTyCon data RTyCon = RTyCon @@ -459,7 +458,7 @@ , rtc_pvars :: ![RPVar] -- ^ Predicate Parameters , rtc_info :: !TyConInfo -- ^ TyConInfo } - deriving (Generic, Data, Typeable) + deriving (Generic, Data) instance F.Symbolic RTyCon where symbol = F.symbol . rtc_tc @@ -683,7 +682,7 @@ { varianceTyArgs :: !VarianceInfo -- ^ variance info for type variables , variancePsArgs :: !VarianceInfo -- ^ variance info for predicate variables , sizeFunction :: !(Maybe SizeFun) -- ^ logical UNARY function that computes the size of the structure - } deriving (Generic, Data, Typeable) + } deriving (Generic, Data) instance NFData TyConInfo @@ -769,7 +768,7 @@ | RHole r -- ^ let LH match against the Haskell type and add k-vars, e.g. `x:_` -- see tests/pos/Holes.hs - deriving (Eq, Generic, Data, Typeable, Functor, Foldable, Traversable) + deriving (Eq, Generic, Data, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (RTypeV v c tv r) instance (NFData c, NFData tv, NFData r) => NFData (RType c tv r) @@ -783,7 +782,7 @@ data RTVar tv s = RTVar { ty_var_value :: tv , ty_var_info :: RTVInfo s - } deriving (Generic, Data, Typeable, Functor, Foldable, Traversable) + } deriving (Generic, Data, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (RTVar tv s) mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s @@ -800,7 +799,7 @@ , rtv_is_pol :: Bool -- true iff the type variable gets instantiated with -- any refinement (ie is polymorphic on refinements), -- false iff instantiation is with true refinement - } deriving (Generic, Data, Typeable, Functor, Eq, Foldable, Traversable) + } deriving (Generic, Data, Functor, Eq, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (RTVInfo s) @@ -828,7 +827,7 @@ data Ref τ t = RProp { 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, Foldable, Traversable) + } deriving (Eq, Generic, Data, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (Ref τ t) instance (NFData τ, NFData t) => NFData (Ref τ t) @@ -846,7 +845,7 @@ { ur_reft :: !r , ur_pred :: !(PredicateV v) } - deriving (Eq, Generic, Data, Typeable, Functor, Foldable, Traversable) + deriving (Eq, Generic, Data, Functor, Foldable, Traversable) deriving (B.Binary, Hashable) via Generically (UReftV v r) mapUReftV :: (v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r' 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 @@ -1742,7 +1742,7 @@ = notracepp ("CLASSBINDS-1: " ++ showpp (toType False t, isEqualityConstr t)) [] isEqualityConstr :: SpecType -> Bool -isEqualityConstr (toType False -> ty) = Ghc.isEqPred ty || Ghc.isEqPrimPred ty +isEqualityConstr (toType False -> ty) = Ghc.isNomEqPred ty || Ghc.isEqPred ty -------------------------------------------------------------------------------- -- | Termination Predicates ---------------------------------------------------- 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 @@ -175,7 +175,6 @@ import Control.DeepSeq import Data.Bifunctor -import Data.Typeable (Typeable) import Data.Generics (Data) import qualified Data.Binary as B import Data.Hashable @@ -310,12 +309,12 @@ , riDictName :: Maybe (F.Located LHName) , ritype :: [t] , risigs :: [(F.Located LHName, RISig t)] - } deriving (Eq, Generic, Functor, Data, Typeable, Foldable, Traversable, Show) + } deriving (Eq, Generic, Functor, Data, Foldable, Traversable, Show) deriving Hashable via Generically (RInstance t) deriving B.Binary via Generically (RInstance t) data RISig t = RIAssumed t | RISig t - deriving (Eq, Generic, Functor, Data, Typeable, Show, Foldable, Traversable) + deriving (Eq, Generic, Functor, Data, Show, Foldable, Traversable) deriving Hashable via Generically (RISig t) deriving B.Binary via Generically (RISig t) @@ -377,7 +376,7 @@ , rtVArgs :: [Symbol] -- ^ value parameters , rtBody :: a -- ^ what the alias expands to -- , rtMod :: !ModName -- ^ module where alias was defined - } deriving (Eq, Data, Typeable, Generic, Functor, Foldable, Traversable) + } deriving (Eq, Data, Generic, Functor, Foldable, Traversable) deriving Hashable via Generically (RTAlias x a) deriving B.Binary via Generically (RTAlias x a) -- TODO support ghosts in aliases? @@ -517,10 +516,10 @@ -------------------------------------------------------------------------------- data ModName = ModName !ModType !ModuleName - deriving (Eq, Ord, Show, Generic, Data, Typeable) + deriving (Eq, Ord, Show, Generic, Data) data ModType = Target | SrcImport | SpecImport - deriving (Eq, Ord, Show, Generic, Data, Typeable) + deriving (Eq, Ord, Show, Generic, Data) -- instance B.Binary ModType -- instance B.Binary ModName @@ -592,7 +591,7 @@ = E (F.ExprV v) -- ^ Measure Refinement: {v | v = e } | P (F.ExprV v) -- ^ Measure Refinement: {v | (? v) <=> p } | R Symbol (F.ExprV v) -- ^ Measure Refinement: {v | p} - deriving (Show, Data, Typeable, Generic, Eq, Functor, Foldable, Traversable) + deriving (Show, Data, Generic, Eq, Functor, Foldable, Traversable) deriving B.Binary via Generically (BodyV v) deriving Hashable via Generically (BodyV v) @@ -613,7 +612,7 @@ , dsort :: Maybe ty , binds :: [(Symbol, Maybe ty)] -- measure binders: the ADT argument fields , body :: BodyV v - } deriving (Show, Data, Typeable, Generic, Eq, Functor) + } deriving (Show, Data, Generic, Eq, Functor) deriving B.Binary via Generically (DefV v ty ctor) deriving Hashable via Generically (DefV v ty ctor) @@ -650,7 +649,7 @@ , msEqns :: [DefV v ty ctor] , msKind :: !MeasureKind , msUnSorted :: !UnSortedExprs -- potential unsorted expressions used at measure denifinitions - } deriving (Eq, Data, Typeable, Generic, Functor) + } deriving (Eq, Data, Generic, Functor) deriving B.Binary via Generically (MeasureV v ty ctor) deriving Hashable via Generically (MeasureV v ty ctor) @@ -691,7 +690,7 @@ | MsAbsMeasure -- ^ due to `measure foo` without equations c.f. tests/pos/T1223.hs | MsSelector -- ^ due to selector-fields e.g. `data Foo = Foo { fld :: Int }` | MsChecker -- ^ due to checkers e.g. `is-F` for `data Foo = F ... | G ...` - deriving (Eq, Ord, Show, Data, Typeable, Generic) + deriving (Eq, Ord, Show, Data, Generic) deriving B.Binary via Generically MeasureKind deriving Hashable via Generically MeasureKind @@ -717,7 +716,7 @@ data CMeasure ty = CM { cName :: F.Located LHName , cSort :: ty - } deriving (Data, Typeable, Generic, Functor) + } deriving (Data, Generic, Functor) instance (F.PPrint v, Ord v, F.Fixpoint v) => F.PPrint (BodyV v) where pprintTidy k (E e) = F.pprintTidy k e @@ -789,7 +788,7 @@ , rcSupers :: [ty] , rcTyVars :: [BTyVar] , rcMethods :: [(F.Located LHName, ty)] - } deriving (Eq, Show, Functor, Data, Typeable, Generic, Foldable, Traversable) + } deriving (Eq, Show, Functor, Data, Generic, Foldable, Traversable) deriving B.Binary via Generically (RClass ty) deriving Hashable via Generically (RClass ty) @@ -834,14 +833,14 @@ ------------------------------------------------------------------------ newtype AnnInfo a = AI (M.HashMap SrcSpan [(Maybe Text, a)]) - deriving (Data, Typeable, Generic, Functor) + deriving (Data, Generic, Functor) data Annot t = AnnUse t | AnnDef t | AnnRDf t | AnnLoc SrcSpan - deriving (Data, Typeable, Generic, Functor) + deriving (Data, Generic, Functor) instance Monoid (AnnInfo a) where mempty = AI M.empty @@ -864,7 +863,7 @@ , o_templs :: !(AnnInfo a) , o_bots :: ![SrcSpan] , o_result :: ErrorResult - } deriving (Typeable, Generic, Functor) + } deriving (Generic, Functor) instance (F.PPrint a) => F.PPrint (Output a) where pprintTidy _ out = F.resultDoc (F.pprint <$> o_result out) @@ -905,7 +904,7 @@ | CaseE Int -- ^ Int is the number of cases | LetE | ProjectE -- ^ Projecting out field of - deriving (Generic, Eq, Ord, Show, Data, Typeable) + deriving (Generic, Eq, Ord, Show, Data) instance Hashable KVKind @@ -966,7 +965,7 @@ , measMap :: M.HashMap (F.Located LHName) (Measure ty ctor) , cmeasMap :: M.HashMap (F.Located LHName) (Measure ty ()) , imeas :: ![Measure ty ctor] - } deriving (Data, Typeable, Generic, Functor) + } deriving (Data, Generic, Functor) instance Bifunctor MSpec where first f (MSpec c m cm im) = MSpec (fmap (fmap (first f)) c) diff --git a/src/Language/Haskell/Liquid/Types/Variance.hs b/src/Language/Haskell/Liquid/Types/Variance.hs --- a/src/Language/Haskell/Liquid/Types/Variance.hs +++ b/src/Language/Haskell/Liquid/Types/Variance.hs @@ -11,7 +11,6 @@ import Prelude hiding (error) import Control.DeepSeq -import Data.Typeable hiding (TyCon) import Data.Data hiding (TyCon) import GHC.Generics import Data.Binary @@ -30,7 +29,7 @@ type VarianceInfo = [Variance] data Variance = Invariant | Bivariant | Contravariant | Covariant - deriving (Eq, Data, Typeable, Show, Generic) + deriving (Eq, Data, Show, Generic) deriving Hashable via Generically Variance flipVariance :: Variance -> Variance diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs --- a/src/Language/Haskell/Liquid/UX/Config.hs +++ b/src/Language/Haskell/Liquid/UX/Config.hs @@ -125,7 +125,7 @@ , dumpOpaqueReflections :: Bool -- Dumps all opaque reflections to the stdout , dumpPreNormalizedCore :: Bool -- Dumps the prenormalized core (before a-normalization) , allowUnsafeConstructors :: Bool -- ^ Allow refining constructors with unsafe refinements - } deriving (Generic, Data, Typeable, Show, Eq) + } deriving (Generic, Data, Show, Eq) allowPLE :: Config -> Bool allowPLE cfg diff --git a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs --- a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +++ b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs @@ -219,7 +219,7 @@ -------------------------------------------------------------------------------- newtype LiquidQuote = LiquidQuote { liquidQuoteSpec :: BPspec } - deriving (Data, Typeable) + deriving (Data) -------------------------------------------------------------------------------- -- Template Haskell Utility Functions ------------------------------------------ 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 @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -94,7 +95,7 @@ | s <- wiredTheorySyms , let srt = F.tsSort $ fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $ - F.lookupSEnv s (F.theorySymbols F.Z3 []) + F.lookupSEnv s (F.theorySymbols F.Z3) ] where wiredTheorySyms = @@ -256,17 +257,17 @@ derivingClasses :: [String] derivingClasses = - [ "GHC.Classes.Eq" - , "GHC.Classes.Ord" - , "GHC.Internal.Enum.Enum" - , "GHC.Internal.Show.Show" - , "GHC.Internal.Read.Read" - , "GHC.Internal.Base.Monad" - , "GHC.Internal.Base.Applicative" - , "GHC.Internal.Base.Functor" - , "GHC.Internal.Data.Foldable.Foldable" - , "GHC.Internal.Data.Traversable.Traversable" - , "GHC.Internal.Real.Fractional" + [ show ''Eq + , show ''Ord + , show ''Enum + , show ''Show + , show ''Read + , show ''Monad + , show ''Applicative + , show ''Functor + , show ''Foldable + , show ''Traversable + , show ''Fractional -- , "GHC.Enum.Bounded" -- , "GHC.Base.Monoid" ]