testsuite/tests/typecheck/no_skolem_info/T14040.stderr


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
47
48
49
50
51
52
53
54
55
56
57
58
59
60


T14040.hs:27:46: error: [GHC-46956]
    • Couldn't match kind ‘k1’ with ‘WeirdList z’
      Expected kind ‘WeirdList k1’,
        but ‘xs’ has kind ‘WeirdList (WeirdList z)’
    • because kind variable ‘z’ would escape its scope
    This (rigid, skolem) kind variable is bound by
      an explicit forall (z :: Type) (x :: z)
                         (xs :: WeirdList (WeirdList z))
      at T14040.hs:26:26-77
    • In the second argument of ‘p’, namely ‘xs’
      In the type ‘Sing wl
                   -> (forall (y :: Type). p _ WeirdNil)
                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
                         -> p _ wl’
      In the type signature:
        elimWeirdList :: forall (a :: Type)
                                (wl :: WeirdList a)
                                (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl
                                                                                     -> (forall (y :: Type).
                                                                                         p _ WeirdNil)
                                                                                        -> (forall (z :: Type)
                                                                                                   (x :: z)
                                                                                                   (xs :: WeirdList (WeirdList z)).
                                                                                            Sing x
                                                                                            -> Sing xs
                                                                                               -> p _ xs
                                                                                                  -> p _ (WeirdCons x xs))
                                                                                           -> p _ wl

T14040.hs:28:27: error: [GHC-46956]
    • Couldn't match kind ‘k0’ with ‘z’
      Expected kind ‘WeirdList k0’,
        but ‘WeirdCons x xs’ has kind ‘WeirdList z’
    • because kind variable ‘z’ would escape its scope
    This (rigid, skolem) kind variable is bound by
      an explicit forall (z :: Type) (x :: z)
                         (xs :: WeirdList (WeirdList z))
      at T14040.hs:26:26-77
    • In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
      In the type ‘Sing wl
                   -> (forall (y :: Type). p _ WeirdNil)
                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
                         -> p _ wl’
      In the type signature:
        elimWeirdList :: forall (a :: Type)
                                (wl :: WeirdList a)
                                (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl
                                                                                     -> (forall (y :: Type).
                                                                                         p _ WeirdNil)
                                                                                        -> (forall (z :: Type)
                                                                                                   (x :: z)
                                                                                                   (xs :: WeirdList (WeirdList z)).
                                                                                            Sing x
                                                                                            -> Sing xs
                                                                                               -> p _ xs
                                                                                                  -> p _ (WeirdCons x xs))
                                                                                           -> p _ wl