[Ur] XML records from higher-order type classes

[Benjamin Barenblat]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi all,

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?

Thanks,
Benjamin
-----BEGIN PGP SIGNATURE-----

iQF8BAEBCgBmBQJVJxhWXxSAAAAAAC4AKGlzc3Vlci1mcHJAbm90YXRpb25zLm9w
ZW5wZ3AuZmlmdGhob3JzZW1hbi5uZXQ5OThCQjVEMTlDOEE3QjE3OUUwREFCODY5
RTczMDE0OUVCOTFDNTNCAAoJEJ5zAUnrkcU72AgH/0IAQmrVCPfLOEz48VUATAOg
jykkHM+jDWJCLMIXxMCjbRe5JgXANJIw9ue7WtP6XDCZ4Q8bD5T0yh4TQy0o32Hv
ez+JA83EeorNCYVmS/UCT2MXM+rYxjBC/ffKDjZsnu/yxpS+8qlytukKnUyQygJP
+BrxoUk4/HaYFx9UPdDIHX0oenPfUCAs/knvq+65aKsCANIepCAxTl2Z/byrq4m8
H5mW07KIv36e8AeMbvrnrLrG43hW19dKb0yWdPeXW3ZHlMCoGfCF35S7EE7zTA3H
B/CXCtHH5sZxDegjt7HCTdYdeto1L3cSAB7TQp44RYbXMzIJ/SJeba+ATlu31cU=
=a7Fo
-----END PGP SIGNATURE-----