[all reports]
| Package |
ghc-typelits-natnormalise-0.7.9 |
| Install |
InstallOk |
| Docs |
Ok |
| Tests |
Ok |
| Time submitted |
2023-10-10 15:23:25.576542421 UTC
|
| Compiler |
ghc-9.2.4 |
| OS |
linux |
| Arch |
x86_64 |
| Dependencies |
base-4.16.3.0, containers-0.6.5.1, ghc-9.2.4, ghc-bignum-1.2, ghc-tcplugins-extra-0.4.5, transformers-0.5.6.2 |
| Flags |
-deverror
|
Code Coverage
| expressions | 100% (0/0) |
|---|
| boolean | guards | 100% (0/0) |
|---|
| conditions | 100% (0/0) |
|---|
| qualifiers | 100% (0/0) |
|---|
| alternatives | 100% (0/0) |
|---|
| local declarations | 100% (0/0) |
|---|
| top-level declarations | 100% (0/0) |
|---|
Build log
[view raw]
Resolving dependencies...
Starting ghc-tcplugins-extra-0.4.5
Building ghc-tcplugins-extra-0.4.5
Completed ghc-tcplugins-extra-0.4.5
Starting ghc-typelits-natnormalise-0.7.9
Building ghc-typelits-natnormalise-0.7.9
Completed ghc-typelits-natnormalise-0.7.9
Test log
[view raw]
Resolving dependencies...
Build profile: -w ghc-9.2.4 -O0
In order, the following will be built (use -v for more details):
- ghc-typelits-natnormalise-0.7.9 (first run)
Configuring ghc-typelits-natnormalise-0.7.9...
Preprocessing library for ghc-typelits-natnormalise-0.7.9..
Building library for ghc-typelits-natnormalise-0.7.9..
[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.9/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.9/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.9/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.9/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.9/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.9/noopt/build/GHC/TypeLits/Normalise.dyn_o )
Preprocessing test suite 'unit-tests' for ghc-typelits-natnormalise-0.7.9..
Building test suite 'unit-tests' for ghc-typelits-natnormalise-0.7.9..
[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.9/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.9/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.9/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.9/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.9/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.9/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.9/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.9/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.9/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.9.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.9/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.9/noopt/hpc/vanilla/html/ghc-typelits-natnormalise-0.7.9/hpc_index.html