ghc-typelits-natnormalise 0.9.3 → 0.9.4
raw patch · 9 files changed
+792/−695 lines, 9 filesdep +interpolatedep +processdep +temporarydep −template-haskelldep ~ghc-tcplugin-apinew-uploaderPVP ok
version bump matches the API change (PVP)
Dependencies added: interpolate, process, temporary
Dependencies removed: template-haskell
Dependency ranges changed: ghc-tcplugin-api
API changes (from Hackage documentation)
Files
- CHANGELOG.md +8/−0
- ghc-typelits-natnormalise.cabal +10/−7
- src/GHC/TypeLits/Normalise.hs +33/−16
- src/GHC/TypeLits/Normalise/Compat.hs +1/−8
- src/GHC/TypeLits/Normalise/Unify.hs +5/−9
- tests/ErrorTests.hs +0/−612
- tests/ShouldError.hs +597/−0
- tests/ShouldError/Tasty.hs +58/−0
- tests/Tests.hs +80/−43
CHANGELOG.md view
@@ -1,5 +1,13 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## Unreleased++## 0.9.4 *March 19th 2026*+* Fixes [#116](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Compile-time loop when processing Given constraints.+* Fixes [#119](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/119) solving constraints involving type families applied to normalised Nat expressions (e.g. `Foo (a + b)`).+* Fixes [#120](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/120) stop emitting Assert (a <=? b) msg ~ (() :: Constraint) constraints+* Fixed regression [#124](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124) involving unification of summands.+ ## 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
ghc-typelits-natnormalise.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: ghc-typelits-natnormalise-version: 0.9.3+version: 0.9.4 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -46,7 +46,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.7, GHC == 9.8.4, GHC == 9.10.2,@@ -70,7 +70,7 @@ build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.9, ghc >=8.8.1 && <9.15,- ghc-tcplugin-api >=0.18.0 && <0.19,+ ghc-tcplugin-api >=0.18.2 && <0.19, transformers >=0.5.2.0 && < 0.7 if impl(ghc >= 9.0.0) build-depends: ghc-bignum >=1.0 && <1.5@@ -100,23 +100,26 @@ test-suite unit-tests type: exitcode-stdio-1.0 main-is: Tests.hs- Other-Modules: ErrorTests+ Other-Modules: ShouldError+ ShouldError.Tasty build-depends: base >=4.8 && <5, ghc-typelits-natnormalise,+ interpolate,+ process, tasty >= 0.10, tasty-hunit >= 0.9,- template-haskell >= 2.11.0.0+ temporary if impl(ghc >= 9.4) build-depends: ghc-prim >= 0.9 hs-source-dirs: tests+ ghc-options: -Wall default-language: Haskell2010 other-extensions: DataKinds GADTs KindSignatures NoImplicitPrelude- TemplateHaskell TypeFamilies TypeOperators ScopedTypeVariables if flag(deverror)- ghc-options: -dcore-lint+ ghc-options: -Werror -dcore-lint
src/GHC/TypeLits/Normalise.hs view
@@ -300,26 +300,43 @@ simplifyNats opts tcs [] $ concatMap (toNatEquality opts tcs givensTyConSubst) redGivens - -- Only enter actual new evidence into the solver loop, i.e. we could derive- -- a new given in our solver loop for which there already is existing evidence.- -- We have no use for two different proofs of the same fact.- let givensPreds = map (CType . ctEvPred . ctEvidence) givens- actuallyNewGivens =- filter ((`notElem` givensPreds) . CType . ctEvPred . ctEvidence) newGivens- -- For now, only admit improved givens in the form of `n ~ L`, where `n` is- -- a type variable and `L` is a numeric literal.- let simplNewGivens = filter- ( \case {EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2); _ -> False}- . classifyPredType- . ctEvPred- . ctEvidence- ) actuallyNewGivens+ -- Only add new Givens that are genuinely new, i.e. that GHC doesn't+ -- already know.+ --+ -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that+ -- the inert set in GHC is a /not necessarily idempotent/ terminating+ -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet),+ -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and+ -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116).+ let+ isSolvedGiven subst ct =+ case classifyPredType $ substTy subst (ctPred ct) of+ EqPred _rel t1 t2 -> t1 `eqType` t2+ _ -> False+ tyEqLit ct =+ case classifyPredType (ctPred ct) of+ EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2)+ _ -> False+ givensSubst = ctsSubst givens -- Computes the idempotent substitution from the Givens+ actuallyNewGivens =+ filter+ (\ ct ->+ tyEqLit ct+ -- For now, only admit improved Givens in the form of `n ~ L`,+ -- where `n` is a type variable and `L` is a numeric literal.+ &&+ not (isSolvedGiven givensSubst ct)+ -- Ensure this Given is genuinely new information to GHC, to+ -- avoid repeatedly emitting facts that GHC already knows,+ -- which can cause the typechecker to loop (#116).+ )+ newGivens tcPluginTrace "decideEqualSOP Givens }" $ vcat [ text "givens:" <+> ppr givens , text "simpls:" <+> ppr simplifiedWanteds , text "contra:" <+> ppr contradictions- , text "new:" <+> ppr simplNewGivens+ , text "new:" <+> ppr actuallyNewGivens ] return $ mkTcPluginSolveResult@@ -329,7 +346,7 @@ [] #endif [] -- no solved Givens- simplNewGivens+ actuallyNewGivens -- Solving phase. -- Solves in/equalities on Nats and simplifiable constraints
src/GHC/TypeLits/Normalise/Compat.hs view
@@ -140,14 +140,7 @@ -- | The constraint @(a <= b)@. mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType mkLEqNat tcs a b =-#if MIN_VERSION_ghc(9,3,0)- -- Starting from GHC 9.3, (a <= b) turns into 'Assert (a <=? b) msg'.- -- We prefer to emit 'Assert (a <=? b) msg ~ (() :: Constraint)',- -- in order to avoid creating an Irred constraint.- mkEqPredRole Nominal- (mkTyConApp (leqTyCon tcs) [natKind, a, b])- (mkTyConTy $ c0TyCon tcs)-#elif MIN_VERSION_ghc(9,1,0)+#if MIN_VERSION_ghc(9,1,0) mkTyConApp (leqTyCon tcs) [natKind, a, b] #else mkTyConApp (leqNatTyCon tcs) [a, b]
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -106,12 +106,7 @@ type CoreProduct = Product TyVar CType type CoreSymbol = Symbol TyVar CType --- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but--- only when the type is constructed out of:------ * literals--- * type variables--- * Applications of the arithmetic operators @(+,-,*,^)@+-- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion]) normaliseNat ty | Just (tc, xs) <- splitTyConApp_maybe ty@@ -143,7 +138,8 @@ (y', cos2) <- normaliseNat y return (normaliseExp x' y', cos1 ++ cos2) goTyConApp tc xs- = return (S [P [C (CType $ mkTyConApp tc xs)]], [])+ = do (xs', cos') <- fmap unzip (traverse normaliseSimplifyNat xs)+ return (S [P [C (CType (mkTyConApp tc xs'))]], concat cos') knownTyCons :: [TyCon] knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]@@ -592,6 +588,8 @@ -- -- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3]. unifiers' ct s1@(S ps1) s2@(S ps2)+ | not $ null psx+ = unifiers' ct (S ps1'') (S ps2'') | Just (s1',s2',_) <- simplifyIneq (s1, s2, True) = unifiers' ct s1' s2' | Just term_unifs <- termByTerm ct ps1 ps2@@ -604,8 +602,6 @@ | null psx , isGiven (ctEvidence ct) = unifiers'' ct (S ps1) (S ps2)- | not $ null psx- = unifiers' ct (S ps1'') (S ps2'') where ps1' = ps1 \\ psx ps2' = ps2 \\ psx
− tests/ErrorTests.hs
@@ -1,612 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances#-}--#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}-#endif--{-# OPTIONS_GHC -fdefer-type-errors #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}-module ErrorTests where--import Data.Proxy-import GHC.TypeLits-#if __GLASGOW_HASKELL__ >= 903-import GHC.Types-#endif--import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)-import Language.Haskell.TH (litE, stringL)-import Language.Haskell.TH.Syntax (runIO)-#if __GLASGOW_HASKELL__ >= 901-import qualified Data.Type.Ord-#endif--#if __GLASGOW_HASKELL__ >= 901-import qualified Data.Type.Ord-#endif--testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)-testProxy1 = id--testProxy1Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy (2 + x)"- ," Actual: Proxy (x + 1)"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy (x + 1) -> Proxy (2 + x)"- ," Actual: Proxy (x + 1) -> Proxy (x + 1)"- ]-#else- ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"- ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"- ]-#endif--type family GCD (x :: Nat) (y :: Nat) :: Nat-type instance GCD 6 8 = 2-type instance GCD 9 6 = 3--testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)-testProxy2 = id--testProxy2Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy (x + GCD 9 6)"- ," Actual: Proxy (2 + x)"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"- ," Actual: Proxy (2 + x) -> Proxy (2 + x)"- ]-#else- ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"- ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"- ]-#endif--proxyFun3 :: Proxy (x + x + x) -> ()-proxyFun3 = const ()--testProxy3 :: Proxy 8 -> ()-testProxy3 = proxyFun3--testProxy3Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy ((x0 + x0) + x0)"- ," Actual: Proxy 8"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 8 -> ()"- ," Actual: Proxy ((x0 + x0) + x0) -> ()"- ]-#else- ["Expected type: Proxy 8 -> ()"- ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"- ]-#endif--proxyFun4 :: Proxy ((2*y)+4) -> ()-proxyFun4 = const ()--testProxy4 :: Proxy 2 -> ()-testProxy4 = proxyFun4--testProxy4Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy ((2 * y0) + 4)"- ," Actual: Proxy 2"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 2 -> ()"- ," Actual: Proxy ((2 * y0) + 4) -> ()"- ]-#else- ["Expected type: Proxy 2 -> ()"- ,"Actual type: Proxy ((2 * y0) + 4) -> ()"- ]-#endif--testProxy5 :: Proxy 7 -> ()-testProxy5 = proxyFun4--testProxy5Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy ((2 * y1) + 4)"- ," Actual: Proxy 7"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy 7 -> ()"- ," Actual: Proxy ((2 * y1) + 4) -> ()"- ]-#else- ["Expected type: Proxy 7 -> ()"- ,"Actual type: Proxy ((2 * y1) + 4) -> ()"- ]-#endif--proxyFun6 :: Proxy (2^k) -> Proxy (2^k)-proxyFun6 = const Proxy--testProxy6 :: Proxy 7-testProxy6 = proxyFun6 (Proxy :: Proxy 7)--testProxy6Errors =-#if __GLASGOW_HASKELL__ >= 902- ["Expected: Proxy 7"- ," Actual: Proxy (2 ^ k0)"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy (2 ^ k0)"- ," Actual: Proxy 7"- ]-#else- ["Expected type: Proxy (2 ^ k0)"- ,"Actual type: Proxy 7"- ]-#endif--proxyFun7 :: Proxy (2^k) -> Proxy k-proxyFun7 = const Proxy--testProxy8 :: Proxy x -> Proxy (y + x)-testProxy8 = id--testProxy8Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy (y + x)"- ," Actual: Proxy x"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy x -> Proxy (y + x)"- ," Actual: Proxy x -> Proxy x"- ]-#else- ["Expected type: Proxy x -> Proxy (y + x)"- ,"Actual type: Proxy x -> Proxy x"- ]-#endif--#if __GLASGOW_HASKELL__ >= 904-proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()-#else-proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()-#endif-proxyInEq _ _ = ()--proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()-proxyInEq' _ _ = ()--testProxy9 :: Proxy (a + 1) -> Proxy a -> ()-testProxy9 = proxyInEq--testProxy9Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: a + 1 <= a"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False’"- else litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"- else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True"- )]-#endif--testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()-testProxy10 = proxyInEq'--testProxy10Errors =-#if __GLASGOW_HASKELL__ >= 910- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) True True False’"- else litE $ stringL "(CmpNat a (a + 2)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with `False"- )- ]-#elif __GLASGOW_HASKELL__ >= 906- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) True True False’"- else litE $ stringL "(CmpNat a (a + 2)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with False"- )- ]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False’"- else litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'False"- else litE $ stringL "with 'False"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"- else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False"- )]-#endif--testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()-testProxy11 = proxyInEq'--testProxy11Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8-#if __GLASGOW_HASKELL__ >= 910- then litE $ stringL "Couldn't match type ‘True’ with ‘False’"- else litE $ stringL "Couldn't match type `True' with `False'"-#elif __GLASGOW_HASKELL__ >= 906- then litE $ stringL "Couldn't match type ‘True’ with ‘False’"- else litE $ stringL "Couldn't match type True with False"-#else- then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"- else litE $ stringL "Couldn't match type 'True with 'False"-#endif- )]--testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()-testProxy12 = proxyInEq--testProxy12Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: a + b <= a + c"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"- else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True"- )]-#endif--testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()-testProxy13 = proxyInEq--testProxy13Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 4 * a <= 2 * a"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"- else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True"- )]-#endif--testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()-testProxy14 = proxyInEq'--testProxy14Errors =-#if __GLASGOW_HASKELL__ >= 910- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with `False"- )- ]-#elif __GLASGOW_HASKELL__ >= 906- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘False"- else litE $ stringL "with False"- )- ]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False’"- else litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'False"- else litE $ stringL "with 'False"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"- else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False"- )]-#endif--type family CLog (b :: Nat) (x :: Nat) :: Nat-type instance CLog 2 2 = 1--testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)-testProxy15 = id--testProxy15Errors =-#if __GLASGOW_HASKELL__ >= 914- ["Expected: Proxy (n + d)"- ," Actual: Proxy n"- ]-#elif __GLASGOW_HASKELL__ >= 900- ["Expected: Proxy n -> Proxy (n + d)"- ," Actual: Proxy n -> Proxy n"- ]-#else- ["Expected type: Proxy n -> Proxy (n + d)"- ,"Actual type: Proxy n -> Proxy n"- ]-#endif--data Fin (n :: Nat) where- FZ :: Fin (n + 1)- FS :: Fin n -> Fin (n + 1)--test16 :: forall n . Integer -> Fin n-test16 n = case n of- 0 -> FZ- x -> FS (test16 @(n-1) (x-1))--test16Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 1 <= n"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat 1 n) 'True 'True 'False’"- else litE $ stringL "(CmpNat 1 n) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’"- else litE $ stringL "Couldn't match type `1 <=? n' with 'True"- )]-#endif--data Dict c where- Dict :: c => Dict c-deriving instance Show (Dict c)-data Boo (n :: Nat) = Boo--test17 :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String-test17 = const show--testProxy17 :: String--testProxy17 = test17 (Proxy :: Proxy 17) Boo-test17Errors = test16Errors--#if __GLASGOW_HASKELL__ >= 904-test19f :: ((1 <= n) ~ (() :: Constraint))-#else-test19f :: (1 <= n)-#endif- => Proxy n -> Proxy n-test19f = id--testProxy19 :: (1 <= m, m <= rp)- => Proxy m- -> Proxy rp- -> Proxy (rp - m)- -> Proxy (rp - m)-testProxy19 _ _ = test19f--test19Errors =-#if __GLASGOW_HASKELL__ >= 904- [ "Cannot satisfy: 1 <= rp - m" ]-#elif __GLASGOW_HASKELL__ >= 902- [ "Could not deduce: Data.Type.Ord.OrdCond"- , "(CmpNat 1 (rp - m)) 'True 'True 'False"- , "~ 'True"- ]-#else- ["Could not deduce: (1 <=? (rp - m)) ~ 'True"]-#endif--testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> ()-testProxy20 = proxyInEq--testProxy20Errors =-#if __GLASGOW_HASKELL__ >= 904- ["Cannot satisfy: 1 <= m ^ 2"]-#elif __GLASGOW_HASKELL__ >= 902- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"- else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False’"- else litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False'"- )- ,$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "with ‘'True’"- else litE $ stringL "with 'True"- )- ]-#else- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘1 <=? (m ^ 2)’ with ‘'True’"- else litE $ stringL "Couldn't match type `1 <=? (m ^ 2)' with 'True"- )]-#endif--type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where- Drop 0 xs = xs- Drop n (x ': xs) = Drop (n-1) xs- Drop n '[] = '[]--t99 :: Proxy ns -> Proxy ( Drop 1 ns ) -> Proxy ( Drop 2 ns )-t99 _ px = px---- Don't want an error of the form 'Couldn't match 1 with 0'--- because that means the plugin turned [W] Drop 1 ns ~ Drop 2 ns--- into 1 ~ 2, which is not valid as Drop is not injective.-t99_errors =-#if __GLASGOW_HASKELL__ >= 811- [ "Couldn't match type: Drop 1 ns"- , " with: Drop 2 ns"- , "Expected: Proxy (Drop 2 ns)"- , " Actual: Proxy (Drop 1 ns)"- , $(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "‘Drop’ is a non-injective type family"- else litE $ stringL "`Drop' is a non-injective type family"- )- ]-#else- [ $(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘Drop 1 ns’ with ‘Drop 2 ns’"- else litE $ stringL "Couldn't match type `Drop 1 ns' with `Drop 2 ns'"- )- , "Expected type: Proxy (Drop 2 ns)"- , " Actual type: Proxy (Drop 1 ns)"- , $(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- 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
+ tests/ShouldError.hs view
@@ -0,0 +1,597 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE QuasiQuotes #-}++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+ , testIssue126+ , inequalityTests+ ]++preamble :: String+preamble = [i|+import Data.Kind (Constraint)+import Data.Proxy+import GHC.TypeLits+|] <> "\n"++source1 :: String+source1 = preamble <> [i|+test :: Proxy (x + 1) -> Proxy (2 + x)+test = id+|]++expected1 :: [String]+expected1 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (2 + x)"+ ," Actual: Proxy (x + 1)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (x + 1) -> Proxy (2 + x)"+ ," Actual: Proxy (x + 1) -> Proxy (x + 1)"+ ]+#else+ ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"+ ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#endif++test1 :: TestTree+test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1++source2 :: String+source2 = preamble <> [i|+type family GCD (x :: Nat) (y :: Nat) :: Nat+type instance GCD 6 8 = 2+type instance GCD 9 6 = 3++test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)+test = id+|]++expected2 :: [String]+expected2 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ," Actual: Proxy (2 + x) -> Proxy (2 + x)"+ ]+#else+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+ ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"+ ]+#endif++test2 :: TestTree+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2++source3 :: String+source3 = preamble <> [i|+proxyFun :: Proxy (x + x + x) -> ()+proxyFun = const ()++test :: Proxy 8 -> ()+test = proxyFun+|]++expected3 :: [String]+expected3 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((x0 + x0) + x0)"+ ," Actual: Proxy 8"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 8 -> ()"+ ," Actual: Proxy ((x0 + x0) + x0) -> ()"+ ]+#else+ ["Expected type: Proxy 8 -> ()"+ ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"+ ]+#endif++test3 :: TestTree+test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3++source4 :: String+source4 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 2 -> ()+test = proxyFun+|]++expected4 :: [String]+expected4 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y0) + 4)"+ ," Actual: Proxy 2"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 2 -> ()"+ ," Actual: Proxy ((2 * y0) + 4) -> ()"+ ]+#else+ ["Expected type: Proxy 2 -> ()"+ ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+ ]+#endif++test4 :: TestTree+test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4++source5 :: String+source5 = preamble <> [i|+proxyFun :: Proxy ((2*y)+4) -> ()+proxyFun = const ()++test :: Proxy 7 -> ()+test = proxyFun+|]++expected5 :: [String]+expected5 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy ((2 * y"+ ,"Actual: Proxy 7"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy 7 -> ()"+ ,"Actual: Proxy ((2 * y"+ ]+#else+ ["Expected type: Proxy 7 -> ()"+ ,"Actual type: Proxy ((2 * y"+ ]+#endif++test5 :: TestTree+test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5++source6 :: String+source6 = preamble <> [i|+proxyFun :: Proxy (2^k) -> Proxy (2^k)+proxyFun = const Proxy++test :: Proxy 7+test = proxyFun (Proxy :: Proxy 7)+|]++expected6 :: [String]+expected6 =+#if __GLASGOW_HASKELL__ >= 902+ ["Expected: Proxy 7"+ ," Actual: Proxy (2 ^ k0)"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy (2 ^ k0)"+ ," Actual: Proxy 7"+ ]+#else+ ["Expected type: Proxy (2 ^ k0)"+ ,"Actual type: Proxy 7"+ ]+#endif++test6 :: TestTree+test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6++source7 :: String+source7 = preamble <> [i|+test :: Proxy x -> Proxy (y + x)+test = id+|]++expected7 :: [String]+expected7 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (y + x)"+ ," Actual: Proxy x"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy x -> Proxy (y + x)"+ ," Actual: Proxy x -> Proxy x"+ ]+#else+ ["Expected type: Proxy x -> Proxy (y + x)"+ ,"Actual type: Proxy x -> Proxy x"+ ]+#endif++test7 :: TestTree+test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7++source8 :: String+source8 = preamble <> [i|+type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1++test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)+test = id+|]++expected8 :: [String]+expected8 =+#if __GLASGOW_HASKELL__ >= 914+ ["Expected: Proxy (n + d)"+ ," Actual: Proxy n"+ ]+#elif __GLASGOW_HASKELL__ >= 900+ ["Expected: Proxy n -> Proxy (n + d)"+ ," Actual: Proxy n -> Proxy n"+ ]+#else+ ["Expected type: Proxy n -> Proxy (n + d)"+ ,"Actual type: Proxy n -> Proxy n"+ ]+#endif++test8 :: TestTree+test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $+ assertCompileError source8 expected8++source9 :: String+source9 = preamble <> [i|+data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)++test :: forall n . Integer -> Fin n+test n = case n of+ 0 -> FZ+ x -> FS (test @(n-1) (x-1))+|]++expected9 :: [String]+expected9 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= n"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 n) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? n with True" ]+#endif++test9 :: TestTree+test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9++source10 :: String+source10 = preamble <> [i|+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]++test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns)+test _ px = px+|]++expected10 :: [String]+expected10 =+#if __GLASGOW_HASKELL__ >= 811+ [ "Couldn't match type: Drop 1 ns"+ , " with: Drop 2 ns"+ , "Expected: Proxy (Drop 2 ns)"+ , " Actual: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#else+ [ "Couldn't match type Drop 1 ns with Drop 2 ns"+ , "Expected type: Proxy (Drop 2 ns)"+ , " Actual type: Proxy (Drop 1 ns)"+ , "Drop is a non-injective type family"+ ]+#endif++test10 :: TestTree+test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10++source11 :: String+source11 = preamble <> [i|+test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5+test _ _ = id+|]++expected11 :: [String]+expected11 =+#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++test11 :: TestTree+test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11++-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so+-- the equality would require b0 ~ -2, which is impossible at kind Nat.+sourceIssue126 :: String+sourceIssue126 = preamble <> [i|+data Index (n :: Nat) = Index++truncateB :: Index (a + b) -> Index a+truncateB = undefined++mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1)+mul _ _ = Index++zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3)+zeroExtendTimesThree = truncateB . (mul Index)+|]++expectedIssue126 :: [String]+expectedIssue126 =+#if __GLASGOW_HASKELL__ >= 906+ [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#elif __GLASGOW_HASKELL__ >= 904+ [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))"+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"+#else+ [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)"+#endif+ , "from the context: 1 <= n"+ ]++++testIssue126 :: TestTree+testIssue126 =+ testCase "Issue 126 regression reproducer" $+ assertCompileError sourceIssue126 expectedIssue126++proxyInEqDef :: String+proxyInEqDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#else+ [i|+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()+|]+#endif++proxyInEq'Def :: String+proxyInEq'Def = [i|+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq' _ _ = ()+|]++source12 :: String+source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + 1) -> Proxy a -> ()+test = proxyInEq+|]++expected12 :: [String]+expected12 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + 1 <= a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + 1) a) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + 1) <=? a with True" ]+#endif++test12 :: TestTree+test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12++source13 :: String+source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()+test = proxyInEq'+|]++expected13 :: [String]+expected13 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat a (a + 2)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type a <=? (a + 2) with False" ]+#endif++test13 :: TestTree+test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13++source14 :: String+source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a :: Nat) -> Proxy a -> ()+test = proxyInEq'+|]++expected14 :: [String]+expected14 = [ "Couldn't match type True with False" ]++test14 :: TestTree+test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14++source15 :: String+source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (a + b) -> Proxy (a + c) -> ()+test = proxyInEq+|]++expected15 :: [String]+expected15 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: a + b <= a + c"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (a + b) (a + c)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (a + b) <=? (a + c) with True" ]+#endif++test15 :: TestTree+test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15++source16 :: String+source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (4*a) -> Proxy (2*a) -> ()+test = proxyInEq+|]++expected16 :: [String]+expected16 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 4 * a <= 2 * a"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat (4 * a) (2 * a)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type (4 * a) <=? (2 * a) with True" ]+#endif++test16 :: TestTree+test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16++source17 :: String+source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|+test :: Proxy (2*a) -> Proxy (4*a) -> ()+test = proxyInEq'+|]++expected17 :: [String]+expected17 =+#if __GLASGOW_HASKELL__ >= 902+ [ "Data.Type.Ord.OrdCond"+ , "(CmpNat (2 * a) (4 * a)) True True False"+ , "with False"+ ]+#else+ [ "Couldn't match type (2 * a) <=? (4 * a) with False" ]+#endif++test17 :: TestTree+test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17++source18 :: String+source18 = preamble <> [i|+data Boo (n :: Nat) = Boo++test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String+test = const show+|]++expected18 :: [String]+expected18 = expected9++test18 :: TestTree+test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18++test19fDef :: String+test19fDef =+#if __GLASGOW_HASKELL__ >= 904+ [i|+test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n+test19f = id+|]+#else+ [i|+test19f :: (1 <= n) => Proxy n -> Proxy n+test19f = id+|]+#endif++source19 :: String+source19 = preamble <> test19fDef <> [i|+test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m)+test _ _ = test19f+|]++expected19 :: [String]+expected19 =+#if __GLASGOW_HASKELL__ >= 904+ [ "Cannot satisfy: 1 <= rp - m" ]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (rp - m)) True True False"+ , "~ True"+ ]+#else+ [ "Could not deduce: (1 <=? (rp - m)) ~ True" ]+#endif++test19 :: TestTree+test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19++source20 :: String+source20 = preamble <> proxyInEqDef <> [i|+test :: Proxy 1 -> Proxy (m ^ 2) -> ()+test = proxyInEq+|]++expected20 :: [String]+expected20 =+#if __GLASGOW_HASKELL__ >= 904+ ["Cannot satisfy: 1 <= m ^ 2"]+#elif __GLASGOW_HASKELL__ >= 902+ [ "Couldn't match type Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (m ^ 2)) True True False"+ , "with True"+ ]+#else+ [ "Couldn't match type 1 <=? (m ^ 2) with True" ]+#endif++test20 :: TestTree+test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20++inequalityTests :: TestTree+inequalityTests = testGroup "Inequality"+ [ test12+ , test13+ , test14+ , test15+ , test16+ , test17+ , test18+ , test19+ , test20+ ]
+ tests/ShouldError/Tasty.hs view
@@ -0,0 +1,58 @@+{-# 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"+ , "-XAllowAmbiguousTypes"+ , "-XConstraintKinds"+ , "-XDataKinds"+ , "-XFlexibleContexts"+ , "-XGADTs"+ , "-XScopedTypeVariables"+ , "-XStandaloneDeriving"+ , "-XTypeApplications"+ , "-XTypeFamilies"+ , "-XTypeOperators"+ , "-XUndecidableInstances"+ , "-XNoStarIsType"+ , "-fno-code"+ , "-fplugin", "GHC.TypeLits.Normalise"+ , 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 = "‘’`'"
tests/Tests.hs view
@@ -37,14 +37,13 @@ import Data.Type.Ord #endif -import Data.Kind (Type)-import Data.List (isInfixOf)+import Data.Kind (Type, Constraint) import Data.Proxy-import Control.Exception+import Data.Type.Equality ((:~:)(..)) import Test.Tasty import Test.Tasty.HUnit -import ErrorTests+import qualified ShouldError data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a@@ -308,6 +307,15 @@ a' -> B0 a' predBNat (B0 x) = B1 (predBNat x) +proxyFun3 :: Proxy (x + x + x) -> ()+proxyFun3 = const ()++proxyFun4 :: Proxy ((2*y)+4) -> ()+proxyFun4 = const ()++proxyFun7 :: Proxy (2^k) -> Proxy k+proxyFun7 = const Proxy+ -- issue 52 begin type role Signal nominal representational data Signal (dom :: Symbol) a = a :- Signal dom a@@ -325,6 +333,12 @@ issue52 = bundle -- issue 52 end +proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq _ _ = ()++proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()+proxyInEq' _ _ = ()+ proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq @@ -453,6 +467,14 @@ succAtMost :: AtMost n -> AtMost (n + 1) succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a) +data Dict c where+ Dict :: c => Dict c++instance Show (Dict c) where+ show Dict = "Dict"++data Boo (n :: Nat) = Boo+ eqReduceForward :: Eq (Boo (n + 1)) => Dict (Eq (Boo (n + 2 - 1)))@@ -473,6 +495,9 @@ => Dict (Eq (Boo (m + 3))) eqReduceBackward' = Dict +type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1+ proxyInEq8fun :: (1 <= (n + CLog 2 n)) => Proxy n@@ -512,6 +537,11 @@ go :: 1 <= b => Proxy a -> Proxy a go = id +type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where+ Drop 0 xs = xs+ Drop n (x ': xs) = Drop (n-1) xs+ Drop n '[] = '[]+ isOkay :: forall x y sh . Proxy x ->@@ -628,47 +658,9 @@ show (oneLtPowSubst (Proxy :: Proxy 0)) @?= "Proxy" ]- , testGroup "errors"- [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors- , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors- , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors- , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors- , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors- , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors- , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors- , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $- 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- , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors- , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors- , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors- , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors- , testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $- testProxy17 `throws` test17Errors- , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @1) (Proxy @1)) `throws` test19Errors- , testCase "Vacuously: 1 <= m ^ 2 ~ True" $ testProxy20 `throws` testProxy20Errors- ]- ]+ , 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` msg) xs- then return ()- else assertFailure msg- showFin :: forall n. KnownNat n => Fin n -> String showFin f = mconcat [ show (finToInt f)@@ -680,6 +672,10 @@ finToInt FZ = 0 finToInt (FS fn) = finToInt fn + 1 +data Fin (n :: Nat) where+ FZ :: Fin (n + 1)+ FS :: Fin n -> Fin (n + 1)+ predFin :: Fin (n + 2) -> Fin (n + 1) predFin (FS fn) = fn predFin FZ = FZ@@ -798,3 +794,44 @@ ) => Proxy n -> Proxy m -> () t97b _ _ = ()++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/116+t116 :: forall n m l. m :~: n -> n :~: 0 -> l :~: 1 -> Float+t116 a b c =+ case a of+ Refl ->+ case b of+ Refl ->+ case c of+ Refl ->+ 3.0++type family Foo (n :: Nat) :: Nat++t119a :: Proxy n -> Proxy (Foo (n + 2)) -> Proxy (Foo (2 + n))+t119a _ = id++--Only applicable for GHC >= 9.4 as prior InEq constraints are of the form `a <=? b ~ 'True`+#if __GLASGOW_HASKELL__ >= 904+t119b ::+ (1 <= a) =>+ (1 <= Foo (a + 1)) =>+ Proxy a ->+ Proxy a+t119b a = go a+ where+ go ::+ ((1 <= Foo (c + 1)) ~ (() :: Constraint)) =>+ Proxy c ->+ Proxy c+ go _ = Proxy+#endif++data NatPhantom (n :: Nat) = NatPhantom++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124+t124 :: 1 <= n => NatPhantom m -> NatPhantom (m + n - 1)+t124 x = go x+ where+ go :: NatPhantom a -> NatPhantom (b + a)+ go _ = NatPhantom