liquidhaskell-boot 0.9.10.1.2 → 0.9.12.2

raw patch · 26 files changed

+201/−163 lines, 26 filesdep ~ghcdep ~liquid-fixpointPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc, liquid-fixpoint

API changes (from Hackage documentation)

Files

• liquidhaskell-boot.cabal +4/−4
• src-ghc/Liquid/GHC/API.hs +29/−9
• src-ghc/Liquid/GHC/API/Extra.hs +3/−2
• src/Language/Haskell/Liquid/Bare/Elaborate.hs +14/−6
• src/Language/Haskell/Liquid/Bare/Measure.hs +5/−1
• src/Language/Haskell/Liquid/Bare/Resolve.hs +1/−1
• src/Language/Haskell/Liquid/Constraint/Generate.hs +11/−4
• src/Language/Haskell/Liquid/GHC/Interface.hs +0/−15
• src/Language/Haskell/Liquid/GHC/Misc.hs +29/−6
• src/Language/Haskell/Liquid/GHC/Plugin.hs +2/−5
• src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs +1/−1
• src/Language/Haskell/Liquid/GHC/TypeRep.hs +0/−4
• src/Language/Haskell/Liquid/LHNameResolution.hs +4/−3
• src/Language/Haskell/Liquid/Parse.hs +4/−3
• src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +34/−38
• src/Language/Haskell/Liquid/Types/Bounds.hs +1/−1
• src/Language/Haskell/Liquid/Types/DataDecl.hs +5/−6
• src/Language/Haskell/Liquid/Types/Errors.hs +2/−3
• src/Language/Haskell/Liquid/Types/Names.hs +4/−1
• src/Language/Haskell/Liquid/Types/RType.hs +15/−16
• src/Language/Haskell/Liquid/Types/RefType.hs +1/−1
• src/Language/Haskell/Liquid/Types/Types.hs +16/−17
• src/Language/Haskell/Liquid/Types/Variance.hs +1/−2
• src/Language/Haskell/Liquid/UX/Config.hs +1/−1
• src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +1/−1
• src/Language/Haskell/Liquid/WiredIn.hs +13/−12

@@ -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

@@ -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

@@ -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

@@ -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"

@@ -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

@@ -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)

@@ -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 

@@ -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

@@ -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

@@ -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 =

@@ -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 

@@ -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) ++ ")"

@@ -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]

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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'

@@ -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 ----------------------------------------------------

@@ -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)

@@ -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

@@ -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

@@ -219,7 +219,7 @@ --------------------------------------------------------------------------------  newtype LiquidQuote = LiquidQuote { liquidQuoteSpec :: BPspec }-                      deriving (Data, Typeable)+                      deriving (Data)  -------------------------------------------------------------------------------- -- Template Haskell Utility Functions ------------------------------------------

@@ -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"   ]