Resolving dependencies... Build profile: -w ghc-9.2.4 -O0 In order, the following will be built (use -v for more details): - ghc-tcplugins-extra-0.4.4 (lib:ghc-tcplugins-extra) (requires build) - tasty-hunit-0.10.0.3 (lib:tasty-hunit) (requires build) - ghc-typelits-natnormalise-0.7.8 (first run) Starting tasty-hunit-0.10.0.3 (all, legacy fallback) Starting ghc-tcplugins-extra-0.4.4 (all, legacy fallback) Building tasty-hunit-0.10.0.3 (all, legacy fallback) Building ghc-tcplugins-extra-0.4.4 (all, legacy fallback) Installing tasty-hunit-0.10.0.3 (all, legacy fallback) Installing ghc-tcplugins-extra-0.4.4 (all, legacy fallback) Completed tasty-hunit-0.10.0.3 (all, legacy fallback) Completed ghc-tcplugins-extra-0.4.4 (all, legacy fallback) Configuring ghc-typelits-natnormalise-0.7.8... Preprocessing library for ghc-typelits-natnormalise-0.7.8.. Building library for ghc-typelits-natnormalise-0.7.8.. [1 of 3] Compiling GHC.TypeLits.Normalise.SOP ( src/GHC/TypeLits/Normalise/SOP.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise/SOP.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise/SOP.dyn_o ) [2 of 3] Compiling GHC.TypeLits.Normalise.Unify ( src/GHC/TypeLits/Normalise/Unify.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise/Unify.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise/Unify.dyn_o ) [3 of 3] Compiling GHC.TypeLits.Normalise ( src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/GHC/TypeLits/Normalise.dyn_o ) Preprocessing test suite 'unit-tests' for ghc-typelits-natnormalise-0.7.8.. Building test suite 'unit-tests' for ghc-typelits-natnormalise-0.7.8.. [1 of 2] Compiling ErrorTests ( tests/ErrorTests.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/ErrorTests.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/ErrorTests.dyn_o ) tests/ErrorTests.hs:32:14: warning: [-Wdeferred-type-errors] " Couldn't match type: x + 1 with: 2 + x Expected: Proxy (x + 1) -> Proxy (2 + x) Actual: Proxy (x + 1) -> Proxy (x + 1) NB: + is a non-injective type family " In the expression: id In an equation for testProxy1: testProxy1 = id " Relevant bindings include testProxy1 :: Proxy (x + 1) -> Proxy (2 + x) (bound at tests/ErrorTests.hs:32:1) | 32 | testProxy1 = id | ^^ tests/ErrorTests.hs:50:14: warning: [-Wdeferred-type-errors] " Couldn't match type: 2 + x with: x + 3 Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) Actual: Proxy (2 + x) -> Proxy (2 + x) NB: + is a non-injective type family " In the expression: id In an equation for testProxy2: testProxy2 = id " Relevant bindings include testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) (bound at tests/ErrorTests.hs:50:1) | 50 | testProxy2 = id | ^^ tests/ErrorTests.hs:67:14: warning: [-Wdeferred-type-errors] " Couldn't match type (x0 + x0) + x0 with 8 Expected: Proxy 8 -> () Actual: Proxy ((x0 + x0) + x0) -> () The type variable x0 is ambiguous " In the expression: proxyFun3 In an equation for testProxy3: testProxy3 = proxyFun3 | 67 | testProxy3 = proxyFun3 | ^^^^^^^^^ tests/ErrorTests.hs:84:14: warning: [-Wdeferred-type-errors] " Couldn't match type (2 * y0) + 4 with 2 Expected: Proxy 2 -> () Actual: Proxy ((2 * y0) + 4) -> () The type variable y0 is ambiguous " In the expression: proxyFun4 In an equation for testProxy4: testProxy4 = proxyFun4 | 84 | testProxy4 = proxyFun4 | ^^^^^^^^^ tests/ErrorTests.hs:98:14: warning: [-Wdeferred-type-errors] " Couldn't match type (2 * y1) + 4 with 7 Expected: Proxy 7 -> () Actual: Proxy ((2 * y1) + 4) -> () The type variable y1 is ambiguous " In the expression: proxyFun4 In an equation for testProxy5: testProxy5 = proxyFun4 | 98 | testProxy5 = proxyFun4 | ^^^^^^^^^ tests/ErrorTests.hs:115:14: warning: [-Wdeferred-type-errors] " Couldn't match type 2 ^ k0 with 7 Expected: Proxy 7 Actual: Proxy (2 ^ k0) The type variable k0 is ambiguous " In the expression: proxyFun6 (Proxy :: Proxy 7) In an equation for testProxy6: testProxy6 = proxyFun6 (Proxy :: Proxy 7) | 115 | testProxy6 = proxyFun6 (Proxy :: Proxy 7) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ tests/ErrorTests.hs:136:14: warning: [-Wdeferred-type-errors] " Couldn't match type x with y + x Expected: Proxy x -> Proxy (y + x) Actual: Proxy x -> Proxy x x is a rigid type variable bound by the type signature for: testProxy8 :: forall (x :: Natural) (y :: Natural). Proxy x -> Proxy (y + x) at tests/ErrorTests.hs:135:1-38 " In the expression: id In an equation for testProxy8: testProxy8 = id " Relevant bindings include testProxy8 :: Proxy x -> Proxy (y + x) (bound at tests/ErrorTests.hs:136:1) | 136 | testProxy8 = id | ^^ tests/ErrorTests.hs:160:14: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (a + 1) a) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy9: testProxy9 = proxyInEq " Relevant bindings include testProxy9 :: Proxy (a + 1) -> Proxy a -> () (bound at tests/ErrorTests.hs:160:1) | 160 | testProxy9 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:191:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat a (a + 2)) 'True 'True 'False with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy10: testProxy10 = proxyInEq' " Relevant bindings include testProxy10 :: Proxy a -> Proxy (a + 2) -> () (bound at tests/ErrorTests.hs:191:1) | 191 | testProxy10 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:237:15: warning: [-Wdeferred-type-errors] " Couldn't match type 'True with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy11: testProxy11 = proxyInEq' | 237 | testProxy11 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:251:16: warning: [-Wdeferred-type-errors] " Couldn't match type: a0 + b0 with: a + b Expected: Proxy (a + b) -> Proxy (a + c) -> () Actual: Proxy (a0 + b0) -> Proxy (a0 + c0) -> () NB: + is a non-injective type family The type variables a0, b0 are ambiguous " In the ambiguity check for testProxy12 To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () | 251 | testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ tests/ErrorTests.hs:252:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy12: testProxy12 = proxyInEq " Relevant bindings include testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () (bound at tests/ErrorTests.hs:252:1) | 252 | testProxy12 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:283:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (4 * a) (2 * a)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy13: testProxy13 = proxyInEq " Relevant bindings include testProxy13 :: Proxy (4 * a) -> Proxy (2 * a) -> () (bound at tests/ErrorTests.hs:283:1) | 283 | testProxy13 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:314:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (2 * a) (4 * a)) 'True 'True 'False with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy14: testProxy14 = proxyInEq' " Relevant bindings include testProxy14 :: Proxy (2 * a) -> Proxy (4 * a) -> () (bound at tests/ErrorTests.hs:314:1) | 314 | testProxy14 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:363:15: warning: [-Wdeferred-type-errors] " Could not deduce: (n + d) ~ n from the context: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) bound by the type signature for: testProxy15 :: forall (n :: Natural) (d :: Natural). (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) => Proxy n -> Proxy (n + d) at tests/ErrorTests.hs:362:1-79 Expected: Proxy n -> Proxy (n + d) Actual: Proxy n -> Proxy n n is a rigid type variable bound by the type signature for: testProxy15 :: forall (n :: Natural) (d :: Natural). (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) => Proxy n -> Proxy (n + d) at tests/ErrorTests.hs:362:1-79 " In the expression: id In an equation for testProxy15: testProxy15 = id " Relevant bindings include testProxy15 :: Proxy n -> Proxy (n + d) (bound at tests/ErrorTests.hs:363:1) | 363 | testProxy15 = id | ^^ tests/ErrorTests.hs:382:8: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 n) 'True 'True 'False with 'True Expected: Fin n Actual: Fin ((n - 1) + 1) " In the expression: FZ In a case alternative: 0 -> FZ In the expression: case n of 0 -> FZ x -> FS (test16 @(n - 1) (x - 1)) " Relevant bindings include test16 :: Integer -> Fin n (bound at tests/ErrorTests.hs:381:1) | 382 | 0 -> FZ | ^^ tests/ErrorTests.hs:419:16: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 n) 'True 'True 'False with 'True arising from a use of show " In the first argument of const, namely show In the expression: const show In an equation for test17: test17 = const show " Relevant bindings include test17 :: Proxy n -> Boo ((n - 1) + 1) -> String (bound at tests/ErrorTests.hs:419:1) | 419 | test17 = const show | ^^^^ tests/ErrorTests.hs:439:19: warning: [-Wdeferred-type-errors] " Could not deduce: Data.Type.Ord.OrdCond (CmpNat 1 (rp - m)) 'True 'True 'False ~ 'True arising from a use of test19f from the context: (1 <= m, m <= rp) bound by the type signature for: testProxy19 :: forall (m :: Natural) (rp :: Natural). (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m) at tests/ErrorTests.hs:(434,1)-(438,19) " In the expression: test19f In an equation for testProxy19: testProxy19 _ _ = test19f " Relevant bindings include testProxy19 :: Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m) (bound at tests/ErrorTests.hs:439:1) | 439 | testProxy19 _ _ = test19f | ^^^^^^^ tests/ErrorTests.hs:454:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 (m ^ 2)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy20: testProxy20 = proxyInEq " Relevant bindings include testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> () (bound at tests/ErrorTests.hs:454:1) | 454 | testProxy20 = proxyInEq | ^^^^^^^^^ [2 of 2] Compiling Main ( tests/Tests.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/Main.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/Main.dyn_o ) [1 of 2] Compiling ErrorTests ( tests/ErrorTests.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/ErrorTests.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/ErrorTests.dyn_o ) [HPC flags changed] tests/ErrorTests.hs:32:14: warning: [-Wdeferred-type-errors] " Couldn't match type: x + 1 with: 2 + x Expected: Proxy (x + 1) -> Proxy (2 + x) Actual: Proxy (x + 1) -> Proxy (x + 1) NB: + is a non-injective type family " In the expression: id In an equation for testProxy1: testProxy1 = id " Relevant bindings include testProxy1 :: Proxy (x + 1) -> Proxy (2 + x) (bound at tests/ErrorTests.hs:32:1) | 32 | testProxy1 = id | ^^ tests/ErrorTests.hs:50:14: warning: [-Wdeferred-type-errors] " Couldn't match type: 2 + x with: x + 3 Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) Actual: Proxy (2 + x) -> Proxy (2 + x) NB: + is a non-injective type family " In the expression: id In an equation for testProxy2: testProxy2 = id " Relevant bindings include testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) (bound at tests/ErrorTests.hs:50:1) | 50 | testProxy2 = id | ^^ tests/ErrorTests.hs:67:14: warning: [-Wdeferred-type-errors] " Couldn't match type (x0 + x0) + x0 with 8 Expected: Proxy 8 -> () Actual: Proxy ((x0 + x0) + x0) -> () The type variable x0 is ambiguous " In the expression: proxyFun3 In an equation for testProxy3: testProxy3 = proxyFun3 | 67 | testProxy3 = proxyFun3 | ^^^^^^^^^ tests/ErrorTests.hs:84:14: warning: [-Wdeferred-type-errors] " Couldn't match type (2 * y0) + 4 with 2 Expected: Proxy 2 -> () Actual: Proxy ((2 * y0) + 4) -> () The type variable y0 is ambiguous " In the expression: proxyFun4 In an equation for testProxy4: testProxy4 = proxyFun4 | 84 | testProxy4 = proxyFun4 | ^^^^^^^^^ tests/ErrorTests.hs:98:14: warning: [-Wdeferred-type-errors] " Couldn't match type (2 * y1) + 4 with 7 Expected: Proxy 7 -> () Actual: Proxy ((2 * y1) + 4) -> () The type variable y1 is ambiguous " In the expression: proxyFun4 In an equation for testProxy5: testProxy5 = proxyFun4 | 98 | testProxy5 = proxyFun4 | ^^^^^^^^^ tests/ErrorTests.hs:115:14: warning: [-Wdeferred-type-errors] " Couldn't match type 2 ^ k0 with 7 Expected: Proxy 7 Actual: Proxy (2 ^ k0) The type variable k0 is ambiguous " In the expression: proxyFun6 (Proxy :: Proxy 7) In an equation for testProxy6: testProxy6 = proxyFun6 (Proxy :: Proxy 7) | 115 | testProxy6 = proxyFun6 (Proxy :: Proxy 7) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ tests/ErrorTests.hs:136:14: warning: [-Wdeferred-type-errors] " Couldn't match type x with y + x Expected: Proxy x -> Proxy (y + x) Actual: Proxy x -> Proxy x x is a rigid type variable bound by the type signature for: testProxy8 :: forall (x :: Natural) (y :: Natural). Proxy x -> Proxy (y + x) at tests/ErrorTests.hs:135:1-38 " In the expression: id In an equation for testProxy8: testProxy8 = id " Relevant bindings include testProxy8 :: Proxy x -> Proxy (y + x) (bound at tests/ErrorTests.hs:136:1) | 136 | testProxy8 = id | ^^ tests/ErrorTests.hs:160:14: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (a + 1) a) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy9: testProxy9 = proxyInEq " Relevant bindings include testProxy9 :: Proxy (a + 1) -> Proxy a -> () (bound at tests/ErrorTests.hs:160:1) | 160 | testProxy9 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:191:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat a (a + 2)) 'True 'True 'False with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy10: testProxy10 = proxyInEq' " Relevant bindings include testProxy10 :: Proxy a -> Proxy (a + 2) -> () (bound at tests/ErrorTests.hs:191:1) | 191 | testProxy10 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:237:15: warning: [-Wdeferred-type-errors] " Couldn't match type 'True with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy11: testProxy11 = proxyInEq' | 237 | testProxy11 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:251:16: warning: [-Wdeferred-type-errors] " Couldn't match type: a0 + b0 with: a + b Expected: Proxy (a + b) -> Proxy (a + c) -> () Actual: Proxy (a0 + b0) -> Proxy (a0 + c0) -> () NB: + is a non-injective type family The type variables a0, b0 are ambiguous " In the ambiguity check for testProxy12 To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () | 251 | testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ tests/ErrorTests.hs:252:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (a + b) (a + c)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy12: testProxy12 = proxyInEq " Relevant bindings include testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () (bound at tests/ErrorTests.hs:252:1) | 252 | testProxy12 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:283:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (4 * a) (2 * a)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy13: testProxy13 = proxyInEq " Relevant bindings include testProxy13 :: Proxy (4 * a) -> Proxy (2 * a) -> () (bound at tests/ErrorTests.hs:283:1) | 283 | testProxy13 = proxyInEq | ^^^^^^^^^ tests/ErrorTests.hs:314:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat (2 * a) (4 * a)) 'True 'True 'False with 'False arising from a use of proxyInEq' " In the expression: proxyInEq' In an equation for testProxy14: testProxy14 = proxyInEq' " Relevant bindings include testProxy14 :: Proxy (2 * a) -> Proxy (4 * a) -> () (bound at tests/ErrorTests.hs:314:1) | 314 | testProxy14 = proxyInEq' | ^^^^^^^^^^ tests/ErrorTests.hs:363:15: warning: [-Wdeferred-type-errors] " Could not deduce: (n + d) ~ n from the context: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) bound by the type signature for: testProxy15 :: forall (n :: Natural) (d :: Natural). (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) => Proxy n -> Proxy (n + d) at tests/ErrorTests.hs:362:1-79 Expected: Proxy n -> Proxy (n + d) Actual: Proxy n -> Proxy n n is a rigid type variable bound by the type signature for: testProxy15 :: forall (n :: Natural) (d :: Natural). (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ 'True) => Proxy n -> Proxy (n + d) at tests/ErrorTests.hs:362:1-79 " In the expression: id In an equation for testProxy15: testProxy15 = id " Relevant bindings include testProxy15 :: Proxy n -> Proxy (n + d) (bound at tests/ErrorTests.hs:363:1) | 363 | testProxy15 = id | ^^ tests/ErrorTests.hs:382:8: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 n) 'True 'True 'False with 'True Expected: Fin n Actual: Fin ((n - 1) + 1) " In the expression: FZ In a case alternative: 0 -> FZ In the expression: case n of 0 -> FZ x -> FS (test16 @(n - 1) (x - 1)) " Relevant bindings include test16 :: Integer -> Fin n (bound at tests/ErrorTests.hs:381:1) | 382 | 0 -> FZ | ^^ tests/ErrorTests.hs:419:16: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 n) 'True 'True 'False with 'True arising from a use of show " In the first argument of const, namely show In the expression: const show In an equation for test17: test17 = const show " Relevant bindings include test17 :: Proxy n -> Boo ((n - 1) + 1) -> String (bound at tests/ErrorTests.hs:419:1) | 419 | test17 = const show | ^^^^ tests/ErrorTests.hs:439:19: warning: [-Wdeferred-type-errors] " Could not deduce: Data.Type.Ord.OrdCond (CmpNat 1 (rp - m)) 'True 'True 'False ~ 'True arising from a use of test19f from the context: (1 <= m, m <= rp) bound by the type signature for: testProxy19 :: forall (m :: Natural) (rp :: Natural). (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m) at tests/ErrorTests.hs:(434,1)-(438,19) " In the expression: test19f In an equation for testProxy19: testProxy19 _ _ = test19f " Relevant bindings include testProxy19 :: Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m) (bound at tests/ErrorTests.hs:439:1) | 439 | testProxy19 _ _ = test19f | ^^^^^^^ tests/ErrorTests.hs:454:15: warning: [-Wdeferred-type-errors] " Couldn't match type Data.Type.Ord.OrdCond (CmpNat 1 (m ^ 2)) 'True 'True 'False with 'True arising from a use of proxyInEq " In the expression: proxyInEq In an equation for testProxy20: testProxy20 = proxyInEq " Relevant bindings include testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> () (bound at tests/ErrorTests.hs:454:1) | 454 | testProxy20 = proxyInEq | ^^^^^^^^^ [2 of 2] Compiling Main ( tests/Tests.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/Main.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests-tmp/Main.dyn_o ) [HPC flags changed] Linking /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/build/unit-tests/unit-tests ... Running 1 test suites... Test suite unit-tests: RUNNING... Test suite unit-tests: PASS Test suite logged to: /home/builder/builder-dir/build-cache/tmp-install/reports/ghc-typelits-natnormalise-0.7.8.test Writing: hpc_index.html Writing: hpc_index_fun.html Writing: hpc_index_alt.html Writing: hpc_index_exp.html Test coverage report written to /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/hpc/vanilla/html/unit-tests/hpc_index.html 1 of 1 test suites (1 of 1 test cases) passed. Writing: hpc_index.html Writing: hpc_index_fun.html Writing: hpc_index_alt.html Writing: hpc_index_exp.html Package coverage report written to /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/ghc-typelits-natnormalise-0.7.8/noopt/hpc/vanilla/html/ghc-typelits-natnormalise-0.7.8/hpc_index.html