summaryrefslogtreecommitdiff
path: root/testsuite/tests/polykinds/T7230.stderr
blob: f59e44d5cd8d0e0692e38d23ab81a882463c24c7 (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 {k} (x :: k) (xs :: [k]).
                            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 {k} (x :: k) (xs :: [k]).
                            Sing x -> Sing xs -> Sing (x : xs),
                 in an equation for ‘crash’
        at T7230.hs:48:17-26
      Expected: SBool (Increasing xs)
        Actual: 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)