[Ur] XML records from higher-order type classes

[Adam Chlipala]

On 04/09/2015 08:39 PM, Benjamin Barenblat wrote:
> Anyway, I’m now stuck with another error:
>
> - ---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 x
> end
> - ---8<-----------------cut here----------------end----------------->8----

Probably putting a full type annotation on the formal parameter 
[witness] will solve this problem.  (Type inference for System F, a 
subset of Ur, is undecidable.)