[Ur] Understanding Ur Inference Failure

[Adam Chlipala]

On 9/24/19 3:38 PM, Mario Alvarez wrote:
> The idea behind the function is the following: I want to construct a 
> record by combining together a record representing a set of 
> customization options with a record representing a set of defaults.
> [...]
> fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ 
> ts2] [ts2 ~ ts3] [ts1 ~ ts3]
>            (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ 
> ts3)) : $(ts1) =
>     @fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) -> 
> $(ts1)]
>      (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r]
>                   (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> 
> $(ts1))
> [ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =>
>             f (z -- nm))
>      (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1
>
> fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]
>     [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)
>     (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ 
> overlap ++ rest) =
>     (i1 ++ (@recDif' ! ! ! fl i2 i1))

Have you seen the triple-minus operator [---]?  I think it does your 
[recDif'], without the seemingly superfluous parameters.  You could 
replace the last line above with [i1 ++ (i2 --- overlap)].

Writing [recDif'] does seem to have been a useful exercise in Ur/Web 
metaprogramming!  Congrats on entering the elite club of people who have 
written new folds from scratch. >:)

> I then attempt to run both of these functions on some simple examples:
> [...]
> val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}
> [...]
> /mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in 
> final record unification
> Can't unify record constructors
> Have:  [A = int, B = int]
> Need:  <UNIF:U235::{Type}> ++ <UNIF:U234::{Type}>

In general, Ur inference isn't meant to solve equalities with just 
multiple unification variables concatenated together on one side.  You 
should always set things up so that there is at most one unification 
variable left when we get to unifying record types.  The underlying 
type-inference problem is undecidable, so we're fundamentally limited to 
using heuristics, and your case here didn't come up before to motivate a 
heuristic to support it.