[Ur] Record subtype constraint

[Karn Kallio]

I thought to express record subtyping using Ur/Web's disjointness constraints 
and symmetric concatenation.

This works:

fun subrecord [super :: {Type}] [evidence ::: {Type}] [super ~ evidence] (sub 
: $(super ++ evidence)) = sub

con supertype :: {Type} = [One = string, Two = string]

val subrec = subrecord [supertype] {One = "foo", Two = "bar", Three = "baz"}

(* ok, doesn't compile *)
val subrec' = subrecord [supertype] {One = "foo", Three = "baz"}

The Ur/Web compiler automatically finds the "evidence" showing the value 
argument has a record subtype or gives a compile error if it is not a subtype.

But I thought a better way to witness that a given record is a subtype would 
be to return the portion with the supertype, so we can use the result in 
contexts expecting the supertype.

However, this does not compile:

fun subrecord' [super :: {Type}] [extension ::: {Type}] [super ~ extension] 
(fl : folder super) (sub : $(super ++ extension))
  = fl [fn (r :: {Type}) => ($(super ++ extension) -> $r)]
       (fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] acc src => {nm = 
sub.nm} ++ acc (src))
       (fn _ => {}) sub

val subrec' = subrecord' [supertype] {One = "foo", Two = "bar", Three = "baz"}

giving error:

f.ur:11:4-11:6: Expression is not a constructor function
Expression:  fl
      Type:  Top.folder[[Type]] super
f.ur:15:26-15:35: Substitution in constructor is blocked by a too-deep 
unification variable
Replacement:  [#One = string, #Two = string]
       Body: 
extension ::: {Type} ->
 [UNBOUND_REL1 ~ extension] =>
  ((Top.folder[[Type]] UNBOUND_REL1) ->
    ($(UNBOUND_REL1 ++ extension) -> <UNIF:F::Type>))


which looks like the unification does not get into the [fn (r :: {Type}) => 
($(super ++ extension) -> $r)] parameter to fl.

What is happening?  Is the compile error due to incompleteness in the 
unification implementation ( related to folder inference maybe? ) or have I 
written nonsense ( and the compiler of course rejects it )?