ghc-typelits-natnormalise 0.9.2 → 0.9.3

raw patch · 5 files changed

+46/−10 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• ghc-typelits-natnormalise.cabal +1/−1
• src/GHC/TypeLits/Normalise/Unify.hs +16/−3
• tests/ErrorTests.hs +24/−6
• tests/Tests.hs +1/−0

@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.9.3 *December 2nd 2025*+* Fixes [#114](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Poor error message in plugin version 0.8 and higher+* Fixes [#113](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Wanted contraints rewrites to itself, leading to infinite solver iterations+ ## 0.9.2 *December 2nd 2025* * Fixes [#108](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/108) Type error after plugin update * Fixes [#111](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/111) Exception for unifying under non-injective type families

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

@@ -9,6 +9,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash                  #-} {-# LANGUAGE RecordWildCards            #-}+{-# LANGUAGE ViewPatterns               #-} {-# LANGUAGE TupleSections              #-}  {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}@@ -52,7 +53,7 @@ import Data.Either   ( partitionEithers ) import Data.List-  ( (\\), intersect, nub )+  ( (\\), intersect, nub, sort ) import Data.Maybe   ( fromMaybe, mapMaybe, isJust ) import GHC.Base@@ -306,7 +307,15 @@     else Just (x', y', isLE)   where     S ps = subtractIneq ineq-    (neg, pos) = partitionEithers $ map classify ps+    -- We need to sort the products in order to retain our canonical form,+    -- not sorting would result in the following rewrite:+    --+    -- 2 * a + b ~ 5  ==>+    -- 5 + -1 * b + -2 * a ==>+    -- b + 2 * a ~ 5+    --+    -- Which lead to issue #113+    (sort -> neg, sort -> pos) = partitionEithers $ map classify ps     (x', y') =       if isLE       then ( S neg, S pos )@@ -606,7 +615,11 @@           | otherwise = ps2'     psx = intersect ps1 ps2 -unifiers' _ s1 s2 = return [UnifyItem s1 s2]+-- Don't generate unify items where one of the sides is an empty sum (i.e.) zero+-- Doing so leads to poor error messages, see #114+unifiers' _ (S []) _ = return []+unifiers' _ _ (S []) = return []+unifiers' _ s1 s2    = return [UnifyItem s1 s2]  -- | Try to match the two expressions term-by-term. -- If this produces a **single unifier**, then we succeed.

@@ -105,16 +105,16 @@  testProxy4Errors = #if __GLASGOW_HASKELL__ >= 914-  ["Expected: Proxy ((2 * 0) + 4)"+  ["Expected: Proxy ((2 * y0) + 4)"   ,"  Actual: Proxy 2"   ] #elif __GLASGOW_HASKELL__ >= 900   ["Expected: Proxy 2 -> ()"-  ,"  Actual: Proxy ((2 * 0) + 4) -> ()"+  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"   ] #else   ["Expected type: Proxy 2 -> ()"-  ,"Actual type: Proxy ((2 * 0) + 4) -> ()"+  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"   ] #endif @@ -123,16 +123,16 @@  testProxy5Errors = #if __GLASGOW_HASKELL__ >= 914-  ["Expected: Proxy ((2 * y0) + 4)"+  ["Expected: Proxy ((2 * y1) + 4)"   ,"  Actual: Proxy 7"   ] #elif __GLASGOW_HASKELL__ >= 900   ["Expected: Proxy 7 -> ()"-  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"+  ,"  Actual: Proxy ((2 * y1) + 4) -> ()"   ] #else   ["Expected type: Proxy 7 -> ()"-  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+  ,"Actual type: Proxy ((2 * y1) + 4) -> ()"   ] #endif @@ -590,5 +590,23 @@            then litE $ stringL "‘Drop’ is a non-injective type family"            else litE $ stringL "`Drop' is a non-injective type family"      )+  ]+#endif++t113 :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5+t113 _ _ = id++t113_errors =+#if __GLASGOW_HASKELL__ >= 914+  ["Expected: Proxy 5"+  ,"  Actual: Proxy ((2 * a) + b)"+  ]+#elif __GLASGOW_HASKELL__ >= 900+  ["Expected: Proxy ((2 * a) + b) -> Proxy 5"+  ,"  Actual: Proxy 5 -> Proxy 5"+  ]+#else+  ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"+  ,"Actual type: Proxy 5 -> Proxy 5"   ] #endif

@@ -640,6 +640,7 @@         testProxy15 (Proxy :: Proxy 1) `throws` testProxy15Errors     , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors     , testCase "Do not unify in non-injective positions" $ t99 `throws` t99_errors+    , testCase "Do not rewrite constraint to itself" $ t113 `throws` t113_errors     , testGroup "Inequality"       [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors       , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors