Force occurs check for introduced types after checking annotated bodies

The current type inference scheme is such that we first introduce the
types for annotation functions, then check their bodies without
additional re-generalization. As part of generalization, we also perform
occurs checks to fix-up recursive tag unions.

However, type annotations can contain type inference variables that are
neither part of the generalization scheme, nor are re-generalized later
on, and in fact end up forming a closure of a recursive type. If we do
not catch and break such closures into recursive types, things go bad
soon after in later stages of the compiler.

To deal with this, re-introduce the values of recursive values after we
check their definitions, forcing an occurs check. This introduction is
benign because we already generalized appropriate type variables anyway.
Though, the introduction is somewhat unnecessary, and I have ideas on
how to make all of this simpler and more performant. That will come in
the future.

crates/compiler/constrain/src/expr.rs

@@ -3435,6 +3435,10 @@ fn constraint_recursive_function(
             rigid_info.constraints.push({
                 // Solve the body of the recursive function, making sure it lines up with the
                 // signature.
+                //
+                // This happens when we're checking that the def of a recursive function actually
+                // aligns with what the (mutually-)recursive signature says, so finish
+                // generalization of the function.
                 let rigids = new_rigid_variables;
                 let flex = def_pattern_state
                     .vars
@@ -3444,7 +3448,16 @@ fn constraint_recursive_function(
                 constraints.let_constraint(
                     rigids,
                     flex,
-                    [], // no headers introduced (at this level)
+                    // Although we will have already introduced the headers of the def in the
+                    // outermost scope when we introduced the rigid variables, we now re-introduce
+                    // them to force an occurs check and appropriate fixing, since we might end up
+                    // inferring recursive types at inference variable points. E.g.
+                    //
+                    //   f : _ -> _
+                    //   f = \F c -> F (List.map f c)
+                    //
+                    // TODO: I (Ayaz) believe we can considerably simplify all this.
+                    def_pattern_state.headers.clone(),
                     def_con,
                     Constraint::True,
                 )

crates/compiler/solve/tests/solve_expr.rs

@@ -8336,4 +8336,20 @@ mod solve_expr {
         "###
         )
     }
+
+    #[test]
+    fn solve_inference_var_in_annotation_requiring_recursion_fix() {
+        infer_queries!(indoc!(
+            r#"
+            app "test" provides [translateStatic] to "./platform"
+
+            translateStatic : _ -> _
+            translateStatic = \Element c ->
+            #^^^^^^^^^^^^^^^{-1}
+                Element (List.map c translateStatic)
+            "#
+        ),
+        @"translateStatic : [Element (List a)] as a -[[translateStatic(0)]]-> [Element (List b)]* as b"
+        )
+    }
 }