Merge remote-tracking branch 'origin/trunk' into more-tyck

compiler/constrain/src/expr.rs

@@ -1729,30 +1729,27 @@ fn constrain_def(
     }
 }
 
+/// Create a let-constraint for a non-recursive def.
+/// Recursive defs should always use `constrain_recursive_defs`.
 pub fn constrain_def_make_constraint(
     constraints: &mut Constraints,
-    new_rigid_variables: impl Iterator<Item = Variable>,
-    new_infer_variables: impl Iterator<Item = Variable>,
-    expr_con: Constraint,
-    body_con: Constraint,
+    annotation_rigid_variables: impl Iterator<Item = Variable>,
+    annotation_infer_variables: impl Iterator<Item = Variable>,
+    def_expr_con: Constraint,
+    after_def_con: Constraint,
     def_pattern_state: PatternState,
 ) -> Constraint {
-    let and_constraint = constraints.and_constraint(def_pattern_state.constraints);
+    let all_flex_variables = (def_pattern_state.vars.into_iter()).chain(annotation_infer_variables);
 
-    let def_con = constraints.let_constraint(
-        [],
-        new_infer_variables,
-        [], // empty, because our functions have no arguments!
-        and_constraint,
-        expr_con,
-    );
+    let pattern_constraints = constraints.and_constraint(def_pattern_state.constraints);
+    let def_pattern_and_body_con = constraints.and_constraint([pattern_constraints, def_expr_con]);
 
     constraints.let_constraint(
-        new_rigid_variables,
-        def_pattern_state.vars,
+        annotation_rigid_variables,
+        all_flex_variables,
         def_pattern_state.headers,
-        def_con,
-        body_con,
+        def_pattern_and_body_con,
+        after_def_con,
     )
 }
 
@@ -2126,15 +2123,35 @@ pub fn rec_defs_help(
         }
     }
 
-    let flex_constraints = constraints.and_constraint(flex_info.constraints);
-    let inner_inner = constraints.let_constraint(
+    // Strategy for recursive defs:
+    // 1. Let-generalize the type annotations we know; these are the source of truth we'll solve
+    //    everything else with. If there are circular type errors here, they will be caught during
+    //    the let-generalization.
+    // 2. Introduce all symbols of the untyped defs, but don't generalize them yet. Now, solve
+    //    the untyped defs' bodies. This way, when checking something like
+    //      f = \x -> f [ x ]
+    //    we introduce `f: b -> c`, then constrain the call `f [ x ]`,
+    //    forcing `b -> c ~ List b -> c` and correctly picking up a recursion error.
+    //    Had we generalized `b -> c`, the call `f [ x ]` would have been generalized, and this
+    //    error would not be found.
+    // 3. Now properly let-generalize the untyped body defs, since we now know their types and
+    //    that they don't have circular type errors.
+    // 4. Solve the bodies of the typed body defs, and check that they agree the types of the type
+    //    annotation.
+    // 5. Solve the rest of the program that happens after this recursive def block.
+
+    // 2. Solve untyped defs without generalization of their symbols.
+    let untyped_body_constraints = constraints.and_constraint(flex_info.constraints);
+    let untyped_def_symbols_constr = constraints.let_constraint(
         [],
         [],
         flex_info.def_types.clone(),
         Constraint::True,
-        flex_constraints,
+        untyped_body_constraints,
     );
 
+    // an extra constraint that propagates information to the solver to check for invalid recursion
+    // and generate a good error message there.
     let (loc_symbols, expr_regions): (Vec<_>, Vec<_>) = defs
         .iter()
         .flat_map(|def| {
@@ -2145,22 +2162,21 @@ pub fn rec_defs_help(
 
     let cycle_constraint = constraints.check_cycle(loc_symbols, expr_regions, cycle_mark);
 
-    let rigid_constraints = {
-        let mut temp = rigid_info.constraints;
-        temp.push(cycle_constraint);
-        temp.push(body_con);
-
-        constraints.and_constraint(temp)
-    };
+    let typed_body_constraints = constraints.and_constraint(rigid_info.constraints);
+    let typed_body_and_final_constr =
+        constraints.and_constraint([typed_body_constraints, cycle_constraint, body_con]);
 
+    // 3. Properly generalize untyped defs after solving them.
     let inner = constraints.let_constraint(
         [],
         flex_info.vars,
         flex_info.def_types,
-        inner_inner,
-        rigid_constraints,
+        untyped_def_symbols_constr,
+        // 4 + 5. Solve the typed body defs, and the rest of the program.
+        typed_body_and_final_constr,
     );
 
+    // 1. Let-generalize annotations we know.
     constraints.let_constraint(
         rigid_info.vars,
         [],