@@ 707,7 707,7 @@ impl Env {
         //     return Ok(());
         // }
         debug!("Unifying {t1} and {t2}");
-        match (&*t1.t, &*t2.t) {
+        let res = match (&*t1.t, &*t2.t) {
             // TODO NEXT: I THINK we have to resolve the ref's of unknownint's
             // somewhere around here...
             (Prim(PrimType::UnknownInt), Prim(PrimType::UnknownInt)) => {

          
@@ 790,7 790,9 @@ impl Env {
                     // UVar is Unknown
                     // Well it has to be the same as our other type now
                     trace!("Setting uvar {:?} to {:?}", t1, t2);
-                    self.set_uvar(*uid, UInfo::Known(t2.clone()));
+                    // self.set_uvar(*uid, UInfo::Known(t2.clone()));
+                    self.set_uvar(t2.id, UInfo::Known(t2.clone()));
+                    self.set_uvar(*uid, UInfo::Ref(t2.id));
                     Ok(())
                 }
             }

          
@@ 798,7 800,14 @@ impl Env {
             (_other_type, UVar(_)) => self.try_unify(t2, t1),
 
             (_, _) => Err(format!("Unification failed: {} != {}", t1, t2)),
-        }
+        };
+        debug!("Unification done, result: {} = {}? {:?}", t1, t2, res);
+        debug!(
+            "uvars: {:?} = {:?}",
+            self.lookup_uvar(t1.id),
+            self.lookup_uvar(t2.id)
+        );
+        res
     }
 
     fn _old_type_equiv(&self, t1: TypeNode, t2: TypeNode) -> Result<TypeNode, String> {

          
@@ 844,6 853,26 @@ impl Env {
         TypeNode::new(res)
     }
 
+    /*
+    /// fuckit if I were to just do bidi inference, what would it look like
+    fn try_infer(e: &mut ENode) -> Result<ENode, String> {
+        match &*e.e {
+            Expr::Let { items, body } => {
+                for item in items {
+                    match &*item.typename.t {
+                        Type::UVar(id) => {
+                            // set type id to the type of the body
+                        }
+                        other => {
+                            // infer the type of the body and set item.typename to that
+                        }
+                    }
+                }
+            }
+        }
+    }
+    */
+
     /// type_of() but takes a list of exprnodes and checks them, and
     /// then returns unit.
     fn check_types(&mut self, es: &mut [ENode]) -> Result<TypeNode, String> {

          
@@ 932,7 961,7 @@ impl Env {
             Let { items, body } => {
                 // Typecheck and bind the vars
                 let mut scope = self.clone();
-                for item in items {
+                for item in items.iter_mut() {
                     // typecheck the init expr
                     // Make sure the typename matches the type of the init expr
                     let init_type = scope.type_of(&mut item.init)?;

          
@@ 940,7 969,7 @@ impl Env {
                         "Trying to typecheck let item {} {} = {:?}",
                         item.varname, item.typename, item.init
                     );
-                    scope.try_unify(&item.typename, &init_type)?;
+                    // type_equiv() will try to unify if necessary
                     scope.type_equiv(init_type, item.typename.clone())?;
                     // Bind the type to the var name
                     scope = scope.add_var_binding(item.varname, &item.typename, item.mutable)?;

          
@@ 1724,6 1753,12 @@ impl Env {
             debug!("  uvar {id:?} = {info:?}");
         }
     }
+
+    fn dump_expr_types(&self) {
+        for (eid, t) in &self.shared.borrow().expr_type_map {
+            debug!("  expr {eid:?} = {t:?}");
+        }
+    }
 }
 
 /// Hmmm, not sure what this should return... a normalized IR, I suspect?

          
@@ 1736,6 1771,7 @@ pub fn typecheck(ir: &mut hir2::Ir) -> R
     env.typecheck_consts(&ir.consts)?;
     env.typecheck_fns(&mut ir.fns)?;
     env.dump_uvars();
+    env.dump_expr_types();
     Ok(env)
 }
 

          

@@ 6,10 6,22 @@ 
 --     7
 
 fn main() {} =
-    let a I32 = 99
+    -- can we move type information from one side of the let to the other?
+    --let a1 I32 = 99
+    --let b1 = 99_I32
+
+    -- can type information flow forward?
+    --let a2 I32 = 3
+    --let b2 = a2
+
+    -- can type information flow backward?
+    -- ...do I care?
+    --let a2 = 3
+    --let b2 I32 = a2
+
+    -- does type information compose?
     let x = 3
-    let b I32 = x
-    --let y = 4
-    --let z I32 = x + y
+    let y I32 = 4
+    let z = x + y
 end