blob: f78ccc0d6110f28050fbbc5885368d2f0081dff5 (
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
|
T7230.hs:48:32: error:
• Could not deduce: (x :<<= x1) ~ 'True
from the context: Increasing xs ~ 'True
bound by the type signature for:
crash :: forall (xs :: [Nat]).
(Increasing xs ~ 'True) =>
SList xs -> SBool (Increasing xs)
at T7230.hs:47:1-68
or from: xs ~ (x : xs1)
bound by a pattern with constructor:
SCons :: forall {a} (x :: a) (xs :: [a]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:8-27
or from: xs1 ~ (x1 : xs2)
bound by a pattern with constructor:
SCons :: forall {a} (x :: a) (xs :: [a]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:17-26
Expected type: SBool (Increasing xs)
Actual type: SBool (x :<<= x1)
• In the expression: x %:<<= y
In an equation for ‘crash’:
crash (SCons x (SCons y xs)) = x %:<<= y
• Relevant bindings include
y :: Sing x1 (bound at T7230.hs:48:23)
x :: Sing x (bound at T7230.hs:48:14)
|
