[Ur] Understanding Ur Inference Failure

[Mario Alvarez]

Dear Ur Users,

I've written a function in Ur that typechecks, but that Ur's inference
appears to fail on unless I explicitly specify type-parameters.

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.

I have a record type (overlap ++ rest) representing the defaults, and
another record type (more ++ overlap) representing the customizations. The
idea is that the "more" and "overlap" fields will be taken from the
customization parameter, the "rest" fields will be taken from the default
parameter, and the result will be of type (more ++ overlap ++ rest).

I have implemented this as the following, using record folds to define a
helper function "recDif" that calculates the "rest" part of the defaults
parameter, given the customization and defaults.

Note that I define two versions of mergeDfl, one which expects the overlap
to be given explicitly as a type parameter, and the other which attempts to
infer it. Otherwise the two versions are identical.

--------------------------

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))

fun mergeDflInfer [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))

--------------------------

I then attempt to run both of these functions on some simple examples:

-------------------------

val works = mergeDfl [[B = int]] {A = 1, B = 1} {B = 2, C = 3}
val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}

-----------------------

If we run the first version of merged ("mergeDfl"), supplying the "overlap"
type parameter as follows, UrWeb accepts it ("val works"). However, if we
run the second modified version of merged ("mergeDflInfer") and attempt to
force UrWeb to infer the overlap ("val fails"), UrWeb rejects it with the
following error:

----------------------

/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}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int, B = int]
Need:  <UNIF:U234::{Type}> ++ <UNIF:U235::{Type}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Error in final
record unification
Can't unify record constructors
Have:  [A = int]
Need:  <UNIF:U234::{Type}> ++ <UNIF:U233::{Type}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int]
Need:  <UNIF:U233::{Type}> ++ <UNIF:U234::{Type}>
yorix at DESKTOP-84OVJN9:~/winhome/Code/Lunes$ urweb lunes
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Error in final
record unification
Can't unify record constructors
Have:  [B = int, C = int]
Need:  <UNIF:U242::{Type}> ++ <UNIF:U241::{Type}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Stuck unifying
these records after canceling matching pieces:
Have:  [B = int, C = int]
Need:  <UNIF:U241::{Type}> ++ <UNIF:U242::{Type}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Error in final
record unification
Can't unify record constructors
Have:  [A = int, B = int]
Need:  <UNIF:U241::{Type}> ++ <UNIF:U240::{Type}>
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int, B = int]
Need:  <UNIF:U240::{Type}> ++ <UNIF:U241::{Type}>

----------------------

Is Ur's inference algorithm simply unable to infer the overlap in a
situation like this, or am I doing something wrong? I am using Ur version
20190217.

Best,
Mario Alvarez
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20190924/8f2254ff/attachment.html>