Result of type inference should not be trusted, but verified

[TomasMikula]

Unison's type inference is complex enough to not trust any particular implementation. However, once (untrusted) type inference fills in all the "gaps" (type applications, foralls), a straightforward (trusted) procedure could verify that the result of type inference is well-typed.

Aside: Programs without gaps also make it simpler to implement type-preserving manipulations.

Aside: Things like codebase format or hashes would no longer be influenced by type inference, since only gap-free programs would be hashed or stored in the codebase. This non-dependence on type inference would in turn allow alternative type inference implementations (because if one wants sufficiently different syntax, they might need a different type inference algorithm).

Prerequisites to implement such verification procedure include at least:

• [ ] type inference actually returning a result, i.e. Term without gaps;
• [ ] Terms ability to represent explicit type application and foralls (Λ-abstraction).

[atennapel]

Would you still store the original user defined term?

[TomasMikula]

Currently, it is not stored and the pretty printed version might differ (beyond just formatting) from the original source. So the problem exists regardless of this proposal. This proposal would just make the average discrepancy between source term and pretty printed codebase term bigger.

My personal opinion is:

• Eventually, no. But this is after there is an IDE that can hide inferable parts of the code and show them on request.
• In the meantime, why not. I already disliked that Unison ate some explicit foralls in my source code.

[aryairani]

This seems reasonable; do you happen to know where we are currently in terms of the pre-requisites you mentioned?