Respect variable type ascription when initializer has type Never (#6911)

## Description

Fixes #6391.

This PR fixes an issue with variable declarations whose initializers
diverge because they contain `return`, `continue` or `break`
expressions. In this case the initializer typechecks to `Never`, and the
variable is inferred to have type `Never` in the subsequent
(unreachable) code:

```
let mut x = return;
x = 42; // Illegal, since x has type Never
```

The problem is that this is the case even when the variable declaration
has a type ascription:

```
let mut x : u32 = return;
x = 42; // Should be legal, since x has the type ascription u32
```

As part of the fix there is another slight change of behavior for code
blocks that diverge. Until now the type of a code block has been
determined based on whether it contains a diverging expression:

```
match { return; true } // Considered to have type Never because of `return;`
{ 
   // Type Never does not have a constructor
}
```

We now determine the type of a code block based on its implicit return:

```
match { return; true }
{
    // Type Boolean has two constructors
    true => ...,
    false => ...,
}
```

In principle this is a breaking change, but the only change in behavior
is in code blocks that contain a `return`, `break` or `continue`, and
then contains dead code after that expression, so I can't imagine anyone
will be affected by it.

## Checklist

- [x] I have linked to any relevant issues.
- [x] I have commented my code, particularly in hard-to-understand
areas.
- [x] I have updated the documentation where relevant (API docs, the
reference, and the Sway book).
- [ ] If my change requires substantial documentation changes, I have
[requested support from the DevRel
team](https://github.com/FuelLabs/devrel-requests/issues/new/choose)
- [x] I have added tests that prove my fix is effective or that my
feature works.
- [x] I have added (or requested a maintainer to add) the necessary
`Breaking*` or `New Feature` labels where relevant.
- [x] I have done my best to ensure that my PR adheres to [the Fuel Labs
Code Review
Standards](https://github.com/FuelLabs/rfcs/blob/master/text/code-standards/external-contributors.md).
- [x] I have requested a review from the relevant team or maintainers.

---------

Co-authored-by: Joshua Batty <joshpbatty@gmail.com>
Co-authored-by: IGI-111 <igi-111@protonmail.com>

Author: 3 people

sway-core/src/language/ty/declaration/declaration.rs

@@ -734,7 +734,7 @@ impl TyDecl {
         let type_engine = engines.te();
         let decl_engine = engines.de();
         let type_id = match self {
-            TyDecl::VariableDecl(decl) => decl.body.return_type,
+            TyDecl::VariableDecl(decl) => decl.return_type,
             TyDecl::FunctionDecl(FunctionDecl { decl_id, .. }) => {
                 let decl = decl_engine.get_function(decl_id);
                 decl.return_type.type_id

sway-core/src/semantic_analysis/ast_node/declaration/variable.rs

@@ -49,37 +49,44 @@ impl ty::TyVariableDecl {
                 None,
             )
             .unwrap_or_else(|err| type_engine.id_of_error_recovery(err));
+
         let mut ctx = ctx
             .with_type_annotation(type_ascription.type_id)
             .with_help_text(
                 "Variable declaration's type annotation does not match up \
-                        with the assigned expression's type.",
+                 with the assigned expression's type.",
             );
+
         let result = ty::TyExpression::type_check(handler, ctx.by_ref(), &var_decl.body);
         let body = result
             .unwrap_or_else(|err| ty::TyExpression::error(err, var_decl.name.span(), engines));
 
-        // TODO: Integers shouldn't be anything special. RHS expressions should be written in
-        //       a way to always use the context provided from the LHS, and if the LHS is
-        //       an integer, RHS should properly unify or type check should fail.
-        //       Remove this special case as a part of the initiative of improving type inference.
-        // Integers are special in the sense that we can't only rely on the type of `body`
-        // to get the type of the variable. The type of the variable *has* to follow
-        // `type_ascription` if `type_ascription` is a concrete integer type that does not
-        // conflict with the type of `body` (i.e. passes the type checking above).
-        let return_type = match &*type_engine.get(type_ascription.type_id) {
-            TypeInfo::UnsignedInteger(_) => type_ascription.type_id,
-            _ => match &*type_engine.get(body.return_type) {
-                // If RHS type check ends up in an error we want to use the
-                // provided type ascription as the variable type. E.g.:
-                //   let v: Struct<u8> = Struct<u64> { x: 0 }; // `v` should be "Struct<u8>".
-                //   let v: ExistingType = non_existing_identifier; // `v` should be "ExistingType".
-                //   let v = <some error>; // `v` will remain "{unknown}".
-                // TODO: Refine and improve this further. E.g.,
-                //   let v: Struct { /* MISSING FIELDS */ }; // Despite the error, `v` should be of type "Struct".
-                TypeInfo::ErrorRecovery(_) => type_ascription.type_id,
-                _ => body.return_type,
-            },
+        // Determine the type of the variable going forward.  Typically this is the type of the RHS,
+        // but in some cases we need to use the type ascription instead.
+        // TODO: We should not have these special cases. The typecheck expressions should be written
+        // in a way to always use the context provided by the LHS, and use the unified type of LHS
+        // and RHS as the return type of the RHS.  Remove this special case as a part of the
+        // initiative of improving type inference.
+        let return_type = match (&*type_engine.get(type_ascription.type_id), &*type_engine.get(body.return_type)) {
+            // Integers: We can't rely on the type of the RHS to give us the correct integer
+            // type, so the type of the variable *has* to follow `type_ascription` if
+            // `type_ascription` is a concrete integer type that does not conflict with the type
+            // of `body` (i.e. passes the type checking above).
+            (TypeInfo::UnsignedInteger(_), _) |
+            // Never: If the RHS resolves to Never, then any code following the declaration is
+            // unreachable. If the variable is used later on, then it should be treated as
+            // having the same type as the type ascription.
+            (_, TypeInfo::Never) |
+            // If RHS type check ends up in an error we want to use the
+            // provided type ascription as the variable type. E.g.:
+            //   let v: Struct<u8> = Struct<u64> { x: 0 }; // `v` should be "Struct<u8>".
+            //   let v: ExistingType = non_existing_identifier; // `v` should be "ExistingType".
+            //   let v = <some error>; // `v` will remain "{unknown}".
+            // TODO: Refine and improve this further. E.g.,
+            //   let v: Struct { /* MISSING FIELDS */ }; // Despite the error, `v` should be of type "Struct".
+            (_, TypeInfo::ErrorRecovery(_)) => type_ascription.type_id,
+            // In all other cases we use the type of the RHS.
+            _ => body.return_type,
         };
 
         if !ctx.code_block_first_pass() {

sway-core/src/semantic_analysis/ast_node/expression/typed_expression.rs

@@ -2427,7 +2427,7 @@ impl ty::TyExpression {
                                         ));
                                     }
 
-                                    break (name, variable_decl.body.return_type);
+                                    break (name, variable_decl.return_type);
                                 }
                                 TyDecl::ConstantDecl(constant_decl) => {
                                     let constant_decl =

test/src/e2e_vm_tests/test_programs/should_pass/language/diverging_exprs/src/main.sw

@@ -88,6 +88,7 @@ fn diverge_in_match_condition() -> u64 {
         return 5;
         true
     } {
+        _ => 42,
     }
 }
 

test/src/e2e_vm_tests/test_programs/should_pass/language/unify_never/Forc.lock

@@ -0,0 +1,13 @@
+[[package]]
+name = "core"
+source = "path+from-root-DFCFC85C94C0C9BD"
+
+[[package]]
+name = "std"
+source = "path+from-root-DFCFC85C94C0C9BD"
+dependencies = ["core"]
+
+[[package]]
+name = "unify_never"
+source = "member"
+dependencies = ["std"]

test/src/e2e_vm_tests/test_programs/should_pass/language/unify_never/Forc.toml

@@ -0,0 +1,8 @@
+[project]
+authors = ["Fuel Labs <contact@fuel.sh>"]
+license = "Apache-2.0"
+name = "unify_never"
+entry = "main.sw"
+
+[dependencies]
+std = { path = "../../../../reduced_std_libs/sway-lib-std-assert" }

test/src/e2e_vm_tests/test_programs/should_pass/language/unify_never/src/main.sw

@@ -0,0 +1,19 @@
+script;
+
+// Test of unification of the Never type
+
+fn test_1(){
+    let mut v1: u32 = 1;
+    v1 = return;
+}
+
+fn test_2(){
+    let mut v2: u32 = return;
+    v2 = 1;
+}
+
+
+fn main() {
+    test_1();
+    test_2();
+}

test/src/e2e_vm_tests/test_programs/should_pass/language/unify_never/test.toml

@@ -0,0 +1,2 @@
+category = "compile"
+expected_warnings = 1