diff --git a/Changelog.md b/Changelog.md --- a/Changelog.md +++ b/Changelog.md @@ -1,9 +1,5 @@ # Changelog -## 0.7.4.1 - -* Supports GHC 9.8.4 - ## 0.7.4.0 * Supports GHC 9.10 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 @@ -1,34 +1,31 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -dcore-lint #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} {-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-} - +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Main where -import Unsafe.Coerce import Data.Proxy -import Numeric.Natural import Data.Type.Equality -import GHC.TypeLits hiding (SNat) import Data.Void +import GHC.TypeLits hiding (SNat) +import Numeric.Natural import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) +import Unsafe.Coerce #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 import qualified Data.Type.Ord as DTO #endif @@ -42,7 +39,7 @@ type n <=! m = IsTrue (n <=? m) infix 4 <=! -{- + type family Length (as :: [k]) where Length '[] = 0 Length (x ': xs) = 1 + Length xs @@ -69,13 +66,13 @@ minusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <=? m) minusLeq _ _ = Witness -absurdTrueFalse :: ( 'True :~: 'False) -> a +absurdTrueFalse :: ('True :~: 'False) -> a absurdTrueFalse = \case {} hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a hoge _ Witness = absurdTrueFalse Refl -bar :: (2 * (n + 1)) ~ (2 * n + 2) => proxy n -> () +bar :: ((2 * (n + 1)) ~ (2 * n + 2)) => proxy n -> () bar _ = () barResult :: () @@ -87,12 +84,12 @@ eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl -predSuccBool :: forall proxy n. (n <=? 0) ~ 'False => proxy n -> IsTrue (n + 1 <=? 2 * n) +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 :: 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 @@ -192,10 +189,10 @@ then unsafeCoerce IsZero else unsafeCoerce (SNat (n - 1)) -pattern Zero :: forall n. () => n ~ 0 => SNat n +pattern Zero :: forall n. () => (n ~ 0) => SNat n pattern Zero <- (viewNat -> IsZero) -pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n +pattern Succ :: forall n. () => forall n1. (n ~ Succ n1) => SNat n1 -> SNat n pattern Succ n <- (viewNat -> IsSucc n) {-# COMPLETE Zero, Succ #-} @@ -207,4 +204,3 @@ 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 @@ -1,39 +1,38 @@ -cabal-version: 1.12 - --- This file has been generated from package.yaml by hpack version 0.36.0. --- --- see: https://github.com/sol/hpack --- --- hash: f62c6305d38380eb4cc8063c8e4c4b0056c9bcb01d01075789915680436a7263 +cabal-version: 3.4 +name: ghc-typelits-presburger +version: 0.7.4.2 +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. + This plugin only work with GHC builtin operations. + To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead. + . + Since 0.3.0.0, integration with package moves to . + . + You can use by adding this package to @build-depends@ and add the following pragma + to the head of .hs files: + . + . + > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger -name: ghc-typelits-presburger -version: 0.7.4.1 -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. - This plugin only work with GHC builtin operations. - To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead. - . - Since 0.3.0.0, integration with package moves to . - . - You can use by adding this package to @build-depends@ and add the following pragma - to the head of .hs files: - . - . - > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger -category: Math, Type System -homepage: https://github.com/konn/ghc-typelits-presburger#readme -bug-reports: https://github.com/konn/ghc-typelits-presburger/issues -author: Hiromi ISHII -maintainer: konn.jinro _at_ gmail.com -copyright: 2015 (c) Hiromi ISHII -license: BSD3 -license-file: LICENSE +category: Math, Type System +homepage: https://github.com/konn/ghc-typelits-presburger#readme +bug-reports: https://github.com/konn/ghc-typelits-presburger/issues +author: Hiromi ISHII +maintainer: konn.jinro _at_ gmail.com +copyright: 2015-2025 (c) Hiromi ISHII +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple tested-with: - GHC==9.2.8 GHC==9.4.8 GHC==9.6.5 GHC==9.8.4 GHC==9.10.1 + ghc ==9.6.7 + ghc ==9.8.4 + ghc ==9.10.2 + ghc ==9.12.2 + extra-source-files: - Changelog.md -build-type: Simple + Changelog.md source-repository head type: git @@ -44,66 +43,76 @@ manual: False default: False +common defaults + autogen-modules: Paths_ghc_typelits_presburger + other-modules: Paths_ghc_typelits_presburger + default-language: Haskell2010 + ghc-options: + -Wall + -Wcompat + -Widentities + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wmissing-export-lists + -Wmissing-home-modules + -Wpartial-fields + -Wredundant-constraints + -Wunused-packages + library + import: defaults + hs-source-dirs: src exposed-modules: - GHC.TypeLits.Presburger.Types - GHC.TypeLits.Presburger - GHC.TypeLits.Presburger.Compat + GHC.TypeLits.Presburger + GHC.TypeLits.Presburger.Compat + GHC.TypeLits.Presburger.Types + other-modules: - Data.Integer.SAT - GHC.TypeLits.Presburger.Flags - Paths_ghc_typelits_presburger - hs-source-dirs: - src - ghc-options: -Wall -Wno-dodgy-imports + Data.Integer.SAT + GHC.TypeLits.Presburger.Flags + build-depends: - base >=4.7 && <5 - , containers - , ghc <9.13 - , ghc-tcplugins-extra >=0.2 && <0.5 - , mtl - , pretty - , reflection - , syb - , transformers - default-language: Haskell2010 + base >=4.7 && <5, + containers, + ghc <9.13, + ghc-tcplugins-extra >=0.2 && <0.6, + mtl, + pretty, + reflection, + syb, + transformers, executable simple-arith-core + import: defaults main-is: simple-arith-core.hs - other-modules: - Paths_ghc_typelits_presburger - hs-source-dirs: - examples - ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports + hs-source-dirs: examples build-depends: - base - , equational-reasoning - , ghc-typelits-presburger - default-language: Haskell2010 + base, + equational-reasoning, + ghc-typelits-presburger, + if !(flag(examples)) buildable: False test-suite test-typeltis-presburger + import: defaults type: exitcode-stdio-1.0 main-is: test.hs + hs-source-dirs: test + -- cabal-gild: discover test --exclude=test/test.hs other-modules: - ErrorsNoPlugin - ErrorsWithPlugin - GHC.TypeLits.PresburgerSpec - Shared - Paths_ghc_typelits_presburger - hs-source-dirs: - test - ghc-options: -Wall -Wno-dodgy-imports - build-tool-depends: - tasty-discover:tasty-discover + ErrorsNoPlugin + ErrorsWithPlugin + GHC.TypeLits.PresburgerSpec + Shared + + build-tool-depends: tasty-discover:tasty-discover build-depends: - base - , equational-reasoning - , ghc-typelits-presburger - , tasty - , tasty-discover - , tasty-expected-failure - , tasty-hunit - , text - default-language: Haskell2010 + base, + equational-reasoning, + ghc-typelits-presburger, + tasty, + tasty-discover, + tasty-expected-failure, + tasty-hunit, + text, 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 @@ -1,3 +1,5 @@ +{- HLINT ignore "Use camelCase" -} +{- HLINT ignore "Move filter" -} {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} @@ -25,7 +27,7 @@ import GHC.Builtin.Names (gHC_TYPENATS, gHC_TYPEERROR) #endif #endif -import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (CtLoc (..), initialSubGoalDepth) +import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat import GHC.Tc.Types.Origin as GHC.TypeLits.Presburger.Compat (CtOrigin (..)) import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat ( evByFiat, @@ -37,13 +39,17 @@ import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..)) import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon) import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (evCast) -import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo) +import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo, Role(..)) +import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (Coercion) import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (UnivCoProvenance(..)) import GHC.Core.DataCon as GHC.TypeLits.Presburger.Compat (dataConWrapId) #else import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) #endif -#if MIN_VERSION_ghc(9,4,1) +#if MIN_VERSION_ghc(9,12,1) +-- mkBaseModule is not available in GHC 9.12.1+ +import GHC.Core.Reduction (reductionReducedType) +#elif MIN_VERSION_ghc(9,4,1) import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule) import GHC.Core.Reduction (reductionReducedType) #else @@ -74,7 +80,9 @@ import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule) #if MIN_VERSION_ghc(9,2,0) import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) +#if !MIN_VERSION_ghc(9,12,1) import GHC.Builtin.Names (mkBaseModule) +#endif #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) import GHC.Driver.Session (unitState, unitDatabases) @@ -182,6 +190,15 @@ #if !MIN_VERSION_ghc(9,4,1) type TcPluginSolveResult = TcPluginResult +#endif + +-- mkUnivCo API compatibility +#if MIN_VERSION_ghc(9,12,1) +mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion +mkUnivCo' prov role ty1 ty2 = mkUnivCo prov [] role ty1 ty2 +#else +mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion +mkUnivCo' = mkUnivCo #endif #if MIN_VERSION_ghc(9,10,1) 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 @@ -362,7 +362,7 @@ | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd , con `elem` assertTy given = Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast` - mkUnivCo + mkUnivCo' (PluginProv $ "ghc-typelits-presburger: extractProof") Representational (mkTyConTy (cTupleTyCon 0))