blob: 0a75b049ecf286c827f5bc68fa6d21f692c960ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
T12444.hs:19:11: error:
• Couldn't match type ‘b’ with ‘'Succ (c :+: b)’
Expected: SNat ('Succ (c :+: b))
Actual: SNat b
‘b’ is a rigid type variable bound by
the type signature for:
foo :: forall (c :: Nat) (b :: Nat).
SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
at T12444.hs:18:1-55
• In the expression: x
In an equation for ‘foo’: foo _ x = x
• Relevant bindings include
x :: SNat b (bound at T12444.hs:19:7)
foo :: SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
(bound at T12444.hs:19:1)
|
