ghc-typelits-presburger 0.7.2.0 → 0.7.3.0

raw patch · 6 files changed

+214/−396 lines, 6 filesdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• Changelog.md +5/−0
• examples/simple-arith-core.hs +4/−8
• ghc-typelits-presburger.cabal +5/−5
• src/Data/Integer/SAT.hs +93/−95
• src/GHC/TypeLits/Presburger/Compat.hs +102/−276
• src/GHC/TypeLits/Presburger/Types.hs +5/−12

@@ -1,5 +1,10 @@ # Changelog +## 0.7.3.0++* Supports GHC 9.8+* Drops support for GHC <9+ ## 0.7.2.0  * Supports GHC 9.6

@@ -8,19 +8,17 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} {-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806-{-# LANGUAGE NoStarIsType #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ViewPatterns #-}-#endif  module Main where @@ -74,10 +72,8 @@ absurdTrueFalse :: ( 'True :~: 'False) -> a absurdTrueFalse = \case {} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a hoge _ Witness = absurdTrueFalse Refl-#endif  bar :: (2 * (n + 1)) ~ (2 * n + 2) => proxy n -> () bar _ = ()

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack ----- hash: d47f404951bd3c54bbbabe3cea49f853ffe14cf61c99382f7240c493409fcdda+-- hash: 979226dcc13643574c669d5607b3d16d2cb873154282a49ef47bfd9c8b52c073  name:          ghc-typelits-presburger-version:       0.7.2.0+version:       0.7.3.0 synopsis:      Presburger Arithmetic Solver for GHC Type-level natural numbers. description:   @ghc-typelits-presburger@ augments GHC type-system with Presburger                Arithmetic Solver for Type-level natural numbers.@@ -30,7 +30,7 @@ license:       BSD3 license-file:  LICENSE tested-with:-    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.1+    GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.3 GHC==9.8.1 extra-source-files:     Changelog.md build-type:    Simple@@ -59,7 +59,7 @@   build-depends:       base >=4.7 && <5     , containers-    , ghc <9.7+    , ghc <9.9     , ghc-tcplugins-extra >=0.2 && <0.5     , mtl     , pretty

@@ -12,39 +12,38 @@   by   Sergey Berezin, Vijay Ganesh, and David L. Dill -}-module Data.Integer.SAT-  ( PropSet,-    noProps,-    checkSat,-    assert,-    Prop (..),-    Expr (..),-    BoundType (..),-    getExprBound,-    getExprRange,-    Name,-    toName,-    fromName,+module Data.Integer.SAT (+  PropSet,+  noProps,+  checkSat,+  assert,+  Prop (..),+  Expr (..),+  BoundType (..),+  getExprBound,+  getExprRange,+  Name,+  toName,+  fromName, -    -- * Iterators-    allSolutions,-    slnCurrent,-    slnNextVal,-    slnNextVar,-    slnEnumerate,+  -- * Iterators+  allSolutions,+  slnCurrent,+  slnNextVal,+  slnNextVar,+  slnEnumerate, -    -- * Debug-    dotPropSet,-    sizePropSet,-    allInerts,-    ppInerts,+  -- * Debug+  dotPropSet,+  sizePropSet,+  allInerts,+  ppInerts, -    -- * For QuickCheck-    iPickBounded,-    Bound (..),-    tConst,-  )-where+  -- * For QuickCheck+  iPickBounded,+  Bound (..),+  tConst,+) where  import Control.Applicative (Alternative (..), Applicative (..), (<$>)) import Control.Monad (MonadPlus (..), ap, guard, liftM)@@ -281,13 +280,13 @@  -- | The inert contains the solver state on one possible path. data Inerts = Inerts-  { -- | Known lower and upper bounds for variables.-    -- Each bound @(c,t)@ in the first list asserts that  @t < c * x@-    -- Each bound @(c,t)@ in the second list asserts that @c * x < t@-    bounds :: NameMap ([Bound], [Bound])-  , -- | Definitions for resolved variables.-    -- These form an idempotent substitution.-    solved :: NameMap Term+  { bounds :: NameMap ([Bound], [Bound])+  -- ^ Known lower and upper bounds for variables.+  -- Each bound @(c,t)@ in the first list asserts that  @t < c * x@+  -- Each bound @(c,t)@ in the second list asserts that @c * x < t@+  , solved :: NameMap Term+  -- ^ Definitions for resolved variables.+  -- These form an idempotent substitution.   }   deriving (Show) @@ -295,7 +294,7 @@ ppInerts is =   vcat $     [ppLower x b | (x, (ls, _)) <- bnds, b <- ls]-    ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]+      ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]       ++ [ppEq e | e <- Map.toList (solved is)]   where     bnds = Map.toList (bounds is)@@ -442,10 +441,10 @@         Just s2 -> go s2 k      hor s k =-      s :-      case slnNextVal s of-        Nothing -> k-        Just s1 -> hor s1 k+      s+        : case slnNextVal s of+          Nothing -> k+          Just s1 -> hor s1 k  slnNextVal :: Solutions -> Maybe Solutions slnNextVal Done = Nothing@@ -500,7 +499,7 @@     -- <=> x   <= (t-1) `div` c     normBound Upper (Bound c t) = do       k <- isConst t-      return (div (k -1) c)+      return (div (k - 1) c)  {- | The largest (resp. least) upper (resp. lower) bound on a term  that will satisfy the model@@ -542,7 +541,7 @@       Lower -> fst      scaleBound c b = case bt of-      Upper -> div (b -1) c+      Upper -> div (b - 1) c       Lower -> div b c + 1  iModel :: Inerts -> [(Name, Integer)]@@ -581,29 +580,30 @@   | Just a <- isConst t = guard (a == 0)   -- A + B * x = 0   | Just (a, b, x) <- tIsOneVar t =-    case divMod (- a) b of-      (q, 0) -> addDef x (tConst q)-      _ -> mzero+      case divMod (-a) b of+        (q, 0) -> addDef x (tConst q)+        _ -> mzero   --  x + S = 0   -- -x + S = 0   | Just (xc, x, s) <- tGetSimpleCoeff t =-    addDef x (if xc > 0 then tNeg s else s)+      addDef x (if xc > 0 then tNeg s else s)   -- A * S = 0   | Just (_, s) <- tFactor t = solveIs0 s   -- See Section 3.1 of paper for details.   -- We obtain an equivalent formulation but with smaller coefficients.   | Just (ak, xk, s) <- tLeastAbsCoeff t =-    do-      let m = abs ak + 1-      v <- newVar-      let sgn = signum ak-          soln =-            (negate sgn * m) |*| tVar v-              |+| tMapCoeff (\c -> sgn * modulus c m) s-      addDef xk soln+      do+        let m = abs ak + 1+        v <- newVar+        let sgn = signum ak+            soln =+              (negate sgn * m)+                |*| tVar v+                |+| tMapCoeff (\c -> sgn * modulus c m) s+        addDef xk soln -      let upd i = div (2 * i + m) (2 * m) + modulus i m-      solveIs0 (negate (abs ak) |*| tVar v |+| tMapCoeff upd s)+        let upd i = div (2 * i + m) (2 * m) + modulus i m+        solveIs0 (negate (abs ak) |*| tVar v |+| tMapCoeff upd s)   | otherwise = error "solveIs0: unreachable"  modulus :: Integer -> Integer -> Integer@@ -623,40 +623,40 @@   | Just (_, s) <- tFactor t = solveIsNeg s   -- See Section 5.1 of the paper   | Just (xc, x, s) <- tLeastVar t =-    do-      ctrs <--        if xc < 0-          then -- -XC*x + S < 0-          -- S < XC*x-          do-            ubs <- getBounds Upper x-            let b = negate xc-                beta = s-            addBound Lower x (Bound b beta)-            return [(a, alpha, b, beta) | Bound a alpha <- ubs]-          else -- XC*x + S < 0-          -- XC*x < -S-          do-            lbs <- getBounds Lower x-            let a = xc-                alpha = tNeg s-            addBound Upper x (Bound a alpha)-            return [(a, alpha, b, beta) | Bound b beta <- lbs]--      -- See Note [Shadows]-      mapM_-        ( \(a, alpha, b, beta) ->+      do+        ctrs <-+          if xc < 0+            then -- -XC*x + S < 0+            -- S < XC*x             do-              let real = ctLt (a |*| beta) (b |*| alpha)-                  dark = ctLt (tConst (a * b)) (b |*| alpha |-| a |*| beta)-                  gray =-                    [ ctEq (b |*| tVar x) (tConst i |+| beta)-                    | i <- [1 .. b - 1]-                    ]-              solveIsNeg real-              foldl orElse (solveIsNeg dark) (map solveIs0 gray)-        )-        ctrs+              ubs <- getBounds Upper x+              let b = negate xc+                  beta = s+              addBound Lower x (Bound b beta)+              return [(a, alpha, b, beta) | Bound a alpha <- ubs]+            else -- XC*x + S < 0+            -- XC*x < -S+            do+              lbs <- getBounds Lower x+              let a = xc+                  alpha = tNeg s+              addBound Upper x (Bound a alpha)+              return [(a, alpha, b, beta) | Bound b beta <- lbs]++        -- See Note [Shadows]+        mapM_+          ( \(a, alpha, b, beta) ->+              do+                let real = ctLt (a |*| beta) (b |*| alpha)+                    dark = ctLt (tConst (a * b)) (b |*| alpha |-| a |*| beta)+                    gray =+                      [ ctEq (b |*| tVar x) (tConst i |+| beta)+                      | i <- [1 .. b - 1]+                      ]+                solveIsNeg real+                foldl orElse (solveIsNeg dark) (map solveIs0 gray)+          )+          ctrs   | otherwise = error "solveIsNeg: unreachable"  orElse :: S () -> S () -> S ()@@ -712,7 +712,8 @@ dotAnswer pp g0 = vcat [text "digraph {", nest 2 (fst $ go 0 g0), text "}"]   where     node x d =-      integer x <+> brackets (text "label=" <> text (show d))+      integer x+        <+> brackets (text "label=" <> text (show d))         <> semi     edge x y = integer x <+> text "->" <+> integer y @@ -746,9 +747,6 @@     go None xs = xs  instance Monad Answer where-#if !MIN_VERSION_ghc(8,8,1)-  fail _             = None-#endif   None >>= _ = None   One a >>= k = k a   Choice m1 m2 >>= k = mplus (m1 >>= k) (m2 >>= k)

@@ -1,18 +1,27 @@-{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-}+ module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where-import Data.Function       (on)-import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName,-                                          tracePlugin)-import Data.Generics.Twins-import Data.Coerce (coerce) -#if MIN_VERSION_ghc(9,0,0)+import Data.Coerce (coerce)+import Data.Function (on) import Data.Functor ((<&>))+import Data.Generics.Twins import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS)+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (CtLoc (..), initialSubGoalDepth)+import GHC.Tc.Types.Origin as GHC.TypeLits.Presburger.Compat (CtOrigin (..))+import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (+  evByFiat,+  lookupModule,+  lookupName,+  tracePlugin,+ ) #if MIN_VERSION_ghc(9,4,1) import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..)) import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon)@@ -30,16 +39,13 @@ import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (dATA_TYPE_EQUALITY) import qualified GHC.Builtin.Names as Old #endif-import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule(..), NoExtField(..))-import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl(..), ImportDeclQualifiedStyle(..))-import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)-import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat-  ( boolTyCon,-    eqTyConName,-    promotedEQDataCon,-    promotedGTDataCon,-    promotedLTDataCon,-  )+import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (+  boolTyCon,+  eqTyConName,+  promotedEQDataCon,+  promotedGTDataCon,+  promotedLTDataCon,+ ) import qualified GHC.Builtin.Types as TysWiredIn import GHC.Builtin.Types.Literals as GHC.TypeLits.Presburger.Compat import GHC.Core.Class as GHC.TypeLits.Presburger.Compat (className, classTyCon)@@ -50,16 +56,19 @@ import GHC.Core.TyCon as GHC.TypeLits.Presburger.Compat import qualified GHC.Core.Type as Old import GHC.Core.Unify as Old (tcUnifyTy)+import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)+import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule (..), NoExtField (..))+import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)+import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl (..), ImportDeclQualifiedStyle (..)) import GHC.Unit.Types (Module, UnitId, toUnitId) import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule)-import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS) #if MIN_VERSION_ghc(9,2,0) import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) import GHC.Driver.Session (unitState, unitDatabases) #endif-import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit, Name)+import GHC.Plugins (InScopeSet, Name, Outputable, Unit, emptyUFM, moduleUnit) #if MIN_VERSION_ghc(9,2,0) import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsParsedModule(..)) import GHC.Types.TyThing as GHC.TypeLits.Presburger.Compat (lookupTyCon)@@ -89,33 +98,36 @@   ) #endif -import GHC.Plugins as GHC.TypeLits.Presburger.Compat-  ( PackageName (..),isStrLitTy, isNumLitTy,-    nilDataCon, consDataCon,-    Hsc,-    Plugin (..),-    TvSubstEnv,-    TyVar,-    defaultPlugin,-    mkTcOcc,-    UnitDatabase(..),-    GenericUnitInfo(..),-    elementOfUniqSet,-    mkUniqSet,-    mkTyConTy,-    mkTyVarTy,-    ppr,-    promotedFalseDataCon,-    promotedTrueDataCon,-    purePlugin,-    splitTyConApp,-    splitTyConApp_maybe,-    text,-    tyConAppTyCon_maybe,-    typeKind,-  )-import GHC.Tc.Plugin (lookupOrig) import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances)+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (+  GenericUnitInfo (..),+  Hsc,+  PackageName (..),+  Plugin (..),+  TvSubstEnv,+  TyVar,+  UnitDatabase (..),+  consDataCon,+  defaultPlugin,+  elementOfUniqSet,+  isNumLitTy,+  isStrLitTy,+  mkTcOcc,+  mkTyConTy,+  mkTyVarTy,+  mkUniqSet,+  nilDataCon,+  ppr,+  promotedFalseDataCon,+  promotedTrueDataCon,+  purePlugin,+  splitTyConApp,+  splitTyConApp_maybe,+  text,+  tyConAppTyCon_maybe,+  typeKind,+ )+import GHC.Tc.Plugin (lookupOrig) #if MIN_VERSION_ghc(9,2,0) import GHC.Tc.Plugin (unsafeTcPluginTcM) import GHC.Utils.Logger (getLogger)@@ -124,127 +136,40 @@ import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) #endif -import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat-  ( TcPluginM,-    getInstEnvs,-    newFlexiTyVar,-    getTopEnv,-    lookupOrig,-    newFlexiTyVar,-    newWanted,-    matchFam,-    tcLookupClass,-    tcLookupTyCon,-    tcPluginIO,-    tcPluginTrace,-  )+import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat (+  TcPluginM,+  getInstEnvs,+  getTopEnv,+  lookupOrig,+  matchFam,+  newFlexiTyVar,+  newWanted,+  tcLookupClass,+  tcLookupTyCon,+  tcPluginIO,+  tcPluginTrace,+ ) import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..))-import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat-  ( Ct,-    CtEvidence,-    ctEvPred,-    ctEvidence,-    isWanted,-  )+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (+  Ct,+  CtEvidence,+  ctEvPred,+  ctEvidence,+  isWanted,+ ) import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (EvTerm)+import GHC.Tc.Utils.Monad as GHC.TypeLits.Presburger.Compat (getCtLocM, unsafeTcPluginTcM) import GHC.Tc.Utils.TcType (TcTyVar, TcType) import GHC.Tc.Utils.TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts) import qualified GHC.TcPluginM.Extra as Extra import GHC.Types.Name.Occurrence as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc) import GHC.Types.Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique) import GHC.Unit.Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName)+import GHC.Unit.State (UnitState (preloadUnits), initUnits) import GHC.Unit.State as GHC.TypeLits.Presburger.Compat (lookupPackageName)-import GHC.Unit.State (initUnits, UnitState (preloadUnits))-import GHC.Unit.Types (UnitId(..), fsToUnit, toUnitId)+import GHC.Unit.Types (UnitId (..), fsToUnit, toUnitId) import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)--- GHC 9 Ends HERE-#else-import UniqSet-import PackageConfig-import Class as GHC.TypeLits.Presburger.Compat (classTyCon, className)-import FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)-import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages, Name, listPackageConfigMap)-import GhcPlugins as GHC.TypeLits.Presburger.Compat (PackageName (..), fsToUnitId, lookupPackageName, lookupTyCon, mkTcOcc, mkTyConTy, ppr, promotedFalseDataCon, promotedTrueDataCon, text, tyConAppTyCon_maybe, typeKind, typeNatKind)-import HscTypes as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))-import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName, mkModule)-import Module (Module, UnitId)-import OccName as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)-import Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)-import Plugins as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin)-import PrelNames as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY)-import qualified PrelNames as Old-import TcEvidence as GHC.TypeLits.Presburger.Compat (EvTerm)-import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps)-import TcPluginM as GHC.TypeLits.Presburger.Compat-  ( TcPluginM,-    getTopEnv,-    lookupOrig,-    matchFam,-    newFlexiTyVar,-    newWanted,-    tcLookupClass,-    tcLookupTyCon,-    tcPluginIO,-    tcPluginTrace,-  )-import TcRnMonad as GHC.TypeLits.Presburger.Compat (TcPluginResult (..))-import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..))-import TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)-import TcTypeNats as GHC.TypeLits.Presburger.Compat-import TyCoRep ()-import TyCoRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))-import TyCon as GHC.TypeLits.Presburger.Compat-import Type as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv, emptyTCvSubst, eqType, mkTyVarTy, splitTyConApp, splitTyConApp_maybe, unionTCvSubst)-import qualified Type as Old-import TysWiredIn as GHC.TypeLits.Presburger.Compat-  ( boolTyCon,-    promotedEQDataCon,-    promotedGTDataCon,-    promotedLTDataCon,-  )-import Unify as Old (tcUnifyTy)-import Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique)-import Var as GHC.TypeLits.Presburger.Compat (TyVar)--- Conditional imports for GHC <9-#if MIN_VERSION_ghc(8,4,1)-import TcType (TcTyVar, TcType)-import qualified GHC.TcPluginM.Extra as Extra-import qualified GHC-#else-import Data.Maybe-import TcPluginM (zonkCt)-import TcRnTypes (cc_ev, ctev_pred)-#endif-#if MIN_VERSION_ghc(8,6,0)-import Plugins as GHC.TypeLits.Presburger.Compat (purePlugin)-#endif-#if MIN_VERSION_ghc(8,8,1)-import Name-import TysWiredIn as GHC.TypeLits.Presburger.Compat (eqTyConName) -import qualified TysWiredIn-#else-import PrelNames as GHC.TypeLits.Presburger.Compat (eqTyConName) -#endif -#if MIN_VERSION_ghc(8,10,1)-import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..))-import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred)-import GHC (NoExtField(..))-import qualified Predicate as Old (classifyPredType)-import Predicate as GHC.TypeLits.Presburger.Compat  (mkPrimEqPredRole)-import Constraint as GHC.TypeLits.Presburger.Compat -    (Ct, ctEvidence, CtEvidence, ctEvPred, isWanted)-#else-import GHC (NoExt(..))-import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))-import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred)-import qualified GhcPlugins as Old (classifyPredType)-import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, isWanted)-import Type      as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole)-import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence)-#endif-#endif- #if !MIN_VERSION_ghc(9,4,1) type TcPluginSolveResult = TcPluginResult #endif@@ -254,12 +179,8 @@ dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality" #endif -#if MIN_VERSION_ghc(8,10,1) type PredTree = Pred-#endif --#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv  #if MIN_VERSION_ghc(9,6,1)@@ -271,8 +192,7 @@ emptyTCvSubst = emptySubst #endif --instance Outputable  TvSubst where+instance Outputable TvSubst where   ppr = ppr . toTCv  emptyTvSubst :: TvSubst@@ -284,7 +204,6 @@   TCvSubst set tvsenv _ -> TvSubst set tvsenv #endif - toTCv :: TvSubst -> TCvSubst #if MIN_VERSION_ghc(9,6,1) toTCv (TvSubst set tvenv) = Subst set emptyUFM tvenv emptyUFM@@ -292,7 +211,6 @@ toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM #endif - substTy :: TvSubst -> Type -> Type substTy tvs = Old.substTy (toTCv tvs) @@ -307,7 +225,6 @@ fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv #endif - promotedBoolTyCon :: TyCon promotedBoolTyCon = boolTyCon @@ -316,52 +233,23 @@   | Old.isFunTy t = Just (t1, t2) viewFunTy _ = Nothing -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 802-#else-pattern FunTy :: Type -> Type -> Type-pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where-  FunTy t1 t2 = Old.mkFunTy t1 t2-#endif- tcUnifyTy :: Type -> Type -> Maybe TvSubst tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2  getEqTyCon :: TcPluginM TyCon getEqTyCon =-#if MIN_VERSION_ghc(8,8,1)   return TysWiredIn.eqTyCon-#else-  tcLookupTyCon Old.eqTyConName-#endif -#else-eqType :: Type -> Type -> Bool-eqType = (==)--getEqTyCon :: TcPluginM TyCon-getEqTyCon = return Old.eqTyCon--#endif-- getEqWitnessTyCon :: TcPluginM TyCon getEqWitnessTyCon = do   md <- lookupModule (mkModuleName "Data.Type.Equality") (fsLit "base")   tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:")  decompFunTy :: Type -> [Type]-#if MIN_VERSION_ghc(9,0,0) decompFunTy (FunTy _ _ t1 t2) = t1 : decompFunTy t2-#else-#if MIN_VERSION_ghc(8,10,1)-decompFunTy (FunTy _ t1 t2) = t1 : decompFunTy t2-#else-decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2-#endif-#endif-decompFunTy t             = [t]+decompFunTy t = [t] -newtype TypeEq = TypeEq { runTypeEq :: Type }+newtype TypeEq = TypeEq {runTypeEq :: Type}  instance Eq TypeEq where   (==) = geq `on` runTypeEq@@ -375,15 +263,13 @@     EqPred _ l r -> l `eqType` r     _ -> False -normaliseGivens-  :: [Ct] -> TcPluginM [Ct]+normaliseGivens ::+  [Ct] -> TcPluginM [Ct] normaliseGivens =-#if MIN_VERSION_ghc(8,4,1)-  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence)) -  . (++) <$> id <*> Extra.flattenGivens-#else-  mapM zonkCt -#endif+  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence))+    . (++)+    <$> id+    <*> Extra.flattenGivens  #if MIN_VERSION_ghc(8,4,1) type Substitution = [(TcTyVar, TcType)]@@ -392,53 +278,25 @@ #endif  subsCt :: Substitution -> Ct -> Ct-subsCt =-#if MIN_VERSION_ghc(8,4,1)-  Extra.substCt-#else-  \subst ct ->-  ct { cc_ev = (cc_ev ct) {ctev_pred = substTy subst (ctev_pred (cc_ev ct))}-     }-#endif+subsCt = Extra.substCt  subsType :: Substitution -> Type -> Type-subsType =-#if MIN_VERSION_ghc(8,4,1)-  Extra.substType-#else-  substTy-#endif+subsType = Extra.substType  mkSubstitution :: [Ct] -> Substitution-mkSubstitution =-#if MIN_VERSION_ghc(8,4,1)-  map fst . Extra.mkSubst'-#else-  foldr (unionTvSubst . genSubst) emptyTvSubst-#endif--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804-genSubst :: Ct -> TvSubst-genSubst ct = case classifyPredType (ctEvPred . ctEvidence $ ct) of-  EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u-  _                -> emptyTvSubst-#endif-+mkSubstitution = map fst . Extra.mkSubst'  classifyPredType :: Type -> PredTree classifyPredType ty = case Old.classifyPredType ty of-  e@EqPred{} -> e-  ClassPred cls [_,t1,t2]-    | className cls == eqTyConName-    -> EqPred NomEq t1 t2+  e@EqPred {} -> e+  ClassPred cls [_, t1, t2]+    | className cls == eqTyConName ->+        EqPred NomEq t1 t2   e -> e -#if MIN_VERSION_ghc(9,0,0) fsToUnitId :: FastString -> UnitId fsToUnitId = toUnitId . fsToUnit-#endif -#if MIN_VERSION_ghc(9,0,0) loadedPackageNames ::   [UnitDatabase UnitId] ->   UnitState ->@@ -447,11 +305,10 @@   let preloads = mkUniqSet $ map (\(UnitId p) -> p) $ preloadUnits us       ents = filter ((`elementOfUniqSet` preloads) . unitIdFS . unitId) $ concatMap unitDatabaseUnits unitDb    in map (coerce . unitPackageName) ents-#endif - type RawPackageName = FastString-preloadedUnitsM :: TcPluginM [RawPackageName] ++preloadedUnitsM :: TcPluginM [RawPackageName] #if MIN_VERSION_ghc(9,4,0) preloadedUnitsM = do   logger <- unsafeTcPluginTcM getLogger@@ -489,45 +346,16 @@   pure packNames #endif --#if MIN_VERSION_ghc(9,0,0) type ModuleUnit = Unit+ moduleUnit' :: Module -> ModuleUnit moduleUnit' = moduleUnit-#else-type ModuleUnit = UnitId-moduleUnit' :: Module -> ModuleUnit-moduleUnit' = GHC.moduleUnitId-#endif -#if !MIN_VERSION_ghc(8,10,1)-type NoExtField = NoExt-#endif- noExtField :: NoExtField-#if MIN_VERSION_ghc(8,10,1) noExtField = NoExtField-#else-noExtField = NoExt-#endif -#if MIN_VERSION_ghc(9,0,1) type HsModule' = HsModule-#else-type HsModule' = GHC.HsModule GHC.GhcPs-#endif -#if !MIN_VERSION_ghc(9,0,1)-type IsBootInterface = Bool-pattern NotBoot :: IsBootInterface-pattern NotBoot = False--pattern IsBoot :: IsBootInterface-pattern IsBoot = True--{-# COMPLETE NotBoot, IsBoot #-}--#endif #if MIN_VERSION_ghc(9,2,0) typeNatKind :: TcType typeNatKind = naturalTy@@ -568,8 +396,8 @@ lookupAssertTyCon = pure Nothing #endif - lookupTyNatPredLt :: TcPluginM (Maybe TyCon)+ -- Note:  base library shipepd with 9.2.1 has a wrong implementation; -- hence we MUST NOT desugar it with <= 9.2.1 #if MIN_VERSION_ghc(9,2,2)@@ -643,7 +471,6 @@ lookupTyGenericCompare = pure Nothing #endif - lookupBool47 :: String -> TcPluginM (Maybe TyCon) #if MIN_VERSION_base(4,17,0) lookupBool47 nam = Just <$> do@@ -658,8 +485,7 @@ lookupTyAnd = lookupBool47 "&&" lookupTyOr = lookupBool47 "||" --matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe  Type)+matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe Type) #if MIN_VERSION_ghc(9,4,1) matchFam' con args = fmap reductionReducedType <$> matchFam con args #else

