ghc-typelits-extra 0.5.2 → 0.5.3

raw patch · 9 files changed

+670/−382 lines, 9 filesdep +directorydep +filepathdep +interpolatedep ~basedep ~ghc-primdep ~ghc-typelits-knownnatnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: directory, filepath, interpolate, process, temporary

Dependency ranges changed: base, ghc-prim, ghc-typelits-knownnat, ghc-typelits-natnormalise

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• ghc-typelits-extra.cabal +17/−10
• src/GHC/TypeLits/Extra.hs +0/−11
• src/GHC/TypeLits/Extra/Solver.hs +2/−2
• src/GHC/TypeLits/Extra/Solver/Operations.hs +1/−1
• tests/ErrorTests.hs +0/−305
• tests/Main.hs +18/−53
• tests/ShouldError.hs +574/−0
• tests/ShouldError/Tasty.hs +53/−0

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.5.3 *March 19th 2026*+* Do not require equality to unit constraint for wanted InEqs for `CLog` and `CLogWZ`.+* Fix wrong reification from `CLogWZ` to `CLog` causing GHC panic. [#71](https://github.com/clash-lang/ghc-typelits-extra/issues/71)+* Do not emit new wanteds for given `CLogWZ ~ CLog` equalities. [#73](https://github.com/clash-lang/ghc-typelits-extra/issues/73)+ # 0.5.2 *December 3rd 2025* * Add `CLogWZ`, an extension of 'CLog', which returns the additional third argument in case the second argument is zero * Add rewrite rules for `Min`, `Max`, `FLog`, `CLog`, and `Log`

@@ -1,6 +1,6 @@ cabal-version:       3.0 name:                ghc-typelits-extra-version:             0.5.2+version:             0.5.3 synopsis:            Additional type-level operations on GHC.TypeLits.Nat description:   Additional type-level operations on @GHC.TypeLits.Nat@:@@ -47,7 +47,7 @@                                  2017-2018, QBayLogic B.V. category:            Type System build-type:          Simple-extra-source-files:  README.md+extra-doc-files:     README.md                      CHANGELOG.md tested-with:         GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,                      GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.3,@@ -73,10 +73,10 @@   build-depends:       base                      >= 4.8      && <5,                        containers                >= 0.5.7.1  && <0.9,                        ghc                       >= 8.8      && <9.17,-                       ghc-prim                  >= 0.5      && <1.0,+                       ghc-prim                  >= 0.5      && <1,                        ghc-tcplugin-api          >= 0.18.1.0 && <0.19,                        ghc-typelits-knownnat     >= 0.7.2    && <0.9,-                       ghc-typelits-natnormalise >= 0.9.3    && <0.10,+                       ghc-typelits-natnormalise >= 0.9.5    && <0.10,                        transformers              >= 0.4.2.0  && <0.7,                        template-haskell          >= 2.15     && <2.25   if impl(ghc >= 9.0.0)@@ -125,16 +125,23 @@ test-suite test-ghc-typelits-extra   type:                exitcode-stdio-1.0   main-is:             Main.hs-  Other-Modules:       ErrorTests-  build-depends:       base                      >= 4.8 && <5,+  Other-Modules:       ShouldError+                       ShouldError.Tasty+  build-depends:       base,+                       directory,+                       filepath,                        ghc-typelits-extra,-                       ghc-typelits-knownnat     >= 0.8.2,-                       ghc-typelits-natnormalise >= 0.9.0,+                       ghc-typelits-knownnat,+                       ghc-typelits-natnormalise,+                       process,+                       interpolate,                        tasty                     >= 0.10,-                       tasty-hunit               >= 0.9+                       tasty-hunit               >= 0.9,+                       temporary   hs-source-dirs:      tests+  ghc-options:         -Wall   default-language:    Haskell2010   other-extensions:    DataKinds                        TypeOperators   if flag(deverror)-    ghc-options:       -dcore-lint+    ghc-options:       -Werror -dcore-lint

@@ -84,9 +84,6 @@ import Data.Proxy             (Proxy (..)) import Data.Type.Bool         (If) import GHC.Base               (Int#,isTrue#,(==#),(+#))-#if MIN_VERSION_ghc(9,4,0)-import GHC.Base               (Constraint)-#endif import GHC.Integer.Logarithms (integerLogBase#) #if MIN_VERSION_ghc(8,2,0) import GHC.Magic              (noinline)@@ -185,11 +182,7 @@ type family CLog (base :: Nat) (value :: Nat) :: Nat where   CLog 2 1 = 0 -- Additional equations are provided by the custom solver -#if MIN_VERSION_ghc(9,4,0)-instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where-#else instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where-#endif   natSing2 = let x  = natVal (Proxy @x)                  y  = natVal (Proxy @y)                  z1 = integerLogBase# x y@@ -204,11 +197,7 @@   CLogWZ _ 0 z = z   CLogWZ b v _ = CLog b v -#if MIN_VERSION_ghc(9,4,0)-instance (KnownNat x, KnownNat y, KnownNat z, (2 <= x) ~ (() :: Constraint)) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where-#else instance (KnownNat x, KnownNat y, KnownNat z, 2 <= x) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where-#endif   natSing3 = let x  = natVal (Proxy @x)                  y  = natVal (Proxy @y)                  z  = natVal (Proxy @z)

@@ -220,13 +220,13 @@                  (CLog a' b', CLogWZ a b _) | a == a' && b == b' -> Just b                  _ -> Nothing       case wz of-        Just x -> do+        Just x | isWantedCt ct -> do           let x' = reifyEOP defs x               one = reifyEOP defs (I 1)           ev <- newWanted (ctLoc ct) $ mkLEqNat (ordTyCons defs) one x'           let newCt = mkNonCanonical ev           simples (fmap (,ct) evM:evs) (newCt:news) eqs'-        Nothing -> do+        _ -> do           ur <- unifyExtra ct u v           tcPluginTrace "unifyExtra result" (ppr ur)           case ur of

@@ -119,7 +119,7 @@   Div x y      -> mkTyConApp (divTyCon defs)  $ reifyEOP defs <$> [x, y]   Mod x y      -> mkTyConApp (modTyCon defs)  $ reifyEOP defs <$> [x, y]   CLog x y     -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y]-  CLogWZ x y z -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y, z]+  CLogWZ x y z -> mkTyConApp (clogWZTyCon defs) $ reifyEOP defs <$> [x, y, z]   FLog x y     -> mkTyConApp (flogTyCon defs) $ reifyEOP defs <$> [x, y]   Log x y      -> mkTyConApp (logTyCon defs)  $ reifyEOP defs <$> [x, y]   GCD x y      -> mkTyConApp (gcdTyCon defs)  $ reifyEOP defs <$> [x, y]

