[Ur] XML records from higher-order type classes

[Adam Chlipala]

In Ur, types and values are in different namespaces.  The [a] near the 
end is a different [a] from the one bound as a formal argument!  In 
particular, it is resolving to the <a> tag from the standard library.

You probably meant to pass just [x].  (The [@] prefix in Ur only makes 
type-class witnesses and folders explicit.  It doesn't make type 
parameters explicit.)  An explicit type-level argument to a value-level 
function is passed inside square brackets.

On 04/09/2015 08:24 PM, Benjamin Barenblat wrote:
> After some discussion on #ur, I’ve tried to implement a container class
> à la Haskell’s Functor.
>
> - ---8<-----------------cut here----------------start--------------->8----
> structure Container : sig
>      class container :: (Type -> Type) -> Type
>      val inject : a ::: Type -> f ::: (Type -> Type)
>                   -> container f
>                   -> a -> f a
> end = struct
>      con container f = {Inject : a ::: Type -> a -> f a}
>      fun inject [a] [f] witness x = @witness.Inject a x
> end
> - ---8<-----------------cut here----------------end----------------->8----
>
> However, trying to compile this produces a nasty error:
>
>      container.ur:8:4: (to 8:54) Error in final record unification
>      Can't unify record constructors
>         Have:
>      <UNIF:G::{Type}> ++
>       [Inject =
>         ({} ->
>           tag
>            ([Link = transaction (xml ([Html = ()]) ([]) ([])), Href = url,
>               Target = string, Rel = string, Data = data_attr, Id = id,
>               Title = string, Role = string, Onblur = transaction {},
>               Onfocus = transaction {},
>      […]
>
> Why does urweb think that XML tags are involved here?