From c0f6b5c4be04891b1470394b35a5ac2419b242cd Mon Sep 17 00:00:00 2001
From: NotAFile <notafile@gmail.com>
Date: Sun, 20 Feb 2022 20:12:35 +0100
Subject: [PATCH] make type inference work-ish

---
 src/frontend.rs       | 50 +++++++++++++++++++++++++++++++++----------
 src/frontend/types.rs | 42 +++++++++++++++++++++++++++++++-----
 2 files changed, 76 insertions(+), 16 deletions(-)

diff --git a/src/frontend.rs b/src/frontend.rs
index ea77959..bb30c14 100644
--- a/src/frontend.rs
+++ b/src/frontend.rs
@@ -297,18 +297,46 @@ impl Context {
             } => {
                 let args_typed: Vec<_> = args.iter().map(|ex| self.infer_expr_types(ex)).collect();
                 let callee_def = self.callables.get(*called);
-                if self.types.is_fully_typed(callee_def.ret_type) {
-                    expr.clone().with_type(callee_def.ret_type)
-                } else {
-                    let param_types: Vec<_> = callee_def.args.iter().map(|param| param.1).collect();
-                    let mut genargs = callee_def.genargs.clone();
-                    let inferred_args: Vec<_> = param_types
-                        .iter()
-                        .zip(args_typed)
-                        .map(|(param, arg)| self.types.infer_type(*param, arg.typ))
-                        .collect();
-                    expr.clone().with_type(callee_def.ret_type)
+
+                let param_types: Vec<_> = callee_def.args.iter().map(|param| param.1).collect();
+                let inferred_args: Vec<_> = param_types
+                    .iter()
+                    .zip(&args_typed)
+                    .map(|(param, arg)| self.types.infer_type(*param, arg.typ))
+                    .collect();
+
+                let mut genargs: Vec<_> = callee_def.genargs.iter().map(|a| a.1).collect();
+
+                let mut new_type = callee_def.ret_type;
+
+                if genargs.len() != 0 {
+                    // need to infer generic arguments
+                    for inf_res in inferred_args {
+                        match inf_res {
+                            types::InferenceResult::First(_) => todo!(),
+                            types::InferenceResult::Second(_) => todo!(),
+                            types::InferenceResult::TypeVar(dbi, tvar, typ) => {
+                                assert_eq!(dbi, 0);
+                                // TODO: type check argument instead of just using it
+                                genargs[tvar as usize] = typ;
+                            }
+                            types::InferenceResult::Incompatible => todo!(),
+                            types::InferenceResult::Ambigous => todo!(),
+                        }
+                    }
+
+                    // TODO: HACKY HACKY HACK
+                    new_type = genargs[0];
                 }
+
+                let mut new_expr = expr.clone();
+                new_expr.typ = new_type;
+                new_expr.kind = typed_ir::ExprKind::Call {
+                    called: called.clone(),
+                    args: args_typed,
+                    genargs,
+                };
+                new_expr
             }
         }
     }
diff --git a/src/frontend/types.rs b/src/frontend/types.rs
index b791c4a..9690d32 100644
--- a/src/frontend/types.rs
+++ b/src/frontend/types.rs
@@ -74,6 +74,20 @@ pub enum GenericArg {
     Type(Type),
 }
 
+#[derive(Debug)]
+pub enum InferenceResult {
+    /// The first type was inferred
+    First(Type),
+    /// The second type was inferred
+    Second(Type),
+    /// A typevar was inferred
+    TypeVar(u32, u32, Type),
+    /// The types were incompatible
+    Incompatible,
+    /// Neither of the types were complete
+    Ambigous,
+}
+
 pub struct PrimitiveTypes {
     pub elabnum: Type,
     pub logic: Type,
@@ -173,15 +187,28 @@ impl TypingContext {
     }
 
     /// Given the type of a variable in two locations, infer what the true type should be
-    pub fn infer_type(&mut self, typ_a: Type, typ_b: Type) -> Type {
+    pub fn infer_type(&mut self, typ_a: Type, typ_b: Type) -> InferenceResult {
         match (&self.get(typ_a).kind, &self.get(typ_b).kind) {
-            (a, b) => panic!("cannot infer between: {:?}, {:?}", a, b),
+            (TypeKind::TypeVar(dbi, tvar), _) => InferenceResult::TypeVar(*dbi, *tvar, typ_b),
+            (_, TypeKind::TypeVar(dbi, tvar)) => InferenceResult::TypeVar(*dbi, *tvar, typ_a),
+            (a, b) => {
+                let a_full = self.is_fully_typed_kind(a);
+                let b_full = self.is_fully_typed_kind(b);
+                if a_full && b_full {
+                    InferenceResult::Incompatible
+                } else if a_full && !b_full {
+                    InferenceResult::Second(typ_a)
+                } else if !a_full && b_full {
+                    InferenceResult::First(typ_b)
+                } else {
+                    InferenceResult::Ambigous
+                }
+            }
         }
     }
 
-    /// return whether the type has no unfilled parameters
-    pub fn is_fully_typed(&self, typ: Type) -> bool {
-        match &self.get(typ).kind {
+    fn is_fully_typed_kind(&self, kind: &TypeKind) -> bool {
+        match kind {
             TypeKind::ElabType(_) => todo!(),
             TypeKind::Logic(data) => {
                 if let ElabValue::Concrete(_) = data.value {
@@ -201,6 +228,11 @@ impl TypingContext {
         }
     }
 
+    /// return whether the type has no unfilled parameters
+    pub fn is_fully_typed(&self, typ: Type) -> bool {
+        self.is_fully_typed_kind(&self.get(typ).kind)
+    }
+
     pub fn pretty_value(&self, w: &mut dyn std::fmt::Write, data: &ElabData) -> std::fmt::Result {
         match &data.value {
             ElabValue::Infer => write!(w, "?: ")?,