[Ur] show t

[Adam Chlipala]

Gergely Buday wrote:
> I wanted to express that an argument is show-able by a proper  t ->
> string function. It seems that I had success with the function show_
> but not with the main function. Why does this simple code leads to a
> too difficult unification problem?
>
> - Gergely
>
> $ cat bar.ur
> fun show_ [t] (arg : show t) =
>      return<xml>{[arg]}</xml>
>    

Something is already strange with this definition, so I suggest fixing 
that first and seeing if the problem recurs.  The code above tries to 
show the witness of membership in the type class [show].  What you want 
instead is to use that witness to render a particular value of type 
[t].  You probably meant this:

fun show_ [t] (_ : show t) (arg : t) =
     return <xml>{[arg]}</xml>

BTW, this function is already in the standard library and is present in 
the default context, with the name [txt], with a more general type.