Regression in `run` - fails to find the function to run

[atacratic]

Using trunk@7ceadd, run fails:

Possibly related commit here.

From slack:

Arya Irani (he/him) 1 hour ago
Just based on the output, it looks to me like the problem is a change in the type of suspended computations, but no corresponding change to main detection
Arya Irani (he/him) 1 hour ago
or maybe it’s just a pretty-printer improvement, and a bug in main detection

[jaredly]

Did you have --new-runtime enabled? I'm also seeing this with new-runtime, and it also refuses to run when invoked with ucm --new-runtime run foo.

The output from stack exec unison -- --new-runtime run .testbed.run_long:

Just (#568rs -> (({[#fgaev]} #568rs)))
.testbed.run_long is not of type '{IO} ()

If I remove --new-runtime, it executes fine.

[atacratic]

Interesting! I was using the old runtime...

[jaredly]

huh ok I'll make a separate ticket :)

[samgqroberts]

@seagreen and I looked into this and I believe we made some progress.

TL;DR: You can indeed run properly typed terms on trunk currently, but something seems off with automatic type inference - it gives a term as simple as '(printLine "hello") an unrunnable type.

---

We confirmed that a term defined like this:

main = '(printLine "hello")

runs successfully on the M1m release, but gives a "this term has improper type" error on trunk (or, before #1814, a "i can't find this term" error).

We found that the Typechecker.isSubtype call in HandleInput.addRunMain that compares mainType, the most general runnable type, and ty, the type of the given term to run, is involved in the discrepancy - it returns that the ty of main is a subtype of mainType (as expected) on M1m, but not on trunk.

On trunk, we printed out the value of mainType:

(User "a". #568rs -> ({[#fgaev]} Var User "a"))

("for all a, a function from unit to a decorated with the IO ability")
and ty:

(User "()". (User "g". Var User "()" -> ({[Var User "g",#fgaev]} #568rs)))

The additional "g" added to the signature and ability list seems to get at the issue here. Since this inferred type seemed more complex than required, we added an explicit type signature to the term:

main : '{IO} ()
main = '(printLine "hello")

And found that run now works as expected. The ty printed out with the explicit type signature is now:

#568rs -> ({[#fgaev]} #568rs)

So it looks like the user can still run terms on trunk, as long as they're properly typed, and this issue specifically has to do with the automatic inference of runnable types. I think it's safe to say that a term defined as '(printLine "hello") ought to be runnable.

[pchiusano]

@stew do you recall why we tried to generalize the type of main? I think it used to be hardcoded to just '{IO} () and we changed that for some reason. I was thinking we could just revert that back in MainTerm.hs.

[sullyj3]

In Rust, you can return a Result from main, or anything that implements std::process::Termination. Is it possible it was to support a feature like this in the future?