summaryrefslogtreecommitdiff
path: root/testsuite/tests/patsyn/should_fail/T15695.stderr
blob: 82398e15a7cf7be70706433cadd371421339d1da (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
37
38
39
40
41
42
43
44
45
46

T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
    • Could not deduce: a2 ~ NA 'VO
      from the context: ((* -> * -> *) ~ (k -> k1 -> *), Either ~~ f,
                         ctx ~~ (a2 ':&: (a3 ':&: 'E)), f a2 ~~ f1, f1 a3 ~~ a4)
        bound by a pattern with pattern synonym:
                   ASSO :: forall kind (a :: kind) (b :: Ctx kind).
                           () =>
                           forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1 -> ks1)
                                  (a2 :: k1) a3.
                           (kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
                            f a1 ~~ f1, f1 a2 ~~ a3) =>
                           a3 -> ApplyT kind a b,
                 in an equation for ‘from'’
        at T15695.hs:39:8-21
      Expected: a4
        Actual: Either (NA 'VO) a3
      ‘a2’ is a rigid type variable bound by
        a pattern with pattern synonym:
          ASSO :: forall kind (a :: kind) (b :: Ctx kind).
                  () =>
                  forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1 -> ks1)
                         (a2 :: k1) a3.
                  (kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
                   f a1 ~~ f1, f1 a2 ~~ a3) =>
                  a3 -> ApplyT kind a b,
        in an equation for ‘from'’
        at T15695.hs:39:8-21
    • In the pattern: Left a
      In the pattern: ASSO (Left a)
      In an equation for ‘from'’: from' (ASSO (Left a)) = Here (a :* Nil)
    • Relevant bindings include
        from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
          (bound at T15695.hs:39:1)

T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)]
    • Couldn't match type: a0 : as0
                     with: '[]
      Expected: NS (NP NA) '[ '[ 'VO]]
        Actual: NS (NP NA) ('[ 'VO] : a0 : as0)
    • In the expression: There (Here undefined)
      In an equation for ‘from'’:
          from' (ASSO (Right b)) = There (Here undefined)
    • Relevant bindings include
        from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
          (bound at T15695.hs:39:1)