git.iko.soy/Idris-dev
on cb90bf8 help sign in
Idris-dev/test/unique004/expected
75 lines 1.8 kB history raw
1unique001a.idr:35:16-43:50:
2 |
335 | showStuff xs = do
4 | ~~ ...
5Type mismatch between
6 Int -> String
7and
8 UniqueType (Int -> String)
10unique001a.idr:46:17-54:28:
11 |
1246 | showStuff' xs = do
13 | ~~ ...
14Type mismatch between
15 Int -> String
16and
17 UniqueType (Int -> String)
19unique001a.idr:57:17-62:33:
20 |
2157 | showThings xs = do
22 | ~~ ...
23Type mismatch between
24 UniqueType (Int -> String)
25and
26 Int -> String
28unique001b.idr:18:19-42:
29 |
3018 | showU (x :: xs) = show x ++ "," ++ free xs
31 | ~~~~~~~~~~~~~~~~~~~~~~~~
32Borrowed name xs must not be used on RHS
34unique001c.idr:47:14-62:
35 |
3647 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
37 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
38Unique name f is used more than once
40unique001d.idr:4:18:
41 |
424 | steal (Read x) = x
43 | ^
44Borrowed name x must not be used on RHS
46unique001e.idr:4:12-40:
47 |
484 | Nil : {a : UniqueType} -> BadList a
49 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
50Constructor Main.Nil has a UniqueType, but the data type does not
52unique002.idr:17:10-20:19:
53 |
5417 | foo xs = do -- let f = \x : Int => showU xs
55 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
56Unique name xs is used more than once
58unique002a.idr:17:10-20:19:
59 |
6017 | foo xs = do let f = \x : Int => showU xs
61 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
62Type mismatch between
63 Int -> String
64and
65 UniqueType (Int -> String)
67unique003.idr:20:10-24:19:
68 |
6920 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context
70 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
71Type mismatch between
72 Int -> String
73and
74 UniqueType (Int -> String)