Bring back box inference?

[kyay10]

I understand it was removed to see how bad it would be without it, and it was determined that it wasn't so bad. Still, it'd be nice to have even as a compiler option (or maybe an in-file toggle like how Haskell does extensions to the language). Some advanced use cases need to use box a lottt due to lack of #271.

[jiribenes]

For what it's worth, the main disadvantage of box inference as we had it were the subpar, mostly incomprehensible error messages that only confused beginners and intermediate users of Effekt (cf. #807), while most of the uses of boxing were explicit anyways (or quite direct ones like binding a computation name to a value, val value = computation)

[kyay10]

That changes things quite a bit. If it never worked well, then yeah, removing it is pretty reasonable. It's likely not worth investing more time into improving it anyway

[jiribenes]

Personally, I am willing to bring it back, but I'd first like to have a nice story of how to teach it and how to make the error messages understandable. :)