@@ -1,305 +0,0 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}-#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif-{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}--module ErrorTests where--import Data.Proxy-import GHC.TypeLits-import GHC.TypeLits.Extra-#if __GLASGOW_HASKELL__ >= 901-import qualified Data.Type.Ord-#endif--testFail1 :: Proxy (GCD 6 8) -> Proxy 4-testFail1 = id--testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))-testFail2 = id--testFail3 :: Proxy (CLog 3 10) -> Proxy 2-testFail3 = id--testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))-testFail4 = id--testFail5 :: Proxy (CLog 0 4) -> Proxy 100-testFail5 = id--testFail6 :: Proxy (CLog 1 4) -> Proxy 100-testFail6 = id--testFail7 :: Proxy (CLog 4 0) -> Proxy 0-testFail7 = id--testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y-testFail8 = id--testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y-testFail9 = id--testFail10 :: Integer-testFail10 = natVal (Proxy :: Proxy (CLog 1 4))--testFail11 :: Integer-testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))--testFail12 :: Proxy (Div 4 0) -> Proxy 4-testFail12 = id--testFail13 :: Proxy (Mod 4 0) -> Proxy 4-testFail13 = id--testFail14 :: Proxy (FLog 0 4) -> Proxy 100-testFail14 = id--testFail15 :: Proxy (FLog 1 4) -> Proxy 100-testFail15 = id--testFail16 :: Proxy (FLog 4 0) -> Proxy 0-testFail16 = id--testFail17 :: Proxy (LCM 6 8) -> Proxy 48-testFail17 = id--testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))-testFail18 = id--testFail19 :: Integer-testFail19 = natVal (Proxy :: Proxy (Log 3 0))--testFail20 :: Integer-testFail20 = natVal (Proxy :: Proxy (Log 3 10))--testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a-testFail21 _ _ = id--testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)-testFail22 _ _ = id--testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()-testFail23' _ _ = ()--testFail23 :: ()-testFail23 = testFail23' (Proxy @18) (Proxy @3)--testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True-testFail24 _ _ _ = id--testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True-testFail25 _ _ = id---- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.-testFail26' :: ((x <=? n) ~ True)  => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n-testFail26' _ _ _ = id--testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)--testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True-testFail27 _ = id--testFail1Errors =-  ["Proxy (GCD 6 8) -> Proxy 4"-  ,"Proxy 4 -> Proxy 4"-  ]--testFail2Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"-  ,"Proxy (2 + x) -> Proxy (2 + x)"-  ]-#elif __GLASGOW_HASKELL__ >= 900-  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"-  ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"-  ]-#else-  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"-  ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"-  ]-#endif--testFail3Errors =-  ["Proxy (CLog 3 10) -> Proxy 2"-  ,"Proxy 2 -> Proxy 2"-  ]--testFail4Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"-  ,"Proxy (3 + x) -> Proxy (3 + x)"-  ]-#elif __GLASGOW_HASKELL__ >= 900-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"-  ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"-  ]-#else-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"-  ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"-  ]-#endif--testFail5Errors =-  ["Proxy (CLog 0 4) -> Proxy 100"-  ,"Proxy 100 -> Proxy 100"-  ]--testFail6Errors =-  ["Proxy (CLog 1 4) -> Proxy 100"-  ,"Proxy 100 -> Proxy 100"-  ]--testFail7Errors =-  ["Proxy (CLog 4 0) -> Proxy 0"-  ,"Proxy 0 -> Proxy 0"-  ]--testFail8Errors =-  ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"-  ,"Proxy y -> Proxy y"-  ]--testFail9Errors =-  ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"-  ,"Proxy y -> Proxy y"-  ]--testFail10Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Cannot satisfy: 2 <= 1"]-#else-  ["Couldn't match type ‘'False’ with ‘'True’"]-#endif--testFail11Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Cannot satisfy: 2 <= 1"]-#else-  ["Couldn't match type ‘'False` with ‘'True’"]-#endif--testFail12Errors =-  ["Proxy (Div 4 0) -> Proxy 4"-  ,"Proxy 4 -> Proxy 4"-  ]--testFail13Errors =-  ["Proxy (Mod 4 0) -> Proxy 4"-  ,"Proxy 4 -> Proxy 4"-  ]--testFail14Errors =-  ["Proxy (FLog 0 4) -> Proxy 100"-  ,"Proxy 100 -> Proxy 100"-  ]--testFail15Errors =-  ["Proxy (FLog 1 4) -> Proxy 100"-  ,"Proxy 100 -> Proxy 100"-  ]--testFail16Errors =-  ["Proxy (FLog 4 0) -> Proxy 0"-  ,"Proxy 0 -> Proxy 0"-  ]--testFail17Errors =-  ["Proxy (LCM 6 8) -> Proxy 48"-  ,"Proxy 48 -> Proxy 48"-  ]--testFail18Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"-  ,"Proxy (24 + x) -> Proxy (24 + x)"-  ]-#elif __GLASGOW_HASKELL__ >= 900-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"-  ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"-  ]-#else-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"-  ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"-  ]-#endif--testFail19Errors =-#if __GLASGOW_HASKELL__ >= 900-  ["Couldn't match type: FLog 3 0"-  ,"               with: CLog 3 0"]-#else-  ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]-#endif--testFail20Errors =-#if __GLASGOW_HASKELL__ >= 904-  ["Couldn't match type ‘2’ with ‘3’"]-#elif __GLASGOW_HASKELL__ >= 900-  ["Couldn't match type: FLog 3 10"-  ,"               with: CLog 3 10"]-#else-  ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]-#endif--testFail21Errors =-  ["Proxy (Min a (a * b)) -> Proxy a"-  ,"Proxy a -> Proxy a"-  ]--testFail22Errors =-#if __GLASGOW_HASKELL__ >= 900-  ["Proxy (Max a (a * b)) -> Proxy (a * b)"-  ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]-#else-  ["Proxy (Max a (a * b)) -> Proxy (a * b)"-  ,"Proxy (a * b) -> Proxy (a * b)"]-#endif--testFail23Errors =-#if __GLASGOW_HASKELL__ >= 804-  ["Couldn't match type ‘'True’ with ‘'False’"]-#else-  ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]-#endif--testFail24Errors =-#if __GLASGOW_HASKELL__ >= 902-  ["Couldn't match type ‘Data.Type.Ord.OrdCond"-  ,"(CmpNat z (Max x y)) 'True 'True 'False’"-  ,"with ‘'True’"]-#else-  ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]-#endif--testFail25Errors =-#if __GLASGOW_HASKELL__ >= 902-  ["Couldn't match type ‘Data.Type.Ord.OrdCond"-  ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"-  ,"with ‘'True’"]-#else-  ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]-#endif--testFail26Errors =-#if __GLASGOW_HASKELL__ >= 906-  ["Could not deduce ‘Max x y ~ n’"-  ,"from the context: (x <=? n) ~ True"-  ]-#elif __GLASGOW_HASKELL__ <= 902-  ["Could not deduce: Max x y ~ n"-  ,"from the context: (x <=? n) ~ 'True"-  ]-#else-  ["Could not deduce (Max x y ~ n)"-  ,"from the context: (x <=? n) ~ 'True"-  ]-#endif--testFail27Errors =-  ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"-  ,"Proxy 'True -> Proxy 'True"-  ]

