Resolve type-system and unification related issues due to missing bottom type and TypeSystem::Unknown type annotations

[ironcev]

We have several open issues all coming from the same root cause, the fact that we miss the proper bottom type and that we are not passing the correct type annotations in TypeCheckContext. Here are some notable examples:

• "Verification failed: Struct field type mismatch" compiler error #5492
• Fix TyExpression::deterministically_aborts(), and eliminate its use during IR generation #5438
• Broken handling of type annotation for implicit/explicit return type checking #5518
• Internal compiler error with references, Option, and type ascription #5559
• Internal compiler error when all match branches return Never #5560
• Properly support divergence in DCA #5561
• Internal compiler error with structs, Option, and type ascription #5581

We had similar issues in the past, and always addressed them in isolation. This proposal calls for a systematic fix of all such issues by addressing the root cause.

Proposed steps are the following:

• Introduce the proper bottom type ! (Never)
• Remove the DeterministicallyAborts trait and all the calls to the deterministically_aborts method
• Pass the function return type as a part of the TypeCheckContext
• Double-check all the places where we set TypeInfo::Unknown as ctx type annotation
• Support ! and divergence in DCA
• Optional: Introduce functions like unreachable and todo

Introduce the proper bottom type

• Introduce built-in ! type with the semantic same to the Rust never type
• break, continue, and return have type !; consider this in compute_return_type_and_span
• Remove the hack that every empty enum behaves like bottom type in coersion
• Remove core::never::Never and check library functions that need to return ! (e.g., revert())

Remove the DeterministicallyAborts trait

DeterministicallyAborts actually compensates, or tries to compensate, for the missing bottom type. It is erroneous in its current implementation as #5438 explains, but there is no need to fix it. Once we properly introduce ! and diverging expression have it as a type, the consistent type system will automatically take care of the few places where deterministically_aborts was used.

• As a part if this step, we can check and eliminate double-unifications. (Type-checking of match branches is already done so I am striking it through as example. E.g. TyMatchBranch::type_check calls branch_ctx.unify_with_type_annotation() although the type check of the branch result already does the unification.)

Pass the function return type as a part of the context

@tritao already very well explained the need for this in #5518.

• As a part if this step we can remove should_unify from TyExpression::type_check.

Check places where TypeInfo::Unknown is set as type annotation

There are parts of semantic analysis where we want TypeInfo::Unknown to be set as ctx type annotation. Such places should always be documented in a comment. There are other places where we do set it currently, either:

1. because we were forced to due to the lacking of the proper bottom type
2. because we have a bug and need to properly consider which type actually needs to be passed

An example for 1) is #5492. The bug shows us that if and match expression should not remove the received type annotation from the context by setting it to Unknown. But once @vaivaswatha put the proper annotations to ctx passed to those expressions we've started getting tons of issues related to the missing bottom type.

An example for 2) are #5559 and #5581.

Support Never and divergence in DCA

Currently, __revert() and revert() are treated as special cases in the DCA. Once we get the ! type, this special treatment should be replaced by the generic analysis of all functions that return !.

Also, once all diverging expressions get ! as type, we can straightforwardly fully support divergence in all expressions (e.g., #5561).

Optional: Introduce functions like unreachable and todo

Once we have ! we could offer counterparts of Rust unreachable and todo macros as std functions. If I remember well this was even requested during the std audit. The function would simply log the message and revert.

However, we should think carefully about this. One day we want to have macros and having these as macros like in Rust would be more suitable. Without macros we cannot offer at the same time todo() without arguments and todo("With argument"). But then, we can start with functions and turn to macros later on. Decision needed, but nevertheless '!' opens door to this functionality.

[esdrubal]

Thanks for the detailed issue, I will look into this.

[esdrubal]

This was closed by mistake.