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:
[x] #5492
[x] #5438
[x] #5518
[x] #5559
[x] #5560
[ ] #5561
[x] #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:
[x] Introduce the proper bottom type ! (Never)
[x] Remove the DeterministicallyAborts trait and all the calls to the deterministically_aborts method
[x] 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
[x] Introduce built-in ! type with the semantic same to the Rust never type
[x] break, continue, and return have type !; consider this in compute_return_type_and_span
[x] Remove the hack that every empty enum behaves like bottom type in coersion
[x] 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.
[x] 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:
because we were forced to due to the lacking of the proper bottom type
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.
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: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:
!
(Never)DeterministicallyAborts
trait and all the calls to thedeterministically_aborts
methodTypeCheckContext
TypeInfo::Unknown
asctx
type annotation!
and divergence in DCAunreachable
andtodo
Introduce the proper bottom type
!
type with the semantic same to the Rust never typebreak
,continue
, andreturn
have type!
; consider this incompute_return_type_and_span
core::never::Never
and check library functions that need to return!
(e.g.,revert()
)Remove the
DeterministicallyAborts
traitDeterministicallyAborts
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 wheredeterministically_aborts
was used.E.g.)TyMatchBranch::type_check
callsbranch_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.
should_unify
fromTyExpression::type_check
.Check places where
TypeInfo::Unknown
is set as type annotationThere are parts of semantic analysis where we want
TypeInfo::Unknown
to be set asctx
type annotation. Such places should always be documented in a comment. There are other places where we do set it currently, either:An example for 1) is #5492. The bug shows us that
if
andmatch
expression should not remove the received type annotation from the context by setting it toUnknown
. But once @vaivaswatha put the proper annotations toctx
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()
andrevert()
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
andtodo
Once we have
!
we could offer counterparts of Rustunreachable
andtodo
macros asstd
functions. If I remember well this was even requested during thestd
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 andtodo("With argument")
. But then, we can start with functions and turn to macros later on. Decision needed, but nevertheless '!' opens door to this functionality.