@@ -12,19 +12,22 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} #endif +-- Even though binders are not used, they're compiled and that's what we're after.+{-# OPTIONS_GHC -Wno-unused-top-binds #-} -import Data.List (isInfixOf)+-- Only applies to old GHCs.+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ import Data.Proxy-import Data.Type.Bool-import Control.Exception+import Data.Type.Equality import Test.Tasty import Test.Tasty.HUnit -import ErrorTests- import GHC.TypeLits import GHC.TypeLits.Extra +import qualified ShouldError+ test1 :: Proxy (GCD 6 8) -> Proxy 2 test1 = id @@ -275,6 +278,12 @@ test69 :: 1 <= n => Proxy n -> Proxy (CLogWZ 2 n 0) -> Proxy (CLog 2 n) test69 _ = id +-- Regression test for: https://github.com/clash-lang/ghc-typelits-extra/issues/73+test70 :: (CLog 2 n ~ CLogWZ 2 n 0) => Proxy n -> Proxy n+test70 _ =+  case (Refl :: Max (n + 1) 1 :~: (1 + n)) of+    Refl -> Proxy+ main :: IO () main = defaultMain tests @@ -485,53 +494,9 @@     , testCase "1 <= n => CLogWZ 2 n 0 ~ CLog 2 n" $       show (test69 (Proxy :: Proxy 3) Proxy) @?=       "Proxy"-    ]-  , testGroup "errors"-    [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors-    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors-    , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors-    , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors-    , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors-    , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors-    , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors-    , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors-    , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors-    , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors-    , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors-    , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors-    , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors-    , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors-    , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors-    , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors-    , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors-    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors-    , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors-    , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors-    , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors-    , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors-    , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors-    , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors-    , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors-    , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors-    , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors+    , testCase "CLogWZ ~ CLog given does not loop" $+      show (test70 (Proxy :: Proxy 1)) @?=+      "Proxy"     ]+  , ShouldError.tests   ]---- | Assert that evaluation of the first argument (to WHNF) will throw--- an exception whose string representation contains the given--- substrings.-throws :: a -> [String] -> Assertion-throws v xs = do-  result <- try (evaluate v)-  case result of-    Right _ -> assertFailure "No exception!"-    Left (TypeError msg) ->-      if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs-         then return ()-         else assertFailure msg---- The kind and amount of quotes in GHC error messages changes depending on--- whether or not our locale supports unicode.--- Remove the problematic characters to enable comparison of errors.-removeProblemChars = filter (`notElem` problemChars)-  where problemChars = "‘’`'"

