<div dir="ltr"><div>Dear Ur Users,<br><br></div><div>I've written a function in Ur that typechecks, but that Ur's inference appears to fail on unless I explicitly specify type-parameters.<br><br></div><div>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.<br><br>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).<br><br></div><div>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.<br><br> 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.<br></div><div><br></div><div>--------------------------</div><div><br></div><div>fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ ts2] [ts2 ~ ts3] [ts1 ~ ts3]<br>           (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ ts3)) : $(ts1) =<br>    @fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) -> $(ts1)]<br>     (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r] <br>                  (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> $(ts1))<br>     [ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =><br>            f (z -- nm))<br>     (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1<br><br>fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]<br>       [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)<br>       (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ overlap ++ rest) =<br>    (i1 ++ (@recDif' ! ! ! fl i2 i1))<br><br>fun mergeDflInfer [more ::: {Type}] [overlap ::: {Type}] [rest ::: {Type}]<br>       [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)<br>       (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ overlap ++ rest) =<br>    (i1 ++ (@recDif' ! ! ! fl i2 i1))<br><br></div><div>--------------------------<br><br></div><div>I then attempt to run both of these functions on some simple examples:<br><br>-------------------------<br><br>val works = mergeDfl [[B = int]] {A = 1, B = 1} {B = 2, C = 3}<br>val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}<br><br>-----------------------<br>       </div><div><br></div><div>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:<br><br>----------------------<br><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in final record unification<br>Can't unify record constructors<br>Have:  [A = int, B = int]<br>Need:  <UNIF:U235::{Type}> ++ <UNIF:U234::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Stuck unifying these records after canceling matching pieces:<br>Have:  [A = int, B = int]<br>Need:  <UNIF:U234::{Type}> ++ <UNIF:U235::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Error in final record unification<br>Can't unify record constructors<br>Have:  [A = int]<br>Need:  <UNIF:U234::{Type}> ++ <UNIF:U233::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Stuck unifying these records after canceling matching pieces:<br>Have:  [A = int]<br>Need:  <UNIF:U233::{Type}> ++ <UNIF:U234::{Type}><br>yorix@DESKTOP-84OVJN9:~/winhome/Code/Lunes$ urweb lunes<br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Error in final record unification<br>Can't unify record constructors<br>Have:  [B = int, C = int]<br>Need:  <UNIF:U242::{Type}> ++ <UNIF:U241::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Stuck unifying these records after canceling matching pieces:<br>Have:  [B = int, C = int]<br>Need:  <UNIF:U241::{Type}> ++ <UNIF:U242::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Error in final record unification<br>Can't unify record constructors<br>Have:  [A = int, B = int]<br>Need:  <UNIF:U241::{Type}> ++ <UNIF:U240::{Type}><br>/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Stuck unifying these records after canceling matching pieces:<br>Have:  [A = int, B = int]<br>Need:  <UNIF:U240::{Type}> ++ <UNIF:U241::{Type}><br><br>----------------------<br><br>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.<br><br></div><div>Best,</div><div>Mario Alvarez<br></div></div>