@@ -18,6 +18,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-}+ -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types   ( pluginWith,@@ -106,9 +107,7 @@ pluginWith trans =   defaultPlugin     { tcPlugin = Just . presburgerPlugin trans . procOpts-#if MIN_VERSION_ghc(8,6,0)     , pluginRecompile = purePlugin-#endif     }   where     procOpts opts@@ -733,15 +732,7 @@  simpleExp :: Given Translation => Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)-#if MIN_VERSION_ghc(9,0,0) simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2)-#else-#if MIN_VERSION_ghc(8,10,1)-simpleExp (FunTy f t1 t2) = FunTy f (simpleExp t1) (simpleExp t2)-#else-simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)-#endif-#endif  simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) simpleExp (TyConApp tc (lastTwo -> ts)) =   fromMaybe (TyConApp tc (map simpleExp ts)) $@@ -767,11 +758,13 @@  type Machine = MaybeT (StateT ParseEnv TcPluginM) + runMachine :: Machine a -> TcPluginM (Maybe a) runMachine act = do   (ma, dic) <- runStateT (runMaybeT act) M.empty-  forM_ (M.toList dic) $ \(TypeEq ty, var) ->-    newWanted undefined $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty+  forM_ (M.toList dic) $ \(TypeEq ty, var) -> do+    loc <- unsafeTcPluginTcM $ getCtLocM (Shouldn'tHappenOrigin "runMachine dummy wanted") Nothing+    newWanted loc $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty   return ma  toVar :: Type -> Machine TyVar