@@ -0,0 +1,574 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}++module ShouldError (tests) where++import Data.String.Interpolate (i)+import ShouldError.Tasty (assertCompileError)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase)++tests :: TestTree+tests = testGroup "ShouldError"+    [ test1+    , test2+    , test3+    , test4+    , test5+    , test6+    , test7+    , test8+    , test9+    , test10+    , test11+    , test12+    , test13+    , test14+    , test15+    , test16+    , test17+    , test18+    , test19+    , test20+    , test21+    , test22+    , test23+    , test24+    , test25+    , test26+    , test27+    , test28+    ]++preamble :: String+preamble = [i|+import Data.Proxy+import GHC.TypeLits+import GHC.TypeLits.Extra+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (GCD 6 8) -> Proxy 4+test = id+|]++expected1 :: [String]+expected1 =+  ["Proxy (GCD 6 8) -> Proxy 4"+  ,"Proxy 4 -> Proxy 4"+  ]++test1 :: TestTree+test1 = testCase "GCD 6 8 /~ 4" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+test :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 904+  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+  ,"Proxy (2 + x) -> Proxy (2 + x)"+  ]+#elif __GLASGOW_HASKELL__ >= 900+  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+  ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"+  ]+#else+  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+  ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"+  ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+test :: Proxy (CLog 3 10) -> Proxy 2+test = id+|]++expected3 :: [String]+expected3 =+  ["Proxy (CLog 3 10) -> Proxy 2"+  ,"Proxy 2 -> Proxy 2"+  ]++test3 :: TestTree+test3 = testCase "CLog 3 10 /~ 2" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+test :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))+test = id+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 904+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+  ,"Proxy (3 + x) -> Proxy (3 + x)"+  ]+#elif __GLASGOW_HASKELL__ >= 900+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+  ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"+  ]+#else+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+  ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"+  ]+#endif++test4 :: TestTree+test4 = testCase "CLog 3 10 + x /~ x + CLog 2 10" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+test :: Proxy (CLog 0 4) -> Proxy 100+test = id+|]++expected5 :: [String]+expected5 =+  ["Proxy (CLog 0 4) -> Proxy 100"+  ,"Proxy 100 -> Proxy 100"+  ]++test5 :: TestTree+test5 = testCase "CLog 0 4 /~ 100" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+test :: Proxy (CLog 1 4) -> Proxy 100+test = id+|]++expected6 :: [String]+expected6 =+  ["Proxy (CLog 1 4) -> Proxy 100"+  ,"Proxy 100 -> Proxy 100"+  ]++test6 :: TestTree+test6 = testCase "CLog 1 4 /~ 100" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy (CLog 4 0) -> Proxy 0+test = id+|]++expected7 :: [String]+expected7 =+  ["Proxy (CLog 4 0) -> Proxy 0"+  ,"Proxy 0 -> Proxy 0"+  ]++test7 :: TestTree+test7 = testCase "CLog 4 0 /~ 0" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+test :: Proxy (CLog 1 (1^y)) -> Proxy y+test = id+|]++expected8 :: [String]+expected8 =+  ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"+  ,"Proxy y -> Proxy y"+  ]++test8 :: TestTree+test8 = testCase "CLog 1 (1^y) /~ y" $ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+test :: Proxy (CLog 0 (0^y)) -> Proxy y+test = id+|]++expected9 :: [String]+expected9 =+  ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"+  ,"Proxy y -> Proxy y"+  ]++test9 :: TestTree+test9 = testCase "CLog 0 (0^y) /~ y" $ assertCompileError source9 expected9++source10 :: String+source10 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (CLog 1 4))+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 904+  ["Cannot satisfy: 2 <= 1"]+#else+  ["Couldn't match type ''False' with ''True'"]+#endif++test10 :: TestTree+test10 = testCase "No instance (KnownNat (CLog 1 4))" $ assertCompileError source10 expected10++source11 :: String+source11 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))+|]++expected11 :: [String]+expected11 =+#if __GLASGOW_HASKELL__ >= 904+  ["Cannot satisfy: 2 <= 1"]+#else+  ["Couldn't match type ''False` with ''True'"]+#endif++test11 :: TestTree+test11 = testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ assertCompileError source11 expected11++source12 :: String+source12 = preamble <> [i|+test :: Proxy (Div 4 0) -> Proxy 4+test = id+|]++expected12 :: [String]+expected12 =+  ["Proxy (Div 4 0) -> Proxy 4"+  ,"Proxy 4 -> Proxy 4"+  ]++test12 :: TestTree+test12 = testCase "Div 4 0 /~ 4" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> [i|+test :: Proxy (Mod 4 0) -> Proxy 4+test = id+|]++expected13 :: [String]+expected13 =+  ["Proxy (Mod 4 0) -> Proxy 4"+  ,"Proxy 4 -> Proxy 4"+  ]++test13 :: TestTree+test13 = testCase "Mod 4 0 /~ 4" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> [i|+test :: Proxy (FLog 0 4) -> Proxy 100+test = id+|]++expected14 :: [String]+expected14 =+  ["Proxy (FLog 0 4) -> Proxy 100"+  ,"Proxy 100 -> Proxy 100"+  ]++test14 :: TestTree+test14 = testCase "FLog 0 4 /~ 100" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> [i|+test :: Proxy (FLog 1 4) -> Proxy 100+test = id+|]++expected15 :: [String]+expected15 =+  ["Proxy (FLog 1 4) -> Proxy 100"+  ,"Proxy 100 -> Proxy 100"+  ]++test15 :: TestTree+test15 = testCase "FLog 1 4 /~ 100" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> [i|+test :: Proxy (FLog 4 0) -> Proxy 0+test = id+|]++expected16 :: [String]+expected16 =+  ["Proxy (FLog 4 0) -> Proxy 0"+  ,"Proxy 0 -> Proxy 0"+  ]++test16 :: TestTree+test16 = testCase "FLog 4 0 /~ 0" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> [i|+test :: Proxy (LCM 6 8) -> Proxy 48+test = id+|]++expected17 :: [String]+expected17 =+  ["Proxy (LCM 6 8) -> Proxy 48"+  ,"Proxy 48 -> Proxy 48"+  ]++test17 :: TestTree+test17 = testCase "LCM 6 8 /~ 48" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+test :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))+test = id+|]++expected18 :: [String]+expected18 =+#if __GLASGOW_HASKELL__ >= 904+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+  ,"Proxy (24 + x) -> Proxy (24 + x)"+  ]+#elif __GLASGOW_HASKELL__ >= 900+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+  ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"+  ]+#else+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"+  ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"+  ]+#endif++test18 :: TestTree+test18 = testCase "LCM 6 8 + x /~ x + LCM 6 9" $ assertCompileError source18 expected18++source19 :: String+source19 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 0))+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 900+  ["Couldn't match type: FLog 3 0"+  ,"               with: CLog 3 0"]+#else+  ["Couldn't match type 'FLog 3 0' with 'CLog 3 0'"]+#endif++test19 :: TestTree+test19 = testCase "No instance (KnownNat (Log 3 0))" $ assertCompileError source19 expected19++source20 :: String+source20 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test :: Integer+test = natVal (Proxy :: Proxy (Log 3 10))+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+  ["Couldn't match type '2' with '3'"]+#elif __GLASGOW_HASKELL__ >= 900+  ["Couldn't match type: FLog 3 10"+  ,"               with: CLog 3 10"]+#else+  ["Couldn't match type 'FLog 3 10' with 'CLog 3 10'"]+#endif++test20 :: TestTree+test20 = testCase "No instance (KnownNat (Log 3 10))" $ assertCompileError source20 expected20++source21 :: String+source21 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Min a (a * b)) -> Proxy a+test _ _ = id+|]++expected21 :: [String]+expected21 =+  ["Proxy (Min a (a * b)) -> Proxy a"+  ,"Proxy a -> Proxy a"+  ]++test21 :: TestTree+test21 = testCase "Min a (a*b) /~ a" $ assertCompileError source21 expected21++source22 :: String+source22 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy (Max a (a * b)) -> Proxy (a * b)+test _ _ = id+|]++expected22 :: [String]+expected22 =+#if __GLASGOW_HASKELL__ >= 900+  ["Proxy (Max a (a * b)) -> Proxy (a * b)"+  ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]+#else+  ["Proxy (Max a (a * b)) -> Proxy (a * b)"+  ,"Proxy (a * b) -> Proxy (a * b)"]+#endif++test22 :: TestTree+test22 = testCase "Max a (a*b) /~ (a*b)" $ assertCompileError source22 expected22++source23 :: String+source23 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|+test' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()+test' _ _ = ()++test :: ()+test = test' (Proxy @18) (Proxy @3)+|]++expected23 :: [String]+expected23 =+#if __GLASGOW_HASKELL__ >= 804+  ["Couldn't match type ''True' with ''False'"]+#else+  ["Couldn't match type '1 <=? Div 18 3' with ''False'"]+#endif++test23 :: TestTree+test23 = testCase "(1 <=? Div 18 3) ~ False" $ assertCompileError source23 expected23++source24 :: String+source24 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True+test _ _ _ = id+|]++expected24 :: [String]+expected24 =+#if __GLASGOW_HASKELL__ >= 902+  ["Couldn't match type 'Data.Type.Ord.OrdCond"+  ,"(CmpNat z (Max x y)) 'True 'True 'False'"+  ,"with ''True'"]+#else+  ["Couldn't match type 'z <=? Max x y' with ''True'"]+#endif++test24 :: TestTree+test24 = testCase "(z <=? Max x y) /~ True" $ assertCompileError source24 expected24++source25 :: String+source25 = [i|+{-# LANGUAGE CPP #-}+|] <> preamble <> [i|+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif++test :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True+test _ _ = id+|]++expected25 :: [String]+expected25 =+#if __GLASGOW_HASKELL__ >= 902+  ["Couldn't match type 'Data.Type.Ord.OrdCond"+  ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False'"+  ,"with ''True'"]+#else+  ["Couldn't match type '(x + 1) <=? Max x y' with ''True'"]+#endif++test25 :: TestTree+test25 = testCase "(x+1 <=? Max x y) /~ True" $ assertCompileError source25 expected25++source26 :: String+source26 = [i|+{-# LANGUAGE TypeApplications #-}+|] <> preamble <> [i|++-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.+test' :: ((x <=? n) ~ True)  => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n+test' _ _ _ = id++test = test' (Proxy @4) (Proxy @6) (Proxy @6)+|]++expected26 :: [String]+expected26 =+#if __GLASGOW_HASKELL__ >= 906+  ["Could not deduce 'Max x y ~ n'"+  ,"from the context: (x <=? n) ~ True"+  ]+#elif __GLASGOW_HASKELL__ <= 902+  ["Could not deduce: Max x y ~ n"+  ,"from the context: (x <=? n) ~ 'True"+  ]+#else+  ["Could not deduce (Max x y ~ n)"+  ,"from the context: (x <=? n) ~ 'True"+  ]+#endif++test26 :: TestTree+test26 = testCase "(x <= n) /=> (Max x y) ~ n" $ assertCompileError source26 expected26++source27 :: String+source27 = preamble <> [i|+test :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True+test _ = id+|]++expected27 :: [String]+expected27 =+  ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"+  ,"Proxy 'True -> Proxy 'True"+  ]++test27 :: TestTree+test27 = testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ assertCompileError source27 expected27++source28 :: String+source28 = [i|+{-# LANGUAGE KindSignatures #-}+|] <> preamble <> [i|+type Size (n :: Nat) = Max 0 (CLogWZ 2 n 0)++pack :: Proxy n -> Proxy (Size n)+pack _ = Proxy++repro :: Proxy (Size 1)+repro = pack (undefined :: Proxy (n :: Nat))+|]++expected28 :: [String]+expected28 =+  ["CLogWZ 2 n"+  ,"ambiguous"+  ]++test28 :: TestTree+test28 = testCase "CLogWZ reify with Max 0 (type synonym) doesn't panic" $+  assertCompileError source28 expected28

