expected

unique001a.idr:35:16-43:50:
   |
35 | showStuff xs = do
   |                ~~ ...
Type mismatch between
        Int -> String
and
        UniqueType (Int -> String)

unique001a.idr:46:17-54:28:
   |
46 | showStuff' xs = do
   |                 ~~ ...
Type mismatch between
        Int -> String
and
        UniqueType (Int -> String)

unique001a.idr:57:17-62:33:
   |
57 | showThings xs = do
   |                 ~~ ...
Type mismatch between
        UniqueType (Int -> String)
and
        Int -> String

unique001b.idr:18:19-42:
   |
18 | showU (x :: xs) = show x ++ "," ++ free xs
   |                   ~~~~~~~~~~~~~~~~~~~~~~~~
Borrowed name xs must not be used on RHS

unique001c.idr:47:14-62:
   |
47 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
   |              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Unique name f is used more than once

unique001d.idr:4:18:
  |
4 | steal (Read x) = x
  |                  ^
Borrowed name x must not be used on RHS

unique001e.idr:4:12-40:
  |
4 |      Nil : {a : UniqueType} -> BadList a
  |            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Constructor Main.Nil has a UniqueType, but the data type does not

unique002.idr:17:10-20:19:
   |
17 | foo xs = do -- let f = \x : Int => showU xs
   |          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
Unique name xs is used more than once

unique002a.idr:17:10-20:19:
   |
17 | foo xs = do let f = \x : Int => showU xs
   |          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
Type mismatch between
        Int -> String
and
        UniqueType (Int -> String)

unique003.idr:20:10-24:19:
   |
20 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context
   |          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
Type mismatch between
        Int -> String
and
        UniqueType (Int -> String)