ghc-typelits-natnormalise 0.7.5 → 0.7.6

raw patch · 4 files changed

+8/−11 lines, 4 filesdep ~ghc-bignumPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc-bignum

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• ghc-typelits-natnormalise.cabal +1/−1
• src/GHC/TypeLits/Normalise.hs +3/−1
• src/GHC/TypeLits/Normalise/Unify.hs +0/−9

@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.7.6 *June 20th 2021*+* Do not vacuously solve `forall a b . 1 <=? a^b ~ True`+* Do not solve constraints within `KnownNat`, leave that to https://hackage.haskell.org/package/ghc-typelits-knonwnnat+ ## 0.7.5 *June 17th 2021* * Fixes [#52](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/50) Plugin doesn't solve inside arbitrary class constraints * Build on GHC 9.2.0.20210422

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.7.5+version:             0.7.6 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ and /inequalities/

@@ -192,6 +192,7 @@ import GHC.Builtin.Types.Literals (typeNatLeqTyCon) #endif import GHC.Core (Expr (..))+import GHC.Core.Class (className) import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo) import GHC.Core.Predicate   (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,@@ -243,6 +244,7 @@ import TysWiredIn (typeNatKind)  import Coercion   (CoercionHole, Role (..), mkUnivCo)+import Class      (className) import TcPluginM  (newCoercionHole, tcLookupClass, newEvVar) import TcRnTypes  (TcPlugin (..), TcPluginResult(..)) import TyCoRep    (UnivCoProvenance (..))@@ -521,7 +523,7 @@         -- No existing evidence found         Nothing -> case getClassPredTys_maybe pred' of           -- Are we trying to solve a class instance?-          Just _ -> do+          Just (cls,_) | className cls /= knownNatClassName -> do             -- Create new evidence binding for normalized class constraint             evVar <- newEvVar pred'             -- Bind the evidence to a new wanted normalized class constraint

@@ -656,15 +656,6 @@   if sN && pN      then isNatural (S [P ps])      else WriterT Nothing--- This is a quick hack, it determines that------ > a^b - 1------ is a natural number as long as 'a' and 'b' are natural numbers.--- This used to assert that:------ > (1 <=? a^b) ~ True-isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p]) -- We give up for all other products for now isNatural (S [P (C c:ps)]) = do   tell (Set.singleton c)