blob: 55798b1189d064c52e49828bc42a52d3ff5d1dc2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
T13674.hs:56:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
Expected: GF m
Actual: GF (Lcm m m)
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at T13674.hs:55:1-44
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at T13674.hs:56:17)
x :: GF m (bound at T13674.hs:56:6)
bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
T13674.hs:56:31: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
Expected: GF m
Actual: GF (Lcm m m)
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at T13674.hs:55:1-44
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at T13674.hs:56:17)
x :: GF m (bound at T13674.hs:56:6)
bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
|
