@@ 226,19 226,16 @@ fn compile_decl(w: &mut impl Write, decl
 /// Compile a function signature
 fn compile_fn_signature(sig: &hir2::Sig) -> String {
     let mut accm = String::from("");
-    /*
-    TODO
-    let generics = sig.type_params();
 
-    if !generics.is_empty() {
+    // TODO: Eventually monomorph should make this go away...
+    if !sig.typeparams.is_empty() {
         accm += "<";
-        for generic in generics.iter() {
-            accm += &mangle_name(*generic);
+        for (tvar, _kind) in sig.typeparams.iter() {
+            accm += &mangle_name(*tvar);
             accm += ", ";
         }
         accm += ">";
     }
-    */
     accm += "(";
     for (varsym, typesym) in sig.params.iter() {
         accm += &*INT.fetch(*varsym);

          
@@ 248,16 245,14 @@ fn compile_fn_signature(sig: &hir2::Sig)
     }
     accm += ") -> ";
     accm += &compile_typename(&sig.rettype);
-    /*
-    TODO
-    if !generics.is_empty() {
+
+    if !sig.typeparams.is_empty() {
         accm += " where ";
-        for generic in generics.iter() {
-            accm += &mangle_name(*generic);
+        for (tvar, _kind) in sig.typeparams.iter() {
+            accm += &mangle_name(*tvar);
             accm += ": Copy,";
         }
     }
-    */
     accm
 }
 

          

@@ 198,6 198,10 @@ impl TypeNode {
         // Type::Var(s, vec![])
         todo!()
     }
+
+    pub fn forall(args: &[(Sym, Kind)], body: &TypeNode) -> Self {
+        Self::new(Type::Forall(args.to_vec(), body.clone()))
+    }
     pub fn function(params: &[TypeNode], rettype: &TypeNode) -> Self {
         TypeNode::new(Type::Func(Vec::from(params), rettype.clone()))
     }

          
@@ 496,6 500,8 @@ impl Type {
 
     /// Get a string for the name of the given type in valid Garnet syntax.
     /// Or at least should be.
+    ///
+    /// ...not all of these things have valid Garnet surface syntax, hm.
     pub fn get_name(&self) -> Cow<'static, str> {
         let join_types_with_commas = |lst: &[TypeNode]| {
             let p_strs = lst.iter().map(TypeNode::get_name).collect::<Vec<_>>();

          
@@ 543,11 549,6 @@ impl Type {
                 let mut t = String::from("fn");
                 t += "(";
 
-                // if typeparams.len() > 0 {
-                //     t += "|";
-                //     t += &join_types_with_commas(typeparams);
-                //     t += "| ";
-                // }
                 t += &join_types_with_commas(params);
 
                 t += ")";

          
@@ 558,26 559,12 @@ impl Type {
             }
             Type::Struct(body) => {
                 let mut res = String::from("struct ");
-                // if generics.is_empty() {
-                //     res += " "
-                // } else {
-                //     res += "[";
-                //     res += &join_types_with_commas(generics);
-                //     res += "] ";
-                // }
                 res += &join_vars_with_commas(body, ":");
                 res += " end";
                 Cow::Owned(res)
             }
             Type::Sum(body) => {
                 let mut res = String::from("sum");
-                // if generics.is_empty() {
-                //     res += " "
-                // } else {
-                //     res += "[";
-                //     res += &join_types_with_commas(generics);
-                //     res += "] ";
-                // }
                 res += &join_vars_with_commas(body, "");
                 res += " end";
                 Cow::Owned(res)

          
@@ 593,6 580,23 @@ impl Type {
             Type::UVar(id) => Cow::Owned(format!("__UVar_{}", id.0)),
             Type::UnknownInt(id) => Cow::Owned(format!("__UInt_{}", id.0)),
             Type::TypeVar(_idx, sym) => Cow::Owned(sym.val().as_ref().clone()),
+            Type::Forall(params, rettype) => {
+                let mut t = String::from("forall");
+                t += "(";
+
+                let strs = &mut vec![];
+                for (nm, kn) in params.iter() {
+                    strs.push(format!("{nm} {kn}"));
+                }
+                let args = strs.join(", ");
+                t += &args;
+
+                t += ")";
+                let rettype_str = rettype.get_name();
+                t += " ";
+                t += &rettype_str;
+                Cow::Owned(t)
+            }
             t => todo!("Name for type {:?}", t),
         }
     }

          

@@ 269,7 269,7 @@ impl Env {
         // flip our db index around to take from the end of the Vec
         // instead of the beginning (as linked-list langs like ML do)
         assert!(self.vals_size() > 0, "env size is zero, aieeee");
-        self.trace_bindings();
+        // self.trace_bindings();
         let i = self.vals_size() - 1 - idx.0;
         self.vals
             .get(i as usize)

          
@@ 303,8 303,7 @@ impl Env {
     /// Makes sure that the binding at the given Idx is a variable or type variable
     /// with the name specified.  Panics if it is not.
     fn check_var_name(&self, idx: Idx, name: Sym) {
-        trace!("FDSAFSDA");
-        self.trace_bindings();
+        // self.trace_bindings();
         match self
             .get_binding(idx)
             .expect("Invalid index, should never happen!")

          
@@ 484,13 483,16 @@ impl Env {
                 let new_body = self.eval_types(&*body)?;
                 NType::Tuple(new_body)
             }
-            TypeVar(idx, name) => match self.get_type_binding(idx)? {
-                TypeBinding::TypeVar(nty, _kn, _name) => nty,
-                other => Err(format!(
-                    "Expected typevar for {}, got {:?}\nContext is {:?}",
-                    name, other, self
-                ))?,
-            },
+            TypeVar(idx, name) => {
+                // debug!("Looking up type for type var {}", name);
+                match self.get_type_binding(idx)? {
+                    TypeBinding::TypeVar(nty, _kn, _name) => nty,
+                    other => Err(format!(
+                        "Expected typevar for {}, got {:?}\nContext is {:?}",
+                        name, other, self
+                    ))?,
+                }
+            }
 
             // here we *delay evaluation* of the forall by wrapping
             // it into a closure.  The closure just has a copy of the

          
@@ 699,6 701,10 @@ impl Env {
             (Prim(PrimType::UnknownInt), _) | (_, Prim(PrimType::UnknownInt)) => {
                 unreachable!("PrimType::UnknownInt should never exist in HIR!")
             }
+            // Well if the index and name of a type varboth match then it
+            // *definitely* is correct...
+            // TODO: This should just have to be the index, right?
+            (TypeVar(i1, nm1), TypeVar(i2, nm2)) if i1 == i2 && nm1 == nm2 => Ok(()),
             // Primitives just match directly
             (Prim(p1), Prim(p2)) if p1 == p2 => Ok(()),
             (Tuple(t1body), Tuple(t2body)) => {

          
@@ 966,7 972,9 @@ impl Env {
                         }
                         given_rettype.clone()
                     }
-                    other => return Err(format!("Function type expected in apply, got {}", other)),
+                    other => {
+                        return Err(format!("Function type expected in funcall, got {}", other))
+                    }
                 }
             }
             // I THINK this is correct...

          
@@ 1033,12 1041,42 @@ impl Env {
             }
             Deref { expr: _ } => todo!(),
             Ref { expr: _ } => todo!(),
+            // We are *evaluating* this big-forall term so we
+            // bind its arg, then find the type of its body.
             ForallLambda {
-                args: _,
-                rettype: _,
-                body: _,
-            } => todo!(),
-            ForallApply { e: _, t: _ } => todo!(),
+                args,
+                rettype,
+                body,
+            } => {
+                // The arg variables are something that has not been bound yet,
+                // so we create a new neutral value for each arg and bind them.
+                let mut new_ctx = self.clone();
+                for (argname, argkind) in args {
+                    new_ctx = self.add_neu_binding(*argname, argkind.clone());
+                }
+                let bodytype = new_ctx.type_of(body)?;
+                TypeNode::forall(args, &bodytype)
+            }
+            // Again just applying a lambda, though it's a little fiddly
+            // 'cause you have to get everything in the right oder.
+            ForallApply { e, t } => {
+                // somehow this is miraculously correct, it seems.
+                // The magic of binding the variable into the forall
+                // closure is handled by a mixture of eval_type() and apply().
+                // (Mostly apply().)
+                let type_of_expr = self.type_of(e)?;
+                let functype = self.eval_type(type_of_expr)?;
+                let argkinds: Result<Vec<_>, _> =
+                    t.iter().map(|ty| self.kind_of(ty.clone())).collect();
+                let argkinds = argkinds?;
+                let args: Result<Vec<_>, _> =
+                    t.iter().map(|ty| self.eval_type(ty.clone())).collect();
+                let args = args?;
+                // We check that the kind of the Forall is correct in apply()
+                // let argkind = self.kind_of(typearg.clone())?;
+                let res = apply(functype, &args, &argkinds)?;
+                quote(self.types_size(), res)?
+            }
         };
         /*
                     Ascribe(expr, ty) => {

          
@@ 1307,22 1345,28 @@ pub fn quote(env_size: usize, v: NType) 
         NType::Neu(neuval) => quote_neu(env_size, neuval)?,
         NType::UVar(uid) => Type::UVar(uid),
         NType::UnknownInt(uid) => Type::UnknownInt(uid),
+        NType::Forall(clos) => {
+            // this is the type of an expression with a type var that hasn't been evaluated,
+            // so we quote its parameters back into a neutral value.
+            // I think the Trick is that this only ever gets called when we're
+            // outside an (apply (lambda ...)) pair, or if there's something
+            // in between the apply and lambda that makes it irreducable?
+            let Closure(args, _env, _bodytype) = clos.clone();
+            let new_vars: Vec<_> = args
+                .iter()
+                .map(|(name, _kind)| {
+                    let lvl = Lvl(env_size);
+                    NType::Neu(Neutral::Var(lvl, *name))
+                })
+                .collect();
+            let inst_body = inst(clos, &new_vars)?;
+            let newbody = quote(env_size + 1, inst_body)?;
+            Type::Forall(args, newbody)
+        }
 
         other => todo!("{:?}", other),
     };
     /*
-        NType::Forall(clos) => {
-            // this is the type of an expression with a type var that hasn't been evaluated,
-            // so we quote its parameter back into a neutral value.
-            // I think the Trick is that this only ever gets called when we're
-            // outside an (apply (lambda ...)) pair, or if there's something
-            // in between the apply and lambda that makes it irreducable?
-            let Closure(name, _env, _bodytype, kind) = clos.clone();
-            let new_var = NType::Neu(Neutral::Var(Lvl(env_size), name.clone()));
-            let inst_body = inst(clos, new_var)?;
-            let newbody = quote(env_size + 1, inst_body)?;
-            Type::Forall(name, kind, Box::new(newbody))
-        }
         NType::Record(fields) => {
             // just recurse over fields.
             let new_fields = record_map(fields, &|t| quote(env_size, t))?;

          
@@ 1498,14 1542,15 @@ impl Env {
         // see kind_of() for Type::TypeLambda for how to handle
         // binding type args
         for (name, kn) in sig.typeparams.iter() {
+            debug!("Adding type param {} to env", name);
             func_env = func_env.add_neu_binding(*name, kn.clone());
         }
         for (name, ty) in sig.params.iter() {
             func_env = func_env.add_var_binding(*name, &ty, false)?;
         }
 
-        let (_new_env, res_type) = func_env.typecheck_block(&body, &sig.rettype)?;
-        if self.type_equiv(res_type, sig.rettype.clone()).is_err() {
+        let (mut new_env, res_type) = func_env.typecheck_block(&body, &sig.rettype)?;
+        if new_env.type_equiv(res_type, sig.rettype.clone()).is_err() {
             let msg = format!("Function {} does not return type {}", name, sig.rettype);
             return Err(msg);
         }

          

@@ 11,7 11,7 @@ end
 
 fn main() {} =
     let a {I32, Bool, I32} = identity(|{I32, Bool, I32}| {1, false, 3})
-    let b {I32, Bool, I32} = identity({1, false, 3})
-    let c {I32, Bool, I32} = identity {1, false, 3}
-    let d {I32, I32} = identity {12, 12}
+    -- let b {I32, Bool, I32} = identity({1, false, 3})
+    -- let c {I32, Bool, I32} = identity {1, false, 3}
+    -- let d {I32, I32} = identity {12, 12}
 end