diff --git a/Changelog.md b/Changelog.md new file mode 100644 --- /dev/null +++ b/Changelog.md @@ -0,0 +1,44 @@ +# Changelog + +## 0.7.2.0 + +* Supports GHC 9.6 +* More robust `equational-reasoning` package detection logic. + +## 0.7.1.0 + +* Proper Support of GHC 9.4 (Now can solve `Assert` properly) + +## 0.7.0.0 + +* Support GHC 9.4 +* The plugin can solve constraints involving type-level `Assert`, `Not`, `(&&)`, `(||)`, and/or `If` from new base. + +## 0.6.2.0 + +* Support GHC 9.2.1 +* Decoding in Min/Max expression in terms of OrdCond + +## 0.6.0.0 + +* Stop discharging redundant constraints +* Support GHC 9.0.1 +* Drop a support for GHC <8.6 + +## 0.4.0.0 + +* Fixes constraint solving (fixes #9); this may change the previous (unsound) behaviour, and hence it is breaking change. + +## 0.3.0.1 + +* Supports GHC >= 8.10. + +## 0.3.0.0 + +* Drops support for GHC < 8.4 +* Entire overhaul. +* Adds `negated-numbers` option. +* Allows terms which includes uninterpreted terms (still much incomplete). +* Separates `singletons` support as `singletons-presburger` package. +* Provides an interface for extending solver with additional syntax constructs. + See `GHC.TypeLits.Presburger.Types` module for more detail. diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs --- a/examples/simple-arith-core.hs +++ b/examples/simple-arith-core.hs @@ -14,6 +14,7 @@ {-# LANGUAGE NoStarIsType #-} {-# 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 #-} @@ -27,7 +28,7 @@ import Data.Proxy import Numeric.Natural import Data.Type.Equality -import GHC.TypeLits +import GHC.TypeLits hiding (SNat) import Data.Void import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 @@ -43,7 +44,7 @@ type n <=! m = IsTrue (n <=? m) infix 4 <=! - +{- type family Length (as :: [k]) where Length '[] = 0 Length (x ': xs) = 1 + Length xs @@ -90,9 +91,12 @@ eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl -predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n) -predSucc _ = Witness - +predSuccBool :: forall proxy n. (n <=? 0) ~ 'False => proxy n -> IsTrue (n + 1 <=? 2 * n) +predSuccBool _ = Witness + -} +predSuccProp :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n) +predSuccProp _ = Witness +{- succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT succLEqLTSucc _ = Refl @@ -207,3 +211,4 @@ boolToPropLeq Zero m = ZeroLeq m boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness + -} diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: d6484409d9fcbd50b1fb2f56f79743a1587a1330768401bbaeecaa4e969e8160 +-- hash: d47f404951bd3c54bbbabe3cea49f853ffe14cf61c99382f7240c493409fcdda name: ghc-typelits-presburger -version: 0.7.1.0 +version: 0.7.2.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,9 @@ 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.4 GHC==9.4.3 + 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 +extra-source-files: + Changelog.md build-type: Simple source-repository head @@ -49,6 +51,7 @@ GHC.TypeLits.Presburger.Compat other-modules: Data.Integer.SAT + GHC.TypeLits.Presburger.Flags Paths_ghc_typelits_presburger hs-source-dirs: src @@ -56,7 +59,7 @@ build-depends: base >=4.7 && <5 , containers - , ghc <9.5 + , ghc <9.7 , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty @@ -75,7 +78,7 @@ build-depends: base , equational-reasoning - , ghc-typelits-presburger >=0.7.1.0 + , ghc-typelits-presburger default-language: Haskell2010 if !(flag(examples)) buildable: False diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs --- a/src/GHC/TypeLits/Presburger/Compat.hs +++ b/src/GHC/TypeLits/Presburger/Compat.hs @@ -8,8 +8,10 @@ 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.Functor ((<&>)) import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS) #if MIN_VERSION_ghc(9,4,1) import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..)) @@ -55,7 +57,7 @@ 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) +import GHC.Driver.Session (unitState, unitDatabases) #endif import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit, Name) #if MIN_VERSION_ghc(9,2,0) @@ -70,18 +72,36 @@ ) #endif +#if MIN_VERSION_ghc(9,6,1) import GHC.Plugins as GHC.TypeLits.Presburger.Compat + ( Subst (..), + emptySubst, + unionSubst, + ) +import GHC.Core.TyCo.Compare as GHC.TypeLits.Presburger.Compat + (eqType) +#else +import GHC.Plugins as GHC.TypeLits.Presburger.Compat + ( TCvSubst (..), + emptyTCvSubst, + eqType, + unionTCvSubst, + ) +#endif + +import GHC.Plugins as GHC.TypeLits.Presburger.Compat ( PackageName (..),isStrLitTy, isNumLitTy, nilDataCon, consDataCon, Hsc, Plugin (..), - TCvSubst (..), TvSubstEnv, TyVar, defaultPlugin, - emptyTCvSubst, - eqType, mkTcOcc, + UnitDatabase(..), + GenericUnitInfo(..), + elementOfUniqSet, + mkUniqSet, mkTyConTy, mkTyVarTy, ppr, @@ -93,14 +113,12 @@ text, tyConAppTyCon_maybe, typeKind, - unionTCvSubst, ) import GHC.Tc.Plugin (lookupOrig) import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances) #if MIN_VERSION_ghc(9,2,0) import GHC.Tc.Plugin (unsafeTcPluginTcM) import GHC.Utils.Logger (getLogger) -import Data.Functor ((<&>)) import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) @@ -141,9 +159,11 @@ 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) +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) @@ -242,25 +262,52 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv +#if MIN_VERSION_ghc(9,6,1) +type TCvSubst = Subst +unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst +unionTCvSubst = unionSubst + +emptyTCvSubst :: Subst +emptyTCvSubst = emptySubst +#endif + + instance Outputable TvSubst where ppr = ppr . toTCv emptyTvSubst :: TvSubst +#if MIN_VERSION_ghc(9,6,1) emptyTvSubst = case emptyTCvSubst of + Subst set _ tvsenv _ -> TvSubst set tvsenv +#else +emptyTvSubst = case emptyTCvSubst of 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 +#else toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM +#endif + substTy :: TvSubst -> Type -> Type substTy tvs = Old.substTy (toTCv tvs) unionTvSubst :: TvSubst -> TvSubst -> TvSubst unionTvSubst s1 s2 = fromTCv $ unionTCvSubst (toTCv s1) (toTCv s2) + fromTCv :: TCvSubst -> TvSubst +#if MIN_VERSION_ghc(9,6,1) +fromTCv (Subst set _ tvsenv _) = TvSubst set tvsenv +#else fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv +#endif + promotedBoolTyCon :: TyCon promotedBoolTyCon = boolTyCon @@ -391,38 +438,53 @@ fsToUnitId = toUnitId . fsToUnit #endif -type RawUnitId = FastString -preloadedUnitsM :: TcPluginM [FastString] +#if MIN_VERSION_ghc(9,0,0) +loadedPackageNames :: + [UnitDatabase UnitId] -> + UnitState -> + [RawPackageName] +loadedPackageNames unitDb us = + 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] #if MIN_VERSION_ghc(9,4,0) preloadedUnitsM = do logger <- unsafeTcPluginTcM getLogger dflags <- hsc_dflags <$> getTopEnv - packs <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> - \(_, us, _, _ ) -> preloadUnits us - let packNames = map (\(UnitId p) -> p) packs + packNames <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> + \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us tcPluginTrace "pres: packs" $ ppr packNames - pure packNames + pure $ coerce packNames #elif MIN_VERSION_ghc(9,2,0) preloadedUnitsM = do logger <- unsafeTcPluginTcM getLogger dflags <- hsc_dflags <$> getTopEnv - packs <- tcPluginIO $ initUnits logger dflags Nothing <&> - \(_, us, _, _ ) -> preloadUnits us - let packNames = map (\(UnitId p) -> p) packs + packNames <- tcPluginIO $ initUnits logger dflags Nothing <&> + \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us tcPluginTrace "pres: packs" $ ppr packNames pure packNames #elif MIN_VERSION_ghc(9,0,0) preloadedUnitsM = do dflags <- hsc_dflags <$> getTopEnv - packs <- tcPluginIO $ preloadUnits . unitState <$> initUnits dflags - let packNames = map (\(UnitId p) -> p) packs + packNames <- tcPluginIO $ initUnits dflags <&> \dfs' -> + let st = unitState dfs' + db = maybe [] id $ unitDatabases dfs' + in loadedPackageNames db st tcPluginTrace "pres: packs" $ ppr packNames pure packNames #else preloadedUnitsM = do dflags <- hsc_dflags <$> getTopEnv - (_, packs) <- tcPluginIO $ initPackages dflags - let packNames = map (\(InstalledUnitId p) -> p) packs + (dfs', packs) <- tcPluginIO $ initPackages dflags + let db = listPackageConfigMap dfs' + loadeds = mkUniqSet $ map (\(InstalledUnitId p) -> p) packs + packNames = map (coerce . packageName) $ + filter ((`elementOfUniqSet` loadeds) . coerce . unitId) db tcPluginTrace "pres: packs" $ ppr packNames pure packNames #endif diff --git a/src/GHC/TypeLits/Presburger/Flags.hs b/src/GHC/TypeLits/Presburger/Flags.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Presburger/Flags.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE CPP #-} +module GHC.TypeLits.Presburger.Flags (GHCVer(..), ghcVer) where +import GHC.Generics (Generic) + +data GHCVer + = GHC806 | GHC808 | GHC810 + | GHC900 | GHC902 | GHC904 | GHC906 + deriving (Show, Eq, Ord, Generic) + +ghcVer :: GHCVer +#if MIN_VERSION_ghc(9,6,1) +ghcVer = GHC906 +#elif MIN_VERSION_ghc(9,4,1) +ghcVer = GHC904 +#elif MIN_VERSION_ghc(9,2,1) +ghcVer = GHC902 +#elif MIN_VERSION_ghc(9,0,1) +ghcVer = GHC900 +#elif MIN_VERSION_ghc(8,10,1) +ghcVer = GHC810 +#elif MIN_VERSION_ghc(8,8,1) +ghcVer = GHC808 +#else +ghcVer = GHC806 +#endif diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs --- a/src/GHC/TypeLits/Presburger/Types.hs +++ b/src/GHC/TypeLits/Presburger/Types.hs @@ -58,6 +58,7 @@ import qualified Data.Set as Set import GHC.TypeLits.Presburger.Compat as Compat import qualified Data.Foldable as F +import GHC.TypeLits.Presburger.Flags assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos) @@ -376,13 +377,7 @@ defaultTranslation :: TcPluginM Translation defaultTranslation = do packs <- preloadedUnitsM - let eqThere = fromMaybe False $ - listToMaybe $ do - pname <- packs - rest <- - maybeToList $ - L.stripPrefix "equational-reasoning-" $ unpackFS pname - pure $ null rest || isDigit (head rest) + let eqThere = elem eqReasoning packs (isEmpties, isTrues) <- if eqThere then do @@ -401,7 +396,10 @@ eqBoolTyCon <- tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==") eqWitCon_ <- getEqWitnessTyCon assertTy <- lookupAssertTyCon - vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base") + vmd <- + if ghcVer >= GHC906 + then lookupModule (mkModuleName "GHC.Base") (fsLit "base") + else lookupModule (mkModuleName "Data.Void") (fsLit "base") voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void") nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq tyLeqB <- lookupTyNatBoolLeq diff --git a/test/GHC/TypeLits/PresburgerSpec.hs b/test/GHC/TypeLits/PresburgerSpec.hs --- a/test/GHC/TypeLits/PresburgerSpec.hs +++ b/test/GHC/TypeLits/PresburgerSpec.hs @@ -20,22 +20,22 @@ eith <- try $ void (evaluate $ NoPlugin.zipMVec (True :- Nil) (() :- Nil)) case eith of Left (TypeError msg) - | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" - `T.isInfixOf` T.pack msg - || - "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" - `T.isInfixOf` T.pack msg -> - pure () + | any (`T.isInfixOf` T.pack msg) + [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" + , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’" + ] + -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith , testCase "With plugin" $ do eith <- try $ void (evaluate $ Plugin.zipMVec (True :- Nil) (() :- Nil)) case eith of Left (TypeError msg) - | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" - `T.isInfixOf` T.pack msg - || "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" - `T.isInfixOf` T.pack msg -> - pure () + | any (`T.isInfixOf` T.pack msg) + [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" + , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’" + ] -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith ] @@ -47,22 +47,22 @@ eith <- try $ void (evaluate $ NoPlugin.unSpin (True :- Nil)) case eith of Left (TypeError msg) - | "Could not deduce: n1 ~ n" - `T.isInfixOf` T.pack msg - || "Could not deduce (n1 ~ n)" - `T.isInfixOf` T.pack msg - -> - pure () + | any (`T.isInfixOf` T.pack msg ) + [ "Could not deduce: n1 ~ n" + , "Could not deduce (n1 ~ n)" + , "Could not deduce ‘n1 ~ n’" + ] + -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith , testCase "With plugin" $ do eith <- try $ void (evaluate $ Plugin.unSpin (True :- Nil)) case eith of Left (TypeError msg) - | "Could not deduce: n1 ~ n" - `T.isInfixOf` T.pack msg - || - "Could not deduce (n1 ~ n)" - `T.isInfixOf` T.pack msg -> - pure () + | any (`T.isInfixOf` T.pack msg ) + [ "Could not deduce: n1 ~ n" + , "Could not deduce (n1 ~ n)" + , "Could not deduce ‘n1 ~ n’" + ] + -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith ]