Allow unification of general and specific Ty inference var kinds

The recursive solver would fail on these new tests without this change.

Author: AzureMarker

chalk-solve/src/infer/unify.rs

@@ -115,7 +115,30 @@ impl<'t, I: Interner> Unifier<'t, I> {
                     .expect("unification of two unbound variables cannot fail"))
             }
 
-            // Tried to unify mis-matching inference variables (not caught by prior match arm)
+            // General inference variables can be unified with more specific
+            // inference variables, but they need to inherit the specific
+            // variable's type kind. The general_var kind != the specific_var
+            // kind because of the prior match arm
+            (
+                &TyData::InferenceVar(general_var, TyKind::General),
+                specific_ty_data @ &TyData::InferenceVar(_, _)
+            )
+            | (
+                specific_ty_data @ &TyData::InferenceVar(_, _),
+                &TyData::InferenceVar(general_var, TyKind::General)
+            ) => {
+                let specific_ty = specific_ty_data.clone().intern(interner);
+                self.table
+                    .unify
+                    .unify_var_value(general_var, InferenceValue::from_ty(interner, specific_ty.clone()))
+                    .unwrap();
+
+                debug!("unify_ty_ty: general kinded var {:?} set to {:?}", general_var, specific_ty);
+                Ok(())
+            }
+
+            // Tried to unify inference variables with mis-matching specific type kinds (not caught
+            // by prior match arms)
             (
                 &TyData::InferenceVar(_, kind1),
                 &TyData::InferenceVar(_, kind2),

tests/test/numerics.rs

@@ -119,3 +119,53 @@ fn float_ambiguity() {
         }
     }
 }
+
+/// Integer/float type kinds are just specialized type kinds, so they can unify
+/// with general type kinds.
+#[test]
+fn integer_and_float_are_specialized_ty_kinds() {
+    test! {
+        program {}
+
+        goal {
+            exists<T, int N> {
+                T = N, N = usize
+            }
+        } yields {
+            "Unique; substitution [?0 := Uint(Usize), ?1 := Uint(Usize)], lifetime constraints []"
+        }
+
+        goal {
+            exists<T, float N> {
+                T = N, N = f32
+            }
+        } yields {
+            "Unique; substitution [?0 := Float(F32), ?1 := Float(F32)], lifetime constraints []"
+        }
+    }
+}
+
+/// Once a general type kind is unified with a specific type kind, it cannot be
+/// unified with an incompatible type (ex. integer type kind with char)
+#[test]
+fn general_ty_kind_becomes_specific() {
+    test! {
+        program {}
+
+        goal {
+            exists<T, int N> {
+                T = N, T = char
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            exists<T, float N> {
+                T = N, T = char
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}