Add regression tests for #13601, #13780, #13877
[ghc.git] / testsuite / tests / indexed-types / should_fail / T13877.stderr
1
2 T13877.hs:65:17: error:
3     • Couldn't match type ‘p xs’ with ‘Apply p xs’
4       Expected type: Sing x
5                      -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
6         Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
7     • In the expression: listElimPoly @(:->) @a @p @l
8       In an equation for ‘listElimTyFun’:
9           listElimTyFun = listElimPoly @(:->) @a @p @l
10     • Relevant bindings include
11         listElimTyFun :: Sing l
12                          -> (p @@ '[])
13                          -> (forall (x :: a) (xs :: [a]).
14                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
15                          -> p @@ l
16           (bound at T13877.hs:65:1)
17
18 T13877.hs:65:41: error:
19     • Expecting one more argument to ‘p’
20       Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
21     • In the type ‘p’
22       In the expression: listElimPoly @(:->) @a @p @l
23       In an equation for ‘listElimTyFun’:
24           listElimTyFun = listElimPoly @(:->) @a @p @l
25     • Relevant bindings include
26         listElimTyFun :: Sing l
27                          -> (p @@ '[])
28                          -> (forall (x :: a) (xs :: [a]).
29                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
30                          -> p @@ l
31           (bound at T13877.hs:65:1)