I have taken a bit of a break from it due to some other commitments. @rtfeldman is working on a better version of what is currently implemented.

My fault in the existing implementation was attempting to do it in a minimal number of passes relative to the rest of a compiler. Pulling it out to a separate pass as the original authors of the Lambda Set paper (Morphic) did makes it quite straightforward. I have a toy compiler (online playground) demonstrating it (sorry if it’s a bit opaque).

The main tip I would have is to do it in a separate pass once you already have already specialized all generic types, assuming you have a specializing compiler. At that point, run HM-style inference to determine how function calls are propagated in a program (this is actually equivalent to inferring polymorphic variants via the method described above). If you don’t have a specializing compiler, you give up being able to specialize all call sites but you can run the inference pass in or out of band to specialize calls that are known to be direct.

One last thing to note is that the lambda set-style stuff is disjoint from the type system, since lambda sets are directly encoding values, and not types per-se. So while you can reuse code between the two, fundamentally there is no reason to tie the type system to function-call specialization.

Sorry if this is still a bit opaque, happy to dive into more details as needed (here or in DM)!

Oh, that’s a much better, nuanced clarification! Pretty much addresses all the stuff in my comment.

Thanks for clarifying it. I would be curious to see the Reddit/HN comment (didn’t find it myself).

Also, the language that set the bar for high-quality error messages is Elm, which uses Hindley-Milner type inference and has a very fast compiler, and the Rust team cited Elm as the inspiration for the overhaul of their error messages which gave Rust a reputation for nice error messages:

Let me give you an example. Take this Rust code. The error message it produces:

error[E0597]: `ctx.field` does not live long enough
  --> src/main.rs:10:27
   |
9  | async fn async_fn(ctx: Context) {
   |                   --- binding `ctx` declared here
10 |     let mut field_guard = ctx.field.write().await;
   |                           ^^^^^^^^^--------
   |                           |
   |                           borrowed value does not live long enough
   |                           argument requires that `ctx.field` is borrowed for `'static`
11 |     tokio::task::spawn_blocking(move || blocking_fn(&mut field_guard)).await;
12 | }
   | - `ctx.field` dropped here while still borrowed

To me, the error message is hardly nice. I know what’s going on here: tokio::sync::RwLock::write() borrows ctx.field for lifetime 'a that’s limited to async_fn() scope. Whereas tokio::task::spawn_blocking() takes a closure which is 'static and thus all lifetimes within the closure must be 'static as well. A type error.

Now, look at how the explanation differs from the error message itself. There’s multiple problems here:

1. borrowed value does not live long enough points to ctx.field but there’s no borrowing (&) visible at this point in code. The actual borrowing is elsewhere — it’s the write(&self). It should show up in the error message IMO.
2. argument requires that ctx.field is borrowed for 'static doesn’t say, nor points to what “argument” exactly. There’s multiple arguments within the body of that function so it’s imprecise.
3. Finally, the biggest issue IMO, the error message doesn’t enumerate the reasoning chain the compiler performs so that a programmer could follow it and point out exactly the step at which it diverges from what’s happening inside of the programmer’s head. Ideally, it would look something like:

let mut field_guard = ctx.field.write().await;
                      ^^^^^^^^^--------
                      |
                      `ctx.field` is borrowed here for lifetime 'x
let mut field_guard = ctx.field.write().await;
        ^^^^^^^^^^^
        |
        field_guard's lifetime is 'x

tokio::task::spawn_blocking(move || blocking_fn(&mut field_guard)).await;
                                                ^^^^^^^^^^^^^^^^  
                                                |
                                                `field_guard` is borrowed here for lifetime 'y so 'x must live at least as long as 'y
tokio::task::spawn_blocking(move || blocking_fn(&mut field_guard)).await;
                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                                    |
                                    expression lifetime is 'y
tokio::task::spawn_blocking(move || blocking_fn(&mut field_guard)).await;
                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                            |
                            argument lifetime is 'y

fn spawn_blocking<F, R>(f: F) -> JoinHandle<R> where F: FnOnce() -> R + Send + 'static, R: Send + 'static
                        ^^^^
                        |
                        parameter lifetime is 'static
tokio::task::spawn_blocking(move || blocking_fn(&mut field_guard)).await;
                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                            |
                            argument lifetime is 'static
=> Thus 'y = 'static

=> Error: Unable to prove 'x lives at least as long as 'static