@@ -0,0 +1,53 @@+{-# LANGUAGE CPP #-}++module ShouldError.Tasty where++import Data.List (isInfixOf)+import Data.Maybe (fromMaybe)+import System.Environment (lookupEnv)+import System.Exit+import System.IO+import System.IO.Temp+import System.Process+import Test.Tasty.HUnit++-- | Assert that a Haskell code snippet fails to compile with expected error messages+assertCompileError :: String -> [String] -> Assertion+assertCompileError source expectedErrors = do+  -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI)+  --      isn't set and the test suite is compiled with a GHC compiler other than the+  --      system's default.+  hc <- fromMaybe "ghc" <$> lookupEnv "HC"+  withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do+    hPutStr tempHandle source+    hClose tempHandle+    (exitCode, _, stderrOutput) <- readProcessWithExitCode hc+      [ "-XCPP"+      , "-XDataKinds"+      , "-XTypeOperators"+      , "-XTypeApplications"+      , "-XTypeFamilies"+      , "-XNoStarIsType"+      , "-fno-code"+      , "-fplugin", "GHC.TypeLits.Normalise"+      , "-fplugin", "GHC.TypeLits.KnownNat.Solver"+      , "-fplugin", "GHC.TypeLits.Extra.Solver"+      , tempFile+      ] ""+    case exitCode of+      ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded"+      ExitFailure _ ->+        let cleanedStderr = removeProblemChars stderrOutput+            cleanedExpected = map removeProblemChars expectedErrors+        in if all (`isInfixOf` cleanedStderr) cleanedExpected+           then return ()+           else assertFailure $ "Error message mismatch:\n" +++                               "Expected substrings: " ++ show expectedErrors ++ "\n" +++                               "Actual output:\n" ++ stderrOutput++-- | Remove problematic characters that vary depending on locale+-- The kind and amount of quotes in GHC error messages changes depending on+-- whether or not our locale supports unicode.+removeProblemChars :: String -> String+removeProblemChars = filter (`notElem` problemChars)+  where problemChars = "‘’`'"