blob: 53a7cb705cce3bc57c4533f650d06892ceb56b90 (
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
|
T13674.hs:56:21: error:
• Occurs check: cannot construct the infinite type: m ~ Lcm m m
Expected type: GF m
Actual type: GF (Lcm m m)
• 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:
• Occurs check: cannot construct the infinite type: m ~ Lcm m m
Expected type: GF m
Actual type: GF (Lcm m m)
• 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)
|