data UList : Type -> UniqueType where Nil : UList a (::) : a -> UList a -> UList a free : {a : UniqueType} -> a -> String free xs = "" showU : Show a => Borrowed (UList a) -> String showU xs = "[" ++ showU' xs ++ "]" where showU' : Borrowed (UList a) -> String showU' [] = "" showU' (x :: xs) = show x ++ ", " ++ showU xs foo : UList Int -> IO () foo xs = do -- let f = \x : Int => showU xs putStrLn $ free xs putStrLn $ f 42 xs return () where f : Int -> Borrowed (UList Int) -> String f x xs = showU xs