From 05c13184e45da32b60f7fc5be4dadcd4bdcc048b Mon Sep 17 00:00:00 2001
From: Aaron Councilman <aaronjc4@illinois.edu>
Date: Tue, 10 Sep 2024 16:53:50 -0500
Subject: [PATCH] Juno Improvements: type inference and intrinsics

---
 juno_frontend/examples/intrinsics1.jn |   3 +
 juno_frontend/examples/intrinsics2.jn |   8 +
 juno_frontend/examples/intrinsics3.jn |   7 +
 juno_frontend/src/codegen.rs          |  20 +-
 juno_frontend/src/intrinsics.rs       | 179 ++++++-
 juno_frontend/src/lang.l              |   3 +-
 juno_frontend/src/lang.y              |  58 ++-
 juno_frontend/src/locs.rs             |  35 ++
 juno_frontend/src/main.rs             |   1 +
 juno_frontend/src/semant.rs           | 710 ++++++++++----------------
 juno_frontend/src/types.rs            | 568 +++++++++++----------
 11 files changed, 859 insertions(+), 733 deletions(-)
 create mode 100644 juno_frontend/examples/intrinsics1.jn
 create mode 100644 juno_frontend/examples/intrinsics2.jn
 create mode 100644 juno_frontend/examples/intrinsics3.jn
 create mode 100644 juno_frontend/src/locs.rs

diff --git a/juno_frontend/examples/intrinsics1.jn b/juno_frontend/examples/intrinsics1.jn
new file mode 100644
index 00000000..45a3b51a
--- /dev/null
+++ b/juno_frontend/examples/intrinsics1.jn
@@ -0,0 +1,3 @@
+fn intrinsics1(x : f32, y : f64) -> f64 {
+  return sqrt!(x) as f64 + sqrt!(y);
+}
diff --git a/juno_frontend/examples/intrinsics2.jn b/juno_frontend/examples/intrinsics2.jn
new file mode 100644
index 00000000..efdd1a79
--- /dev/null
+++ b/juno_frontend/examples/intrinsics2.jn
@@ -0,0 +1,8 @@
+fn intrinsics2(x : f32, y : f64) -> f64 {
+  let a : f32 = exp2!(x);
+  let b : f64 = exp!(y);
+  let c : i32 = abs!(x as i32);
+  let d : f64 = sin!(b);
+
+  return a as f64 * d + c as f64;
+}
diff --git a/juno_frontend/examples/intrinsics3.jn b/juno_frontend/examples/intrinsics3.jn
new file mode 100644
index 00000000..85c5ed43
--- /dev/null
+++ b/juno_frontend/examples/intrinsics3.jn
@@ -0,0 +1,7 @@
+fn poly<f : float, i : number>(x : f, y : i) -> f {
+  return powf!(x, x) * abs!(y) as f;
+}
+
+fn intrinsics3(x : f32, y : u32) -> f32 {
+  return poly(x, y);
+}
diff --git a/juno_frontend/src/codegen.rs b/juno_frontend/src/codegen.rs
index d7821c95..a2249812 100644
--- a/juno_frontend/src/codegen.rs
+++ b/juno_frontend/src/codegen.rs
@@ -496,8 +496,24 @@ impl CodeGenerator<'_> {
 
                 (read_id, block)
             },
-            Expr::Intrinsic { .. } => {
-                todo!("intrinsic function codegen")
+            Expr::Intrinsic { id, ty_args : _, args, .. } => {
+                // Code gen for each argument in order
+                let mut block = cur_block;
+                let mut arg_vals = vec![];
+                for arg in args {
+                    let (val, new_block)
+                        = self.codegen_expr(arg, types, ssa, func_id, block);
+                    block = new_block;
+                    arg_vals.push(val);
+                }
+
+                // Create the intrinsic call expression
+                let mut call = self.builder.allocate_node(func_id);
+                let call_id = call.id();
+                call.build_intrinsic(*id, arg_vals.into());
+                let _ = self.builder.add_node(call);
+
+                (call_id, block)
             },
         }
     }
diff --git a/juno_frontend/src/intrinsics.rs b/juno_frontend/src/intrinsics.rs
index 3d9b5459..100d1f25 100644
--- a/juno_frontend/src/intrinsics.rs
+++ b/juno_frontend/src/intrinsics.rs
@@ -1,11 +1,11 @@
 /* Definitions of the set of intrinsic functions in Juno */
 use phf::phf_map;
 
-use crate::types::{Type, TypeSolver};
+use crate::types::{Type, TypeSolver, Primitive};
 use crate::parser;
 
 // How intrinsics are identified in the Hercules IR
-pub type IntrinsicIdentity = usize;
+pub type IntrinsicIdentity = hercules_ir::ir::Intrinsic;
 
 // Information about a single intrinsic, including its type information and how it will be
 // identified in the Hercules IR
@@ -13,24 +13,179 @@ pub type IntrinsicIdentity = usize;
 pub struct IntrinsicInfo {
     pub id      : IntrinsicIdentity,
     pub kinds   : &'static [parser::Kind],
-    pub args    : fn(&Vec<Type>, &mut TypeSolver) -> Vec<(Type, bool)>,
-    pub ret_typ : fn(&Vec<Type>, &mut TypeSolver) -> Type,
+    pub typ     : fn(&Vec<Type>, &mut TypeSolver) -> (Vec<Type>, Type),
 }
 
-fn sqrt_args(ty_args : &Vec<Type>, _ : &mut TypeSolver) -> Vec<(Type, bool)> {
-    vec![(ty_args[0], false)]
+// The type for a function which takes one argument of a variable type and
+// returns a value of that same type
+fn var_type(ty_args : &Vec<Type>, _ : &mut TypeSolver) -> (Vec<Type>, Type) {
+    (vec![ty_args[0]], ty_args[0])
 }
 
-fn sqrt_return(ty_args : &Vec<Type>, _ : &mut TypeSolver) -> Type {
-    ty_args[0]
+// Type type for a function which takes two arguments of the same variable type
+// and returns a value of that same type
+fn var2_type(ty_args : &Vec<Type>, _ : &mut TypeSolver) -> (Vec<Type>, Type) {
+    (vec![ty_args[0], ty_args[0]], ty_args[0])
+}
+
+fn pow_type(ty_args : &Vec<Type>, types : &mut TypeSolver) -> (Vec<Type>, Type) {
+    (vec![ty_args[0], types.new_primitive(Primitive::U32)], ty_args[0])
+}
+
+fn powi_type(ty_args : &Vec<Type>, types : &mut TypeSolver) -> (Vec<Type>, Type) {
+    (vec![ty_args[0], types.new_primitive(Primitive::I32)], ty_args[0])
 }
 
 static INTRINSICS : phf::Map<&'static str, IntrinsicInfo> = phf_map! {
-    "sqrt" => IntrinsicInfo {
-        id      : 0,
+    "abs"   => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Abs,
         kinds   : &[parser::Kind::Number],
-        args    : sqrt_args,
-        ret_typ : sqrt_return,
+        typ     : var_type,
+    },
+    "acos" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ACos,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "acosh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ACosh,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "asin" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ASin,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "asinh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ASinh,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "atan" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ATan,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "atan2" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ATan2,
+        kinds   : &[parser::Kind::Float],
+        typ     : var2_type,
+    },
+    "atanh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ATanh,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "cbrt" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Cbrt,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "ceil" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Ceil,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "cos" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Cos,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "cosh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Cos,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "exp" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Exp,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "exp2" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Exp2,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "exp_m1" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::ExpM1,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "floor" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Floor,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "ln" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Ln,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "ln_1p" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Ln1P,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "log" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Log,
+        kinds   : &[parser::Kind::Float],
+        typ     : var2_type,
+    },
+    "log10" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Log10,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "log2" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Log2,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "pow" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Pow,
+        kinds   : &[parser::Kind::Integer],
+        typ     : pow_type,
+    },
+    "powf" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Powf,
+        kinds   : &[parser::Kind::Float],
+        typ     : var2_type,
+    },
+    "powi" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Powi,
+        kinds   : &[parser::Kind::Float],
+        typ     : powi_type,
+    },
+    "round" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Round,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "sin" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Sin,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "sinh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Sinh,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "sqrt" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Sqrt,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "tan" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Tan,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
+    },
+    "tanh" => IntrinsicInfo {
+        id      : hercules_ir::ir::Intrinsic::Tanh,
+        kinds   : &[parser::Kind::Float],
+        typ     : var_type,
     },
 };
 
diff --git a/juno_frontend/src/lang.l b/juno_frontend/src/lang.l
index 6d96385e..6d449c14 100644
--- a/juno_frontend/src/lang.l
+++ b/juno_frontend/src/lang.l
@@ -22,6 +22,7 @@ const    "const"
 continue "continue"
 else     "else"
 false    "false"
+float    "float"
 fn       "fn"
 for      "for"
 if       "if"
@@ -124,7 +125,7 @@ _        "_"
 0x[0-9a-fA-F]+            "HEX_INT"
 0b[0-1]+                  "BIN_INT"
 0o[0-7]+                  "OCT_INT"
-[0-9]+\.[0-9]*(|e[0-9]+)  "FLOAT"
+[0-9]+\.[0-9]*(|e[0-9]+)  "FLOAT_LIT"
 
 . "UNMATCHED"
 . "UNARY"
diff --git a/juno_frontend/src/lang.y b/juno_frontend/src/lang.y
index 1530981c..98322da4 100644
--- a/juno_frontend/src/lang.y
+++ b/juno_frontend/src/lang.y
@@ -1,7 +1,7 @@
 %start Program
 
 %token UNARY
-%avoid_insert "FUNC_ATTR" "DOT_NUM" "ID" "INT" "HEX_INT" "BIN_INT" "OCT_INT" "FLOAT"
+%avoid_insert "FUNC_ATTR" "DOT_NUM" "ID" "INT" "HEX_INT" "BIN_INT" "OCT_INT" "FLOAT_LIT"
 %expect-unused Unmatched 'UNMATCHED' 'UNARY'
 
 %nonassoc ')'
@@ -81,6 +81,7 @@ Kind -> Result<Kind, ()>
   | 'usize'   { Ok(Kind::USize) }
   | 'number'  { Ok(Kind::Number) }
   | 'integer' { Ok(Kind::Integer) }
+  | 'float'   { Ok(Kind::Float) }
   ;
 
 TypeDecl -> Result<Top, ()>
@@ -111,12 +112,14 @@ ObjField -> Result<ObjField, ()>
 Type -> Result<Type, ()>
   : PrimType
         { Ok(Type::PrimType{ span : $span, typ : $1? }) }
+  | '_'
+        { Ok(Type::WildType{ span : $span }) }
   | '(' Types ')'
         { Ok(Type::TupleType{ span : $span, tys : $2? }) }
   | PackageName
-        { Ok(Type::NamedType{ span : $span, name : $1?, args : vec![] }) }
+        { Ok(Type::NamedType{ span : $span, name : $1?, args : None }) }
   | PackageName '::' '<' TypeExprs '>'
-        { Ok(Type::NamedType{ span : $span, name : $1?, args : $4? }) }
+        { Ok(Type::NamedType{ span : $span, name : $1?, args : Some($4?) }) }
   | Type '[' TypeExprs ']'
         { Ok(Type::ArrayType{ span : $span, elem : Box::new($1?), dims : $3? }) }
   ;
@@ -289,9 +292,9 @@ Stmt -> Result<Stmt, ()>
   | Stmts
       { $1 }
   | PackageName '(' Params ')' ';'
-      { Ok(Stmt::CallStmt{ span : $span, name : $1?, ty_args : vec![], args : $3? }) }
+      { Ok(Stmt::CallStmt{ span : $span, name : $1?, ty_args : None, args : $3? }) }
   | PackageName '::' '<' TypeExprs '>' '(' Params ')' ';'
-      { Ok(Stmt::CallStmt{ span : $span, name : $1?, ty_args : $4?, args : $7? }) }
+      { Ok(Stmt::CallStmt{ span : $span, name : $1?, ty_args : Some($4?), args : $7? }) }
   ;
 Stmts -> Result<Stmt, ()>
   : '{' StmtList '}'  { Ok(Stmt::BlockStmt{ span : $span, body : $2? }) };
@@ -370,9 +373,9 @@ Expr -> Result<Expr, ()>
   | '(' Exprs ')'
       { Ok(Expr::Tuple{ span : $span, exprs : $2? }) }
   | PackageName '{' IdExprs '}'
-      { Ok(Expr::Struct{ span : $span, name : $1?, ty_args : vec![], exprs : $3? }) }
+      { Ok(Expr::Struct{ span : $span, name : $1?, ty_args : None, exprs : $3? }) }
   | PackageName '::' '<' TypeExprs '>' '{' IdExprs '}'
-      { Ok(Expr::Struct{ span : $span, name : $1?, ty_args : $4?, exprs : $7? }) }
+      { Ok(Expr::Struct{ span : $span, name : $1?, ty_args : Some($4?), exprs : $7? }) }
   | 'true'
       { Ok(Expr::BoolLit{ span : $span, value : true }) }
   | 'false'
@@ -380,7 +383,7 @@ Expr -> Result<Expr, ()>
   | IntLit
       { let (span, base) = $1?;
         Ok(Expr::IntLit{ span : span, base : base }) }
-  | 'FLOAT'
+  | 'FLOAT_LIT'
       { Ok(Expr::FloatLit{ span : $span }) }
   | '-' Expr %prec 'UNARY'
       { Ok(Expr::UnaryExpr{ span : $span, op : UnaryOp::Negation, expr : Box::new($2?)}) }
@@ -429,13 +432,13 @@ Expr -> Result<Expr, ()>
   | 'if' Expr 'then' Expr 'else' Expr
       { Ok(Expr::CondExpr{ span: $span, cond : Box::new($2?), thn : Box::new($4?), els : Box::new($6?) })}
   | PackageName '(' Params ')'
-      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : vec![], args: $3? }) }
+      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : None, args: $3? }) }
   | PackageName '::' '<' TypeExprs '>' '(' Params ')'
-      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : $4?, args: $7? }) }
+      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : Some($4?), args: $7? }) }
   | PackageName '!' '(' Params ')'
-      { Ok(Expr::IntrinsicExpr{ span : $span, name : $1?, ty_args : vec![], args: $4? }) }
+      { Ok(Expr::IntrinsicExpr{ span : $span, name : $1?, ty_args : None, args: $4? }) }
   | PackageName '!' '::' '<' TypeExprs '>' '(' Params ')'
-      { Ok(Expr::IntrinsicExpr{ span : $span, name : $1?, ty_args : $5?, args: $8? }) }
+      { Ok(Expr::IntrinsicExpr{ span : $span, name : $1?, ty_args : Some($5?), args: $8? }) }
   ;
 IdExprs -> Result<Vec<(Id, Expr)>, ()>
   : 'ID' '=' Expr               { Ok(vec![(span_of_tok($1)?, $3?)]) }
@@ -477,7 +480,7 @@ NonStructExpr -> Result<Expr, ()>
   | IntLit
       { let (span, base) = $1?;
         Ok(Expr::IntLit{ span : span, base : base }) }
-  | 'FLOAT'
+  | 'FLOAT_LIT'
       { Ok(Expr::FloatLit{ span : $span }) }
   | '-' NonStructExpr %prec 'UNARY'
       { Ok(Expr::UnaryExpr{ span : $span, op : UnaryOp::Negation, expr : Box::new($2?)}) }
@@ -526,9 +529,9 @@ NonStructExpr -> Result<Expr, ()>
   | 'if' NonStructExpr 'then' NonStructExpr 'else' NonStructExpr
       { Ok(Expr::CondExpr{ span: $span, cond : Box::new($2?), thn : Box::new($4?), els : Box::new($6?) })}
   | PackageName '(' Params ')'
-      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : vec![], args: $3? }) }
+      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : None, args: $3? }) }
   | PackageName '::' '<' TypeExprs '>' '(' Params ')'
-      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : $4?, args: $7? }) }
+      { Ok(Expr::CallExpr{ span : $span, name : $1?, ty_args : Some($4?), args: $7? }) }
   ;
 
 TypeExprs -> Result<Vec<TypeExpr>, ()>
@@ -543,12 +546,14 @@ TypeExprsS -> Result<Vec<TypeExpr>, ()>
 TypeExpr -> Result<TypeExpr, ()>
   : PrimType
       { Ok(TypeExpr::PrimType{ span : $span, typ : $1? }) }
+  | '_'
+      { Ok(TypeExpr::WildcardType { span : $span }) }
   | '(' TypeExprs ')'
       { Ok(TypeExpr::TupleType{ span : $span, tys : $2? }) }
   | PackageName
-      { Ok(TypeExpr::NamedTypeExpr{ span : $span, name : $1?, args : vec![]}) }
+      { Ok(TypeExpr::NamedTypeExpr{ span : $span, name : $1?, args : None}) }
   | PackageName '::' '<' TypeExprs '>'
-      { Ok(TypeExpr::NamedTypeExpr{ span : $span, name : $1?, args : $4? }) }
+      { Ok(TypeExpr::NamedTypeExpr{ span : $span, name : $1?, args : Some($4?) }) }
   | TypeExpr '[' TypeExprs ']'
       { Ok(TypeExpr::ArrayTypeExpr{ span : $span, elem : Box::new($1?), dims : $3? }) }
   | IntLit
@@ -599,7 +604,7 @@ pub type PackageName = Vec<Span>;
 pub type ImportName  = (PackageName, Option<Span>); // option is the wildcard *
 
 #[derive(Debug, Copy, Clone)]
-pub enum Kind { Type, USize, Number, Integer }
+pub enum Kind { Type, USize, Number, Integer, Float }
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum Primitive { Bool, I8, U8, I16, U16, I32, U32, I64, U64, USize, F32, F64, Void }
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
@@ -643,8 +648,9 @@ pub enum TyDef {
 #[derive(Debug)]
 pub enum Type {
   PrimType  { span : Span, typ : Primitive },
+  WildType  { span : Span },
   TupleType { span : Span, tys : Vec<Type> },
-  NamedType { span : Span, name : PackageName, args : Vec<TypeExpr> },
+  NamedType { span : Span, name : PackageName, args : Option<Vec<TypeExpr>> },
   ArrayType { span : Span, elem : Box<Type>, dims : Vec<TypeExpr> },
 }
 
@@ -663,7 +669,7 @@ pub enum Stmt {
   BreakStmt  { span : Span },
   ContinueStmt { span : Span },
   BlockStmt    { span : Span, body : Vec<Stmt> },
-  CallStmt     { span : Span, name : PackageName, ty_args : Vec<TypeExpr>,
+  CallStmt     { span : Span, name : PackageName, ty_args : Option<Vec<TypeExpr>>,
                  args : Vec<(bool, Expr)> }, // bool indicates & (for inouts)
 }
 
@@ -692,7 +698,7 @@ pub enum Expr {
   NumField      { span : Span, lhs : Box<Expr>, rhs : Span },
   ArrIndex      { span : Span, lhs : Box<Expr>, index : Vec<Expr> },
   Tuple         { span : Span, exprs : Vec<Expr> },
-  Struct        { span : Span, name : PackageName, ty_args : Vec<TypeExpr>,
+  Struct        { span : Span, name : PackageName, ty_args : Option<Vec<TypeExpr>>,
                   exprs : Vec<(Id, Expr)> },
   BoolLit       { span : Span, value : bool },
   IntLit        { span : Span, base : IntBase },
@@ -701,17 +707,18 @@ pub enum Expr {
   BinaryExpr    { span : Span, op : BinaryOp, lhs : Box<Expr>, rhs : Box<Expr> },
   CastExpr      { span : Span, expr : Box<Expr>, typ : Type },
   CondExpr      { span : Span, cond : Box<Expr>, thn : Box<Expr>, els : Box<Expr> },
-  CallExpr      { span : Span, name : PackageName, ty_args : Vec<TypeExpr>,
+  CallExpr      { span : Span, name : PackageName, ty_args : Option<Vec<TypeExpr>>,
                   args : Vec<(bool, Expr)> }, // bool indicates & (for inouts)
-  IntrinsicExpr { span : Span, name : PackageName, ty_args : Vec<TypeExpr>,
+  IntrinsicExpr { span : Span, name : PackageName, ty_args : Option<Vec<TypeExpr>>,
                   args : Vec<(bool, Expr)> },
 }
 
-#[derive(Debug)]
+#[derive(Debug, Clone)]
 pub enum TypeExpr {
   PrimType        { span : Span, typ : Primitive },
+  WildcardType    { span : Span },
   TupleType       { span : Span, tys : Vec<TypeExpr> },
-  NamedTypeExpr   { span : Span, name : PackageName, args : Vec<TypeExpr> },
+  NamedTypeExpr   { span : Span, name : PackageName, args : Option<Vec<TypeExpr>> },
   ArrayTypeExpr   { span : Span, elem : Box<TypeExpr>, dims : Vec<TypeExpr> },
   IntLiteral      { span : Span, base : IntBase },
   Negative        { span : Span, expr : Box<TypeExpr> },
@@ -772,6 +779,7 @@ impl Spans for TypeExpr {
   fn span(&self) -> Span {
     match self {
       TypeExpr::PrimType          { span, .. }
+      | TypeExpr::WildcardType    { span, .. }
       | TypeExpr::TupleType       { span, .. }
       | TypeExpr::NamedTypeExpr   { span, .. }
       | TypeExpr::ArrayTypeExpr   { span, .. }
diff --git a/juno_frontend/src/locs.rs b/juno_frontend/src/locs.rs
new file mode 100644
index 00000000..24c06711
--- /dev/null
+++ b/juno_frontend/src/locs.rs
@@ -0,0 +1,35 @@
+use lrlex::DefaultLexerTypes;
+use lrpar::NonStreamingLexer;
+use cfgrammar::Span;
+
+use std::fmt;
+
+// A location in the program, used in error messages
+#[derive(Copy, Clone, Debug)]
+pub struct Location {
+    start_line : usize, start_column : usize,
+    end_line   : usize, end_column   : usize,
+}
+
+impl Location {
+    pub fn fake() -> Location {
+        Location { start_line : 0, start_column : 0,
+                   end_line   : 0, end_column   : 0 }
+    }
+}
+
+// Conversion from span to internal locations
+pub fn span_to_loc(span : Span, lexer : &dyn NonStreamingLexer<DefaultLexerTypes<u32>>)
+    -> Location {
+    let ((start_line, start_column), (end_line, end_column)) = lexer.line_col(span);
+    Location { start_line, start_column, end_line, end_column }
+}
+
+// Printing locations
+impl fmt::Display for Location {
+    fn fmt(&self, f : &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "{}, {} -- {}, {}",
+               self.start_line, self.start_column,
+               self.end_line,   self.end_column)
+    }
+}
diff --git a/juno_frontend/src/main.rs b/juno_frontend/src/main.rs
index 72855c0d..886c6365 100644
--- a/juno_frontend/src/main.rs
+++ b/juno_frontend/src/main.rs
@@ -7,6 +7,7 @@ mod dynconst;
 mod env;
 mod intrinsics;
 mod parser;
+mod locs;
 mod semant;
 mod ssa;
 mod types;
diff --git a/juno_frontend/src/semant.rs b/juno_frontend/src/semant.rs
index 7c4338bf..d573154e 100644
--- a/juno_frontend/src/semant.rs
+++ b/juno_frontend/src/semant.rs
@@ -14,6 +14,7 @@ use ordered_float::OrderedFloat;
 use crate::dynconst::DynConst;
 use crate::env::Env;
 use crate::intrinsics;
+use crate::locs::{Location, span_to_loc};
 use crate::parser::*;
 use crate::parser;
 use crate::types::{Either, Type, TypeSolver};
@@ -110,35 +111,6 @@ fn intern_package_name(
     res
 }
 
-// A location in the program, used in error messages
-pub struct Location {
-    start_line : usize, start_column : usize,
-    end_line   : usize, end_column   : usize,
-}
-
-impl Location {
-    fn fake() -> Location {
-        Location { start_line : 0, start_column : 0,
-                   end_line   : 0, end_column   : 0 }
-    }
-}
-
-// Conversion from span to internal locations
-fn span_to_loc(span : Span, lexer : &dyn NonStreamingLexer<DefaultLexerTypes<u32>>)
-    -> Location {
-    let ((start_line, start_column), (end_line, end_column)) = lexer.line_col(span);
-    Location { start_line, start_column, end_line, end_column }
-}
-
-// Printing locations
-impl fmt::Display for Location {
-    fn fmt(&self, f : &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}, {} -- {}, {}",
-               self.start_line, self.start_column,
-               self.end_line,   self.end_column)
-    }
-}
-
 // Error Messages
 pub enum ErrorMessage {
     NotImplemented(Location, String),
@@ -284,8 +256,7 @@ pub enum Expr {
     CallExpr  { func : usize, ty_args : Vec<Type>, dyn_consts : Vec<DynConst>,
                 args : Vec<Either<Expr, usize>>, typ : Type },
     Intrinsic { id : intrinsics::IntrinsicIdentity,
-                ty_args : Vec<Type>, dyn_consts : Vec<DynConst>,
-                args : Vec<Either<Expr, usize>>, typ : Type },
+                ty_args : Vec<Type>, args : Vec<Expr>, typ : Type },
 }
 
 #[derive(Clone, Debug)]
@@ -353,7 +324,7 @@ impl Expr {
             | Expr::CastExpr { expr : _, typ }
             | Expr::CondExpr { cond : _, thn : _, els : _, typ }
             | Expr::CallExpr { func : _, ty_args : _, dyn_consts : _, args : _, typ }
-            | Expr::Intrinsic { id : _, ty_args : _, dyn_consts : _, args : _, typ }
+            | Expr::Intrinsic { id : _, ty_args : _, args : _, typ }
             | Expr::Zero { typ }
             => *typ
         }
@@ -435,22 +406,12 @@ fn analyze_program(
                     kinds.push(kind);
 
                     match kind {
-                        Kind::Type => {
-                            let typ = types.new_type_var(nm, num_type, false, false);
-                            env.insert(nm, Entity::Type { type_args : vec![], value : typ });
-                            num_type += 1;
-                        },
                         Kind::USize => {
                             dyn_const_names.push(nm);
                             num_dyn_const += 1;
                         },
-                        Kind::Number => {
-                            let typ = types.new_type_var(nm, num_type, true, false);
-                            env.insert(nm, Entity::Type { type_args : vec![], value : typ });
-                            num_type += 1;
-                        },
-                        Kind::Integer => {
-                            let typ = types.new_type_var(nm, num_type, true, true);
+                        _ => {
+                            let typ = types.new_type_var(nm, num_type, kind);
                             env.insert(nm, Entity::Type { type_args : vec![], value : typ });
                             num_type += 1;
                         },
@@ -471,11 +432,25 @@ fn analyze_program(
                 env.close_scope();
                 env.insert(nm, Entity::Type { type_args : kinds, value : typ });
             },
-            parser::Top::ConstDecl { span : _, public: _, name, ty: _, body } => {
+            parser::Top::ConstDecl { span, public: _, name, ty, body } => {
                 // TODO: Handle public
                 let nm = intern_id(&name, lexer, &mut stringtab);
                 let val = process_expr_as_constant(body, 0, lexer, &mut stringtab,
                                                    &mut env, &mut types)?;
+
+                // Check type (if specified)
+                if ty.is_some() {
+                    let ty = process_type(ty.unwrap(), 0, lexer, &mut stringtab,
+                                          &env, &mut types, true)?;
+                    if !types.unify(ty, val.1) {
+                        return Err(singleton_error(
+                                ErrorMessage::TypeError(
+                                    span_to_loc(span, lexer),
+                                    unparse_type(&types, ty, &stringtab),
+                                    unparse_type(&types, val.1, &stringtab))));
+                    }
+                }
+
                 env.insert(nm, Entity::Constant { value : val });
             },
             parser::Top::FuncDecl { span, public: _, attr: _, name, ty_vars, args, ty, body } => {
@@ -497,18 +472,8 @@ fn analyze_program(
                             dyn_const_names.push(nm);
                             num_dyn_const += 1;
                         },
-                        Kind::Type => {
-                            let typ = types.new_type_var(nm, num_type_var, false, false);
-                            env.insert(nm, Entity::Type { type_args : vec![], value : typ });
-                            num_type_var += 1;
-                        },
-                        Kind::Number => {
-                            let typ = types.new_type_var(nm, num_type_var, true, false);
-                            env.insert(nm, Entity::Type { type_args : vec![], value : typ });
-                            num_type_var += 1;
-                        },
-                        Kind::Integer => {
-                            let typ = types.new_type_var(nm, num_type_var, true, true);
+                        _ => {
+                            let typ = types.new_type_var(nm, num_type_var, kind);
                             env.insert(nm, Entity::Type { type_args : vec![], value : typ });
                             num_type_var += 1;
                         },
@@ -529,13 +494,7 @@ fn analyze_program(
                 let mut errors = LinkedList::new();
 
                 for (inout, VarBind { span, pattern, typ }) in args {
-                    if !typ.is_some() {
-                        errors.push_back(
-                            ErrorMessage::NotImplemented(
-                                span_to_loc(span, lexer),
-                                "argument type inference".to_string()));
-                        continue;
-                    }
+                    let typ = typ.unwrap_or(parser::Type::WildType { span });
 
                     match pattern {
                         Pattern::Variable { span, name } => {
@@ -548,8 +507,9 @@ fn analyze_program(
                             }
 
                             let nm = intern_package_name(&name, lexer, &mut stringtab)[0];
-                            match process_type(typ.expect("FROM ABOVE"), num_dyn_const,
-                                               lexer, &mut stringtab, &env, &mut types) {
+                            match process_type(typ, num_dyn_const,
+                                               lexer, &mut stringtab, &env,
+                                               &mut types, true) {
                                 Ok(ty) => {
                                     if inout.is_some() {
                                         inout_args.push(arg_types.len());
@@ -568,29 +528,24 @@ fn analyze_program(
                     }
                 }
 
-                let return_type =
-                    match ty {
-                        None => {
-                            errors.push_back(
-                                ErrorMessage::NotImplemented(
-                                    span_to_loc(span, lexer),
-                                    "function return type inference".to_string()));
+                let return_type = {
+                    // A missing return type is implicitly void
+                    let ty = ty.unwrap_or(parser::Type::PrimType {
+                                            span : span,
+                                            typ : parser::Primitive::Void });
+                    match process_type(ty, num_dyn_const, lexer,
+                                       &mut stringtab, &env, &mut types,
+                                       true) {
+                        Ok(ty) => ty,
+                        Err(mut errs) => {
+                            errors.append(&mut errs);
                             types.new_primitive(types::Primitive::Unit)
                         },
-                        Some(ty) => {
-                            match process_type(ty, num_dyn_const, lexer,
-                                               &mut stringtab, &env, &mut types) {
-                                Ok(ty) => ty,
-                                Err(mut errs) => {
-                                    errors.append(&mut errs);
-                                    types.new_primitive(types::Primitive::Unit)
-                                },
-                            }
-                        },
-                    };
+                    }
+                };
 
                 if !errors.is_empty() {
-                    Err(errors)?
+                    return Err(errors);
                 }
 
                 // Compute the proper type accounting for the inouts (which become returns)
@@ -629,7 +584,7 @@ fn analyze_program(
                     // The end of a function being reachable (i.e. there is some possible path
                     // where there is no return statement) is an error unless the return type is
                     // void
-                    if types.is_void(return_type) {
+                    if types.unify_void(return_type) {
                         // Insert return at the end
                         body = Stmt::BlockStmt {
                             body : vec![
@@ -677,6 +632,19 @@ fn analyze_program(
                             "modules".to_string())))?
             },
         }
+
+        // After each top level construct, verify that our types are solved
+        // If not report an error
+        match types.solve() {
+            Ok(()) => (),
+            Err((kind, loc)) => {
+                return Err(singleton_error(
+                        ErrorMessage::SemanticError(
+                            loc,
+                            format!("unconstrained type, not constrained beyond {}",
+                                    kind.to_string()))));
+            },
+        }
     }
 
     Ok((types, res))
@@ -689,9 +657,9 @@ fn process_type_def(def : parser::TyDef, name : usize, num_dyn_const : usize,
   
     match def {
         parser::TyDef::TypeAlias { span: _, body } => {
-            process_type(body, num_dyn_const, lexer, stringtab, env, types)
+            process_type(body, num_dyn_const, lexer, stringtab, env, types, false)
         },
-        parser::TyDef::Struct { span: _, public: _, fields } => {
+        parser::TyDef::Struct { span : _, public: _, fields } => {
             // TODO: handle public correctly (and field public)
             
             let mut field_list = vec![];
@@ -709,7 +677,7 @@ fn process_type_def(def : parser::TyDef, name : usize, num_dyn_const : usize,
                     },
                     Some(ty) => {
                         match process_type(ty, num_dyn_const, lexer, stringtab,
-                                           env, types) {
+                                           env, types, false) {
                             Ok(typ) => {
                                 let idx = field_list.len();
                                 field_list.push(typ);
@@ -749,7 +717,7 @@ fn process_type_def(def : parser::TyDef, name : usize, num_dyn_const : usize,
                         },
                         Some(ty) => {
                             match process_type(ty, num_dyn_const, lexer, 
-                                               stringtab, env, types) {
+                                               stringtab, env, types, false) {
                                 Ok(typ) => {
                                     let idx = constr_list.len();
                                     constr_list.push(typ);
@@ -773,19 +741,29 @@ fn process_type_def(def : parser::TyDef, name : usize, num_dyn_const : usize,
 fn process_type(typ : parser::Type, num_dyn_const : usize,
                 lexer : &dyn NonStreamingLexer<DefaultLexerTypes<u32>>,
                 stringtab : &mut StringTable, env : &Env<usize, Entity>,
-                types : &mut TypeSolver) -> Result<Type, ErrorMessages> {
+                types : &mut TypeSolver, can_infer : bool) -> Result<Type, ErrorMessages> {
 
     match typ {
-        parser::Type::PrimType { span: _, typ } => {
+        parser::Type::PrimType { span : _, typ } => {
             Ok(types.new_primitive(convert_primitive(typ)))
         },
-        parser::Type::TupleType { span: _, tys } => {
+        parser::Type::WildType { span } => {
+            if can_infer {
+                Ok(types.new_of_kind(parser::Kind::Type, span_to_loc(span, lexer)))
+            } else {
+                Err(singleton_error(
+                        ErrorMessage::SemanticError(
+                            span_to_loc(span, lexer),
+                            "cannot infer type in this context".to_string())))
+            }
+        },
+        parser::Type::TupleType { span : _, tys } => {
             let mut fields = vec![];
             let mut errors = LinkedList::new();
 
             for ty in tys {
                 match process_type(ty, num_dyn_const, lexer, stringtab, env,
-                                   types) {
+                                   types, can_infer) {
                     Ok(t) => fields.push(t),
                     Err(mut errs) => errors.append(&mut errs),
                 }
@@ -812,6 +790,22 @@ fn process_type(typ : parser::Type, num_dyn_const : usize,
                 let nm = id[0];
                 match env.lookup(&nm) {
                     Some(Entity::Type { type_args, value }) => {
+                        if args.is_none() && type_args.len() != 0 && !can_infer {
+                            Err(singleton_error(
+                                    ErrorMessage::SemanticError(
+                                        span_to_loc(span, lexer),
+                                        format!("Expected {} type arguments, provided none",
+                                                type_args.len()))))?
+                        }
+
+                        // If we did not provide type arguments (but we can
+                        // infer types) then we make all of the type arguments
+                        // wild cards
+                        let args =
+                            args.unwrap_or_else(
+                                || vec![ parser::TypeExpr::WildcardType { span : span }
+                                       ; type_args.len() ]);
+
                         if args.len() != type_args.len() {
                             Err(singleton_error(
                                     ErrorMessage::SemanticError(
@@ -835,42 +829,19 @@ fn process_type(typ : parser::Type, num_dyn_const : usize,
                                         Ok(val) => dynamic_constants.push(val),
                                     }
                                 },
-                                parser::Kind::Type => {
+                                _ => {
                                     match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => type_vars.push(typ),
-                                    }
-                                },
-                                parser::Kind::Number => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
+                                            arg, num_dyn_const, lexer, stringtab,
+                                            env, types, can_infer) {
                                         Err(mut errs) => errors.append(&mut errs),
                                         Ok(typ) => {
-                                            if types.is_number(typ) {
+                                            if types.unify_kind(typ, *kind) {
                                                 type_vars.push(typ);
                                             } else {
                                                 errors.push_back(
                                                     ErrorMessage::KindError(
                                                         span_to_loc(arg_span, lexer),
-                                                        "number".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                                },
-                                parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
+                                                        kind.to_string(),
                                                         unparse_type(types, typ, stringtab)));
                                             }
                                         },
@@ -909,12 +880,12 @@ fn process_type(typ : parser::Type, num_dyn_const : usize,
                 }
             }
         },
-        parser::Type::ArrayType { span: _, elem, dims } => {
+        parser::Type::ArrayType { span : _, elem, dims } => {
             let mut dimensions = vec![];
             let mut errors = LinkedList::new();
 
             let element = process_type(*elem, num_dyn_const, lexer, stringtab,
-                                       env, types);
+                                       env, types, can_infer);
 
             for dim in dims {
                 match process_type_expr_as_expr(dim, num_dyn_const, lexer, 
@@ -957,6 +928,7 @@ fn process_type_expr_as_expr(exp : parser::TypeExpr, num_dyn_const : usize,
 
     match exp {
         parser::TypeExpr::PrimType { span, .. }
+        | parser::TypeExpr::WildcardType { span }
         | parser::TypeExpr::TupleType { span, .. }
         | parser::TypeExpr::ArrayTypeExpr { span, .. } =>
             Err(singleton_error(
@@ -976,7 +948,7 @@ fn process_type_expr_as_expr(exp : parser::TypeExpr, num_dyn_const : usize,
                 let nm = id[0];
                 match env.lookup(&nm) {
                     Some(Entity::DynConst { value }) => {
-                        if args.len() > 0 {
+                        if args.is_some() {
                             Err(singleton_error(
                                     ErrorMessage::SemanticError(
                                         span_to_loc(span, lexer),
@@ -1073,7 +1045,8 @@ fn process_type_expr_as_expr(exp : parser::TypeExpr, num_dyn_const : usize,
 fn process_type_expr_as_type(exp : parser::TypeExpr, num_dyn_const : usize,
                              lexer : &dyn NonStreamingLexer<DefaultLexerTypes<u32>>,
                              stringtab : &mut StringTable,
-                             env : &Env<usize, Entity>, types : &mut TypeSolver)
+                             env : &Env<usize, Entity>, types : &mut TypeSolver,
+                             can_infer : bool)
     -> Result<Type, ErrorMessages> {
 
     match exp {
@@ -1091,12 +1064,23 @@ fn process_type_expr_as_type(exp : parser::TypeExpr, num_dyn_const : usize,
         parser::TypeExpr::PrimType { span : _, typ } => {
             Ok(types.new_primitive(convert_primitive(typ)))
         },
+        parser::TypeExpr::WildcardType { span } => {
+            if can_infer {
+                Ok(types.new_of_kind(parser::Kind::Type, span_to_loc(span, lexer)))
+            } else {
+                Err(singleton_error(
+                        ErrorMessage::SemanticError(
+                            span_to_loc(span, lexer),
+                            "cannot infer type in this context".to_string())))
+            }
+        },
         parser::TypeExpr::TupleType { span : _, tys } => {
             let mut fields = vec![];
             let mut errors = LinkedList::new();
 
             for ty in tys {
-                match process_type_expr_as_type(ty, num_dyn_const, lexer, stringtab, env, types) {
+                match process_type_expr_as_type(ty, num_dyn_const, lexer, stringtab,
+                                                env, types, can_infer) {
                     Ok(t) => fields.push(t),
                     Err(mut errs) => errors.append(&mut errs),
                 }
@@ -1116,7 +1100,8 @@ fn process_type_expr_as_type(exp : parser::TypeExpr, num_dyn_const : usize,
             let mut dimensions = vec![];
             let mut errors = LinkedList::new();
 
-            let element = process_type_expr_as_type(*elem, num_dyn_const, lexer, stringtab, env, types);
+            let element = process_type_expr_as_type(*elem, num_dyn_const, lexer,
+                                                    stringtab, env, types, can_infer);
 
             for dim in dims {
                 match process_type_expr_as_expr(dim, num_dyn_const, lexer, stringtab, env, types) {
@@ -1158,6 +1143,19 @@ fn process_type_expr_as_type(exp : parser::TypeExpr, num_dyn_const : usize,
                 let nm = id[0];
                 match env.lookup(&nm) {
                     Some(Entity::Type { type_args, value }) => {
+                        if args.is_none() && type_args.len() != 0 && !can_infer {
+                            Err(singleton_error(
+                                    ErrorMessage::SemanticError(
+                                        span_to_loc(span, lexer),
+                                        format!("Expected {} type arguments, provided none",
+                                                type_args.len()))))?
+                        }
+
+                        let args =
+                            args.unwrap_or_else(
+                                || vec![ parser::TypeExpr::WildcardType { span : span }
+                                       ; type_args.len() ]);
+
                         if args.len() != type_args.len() {
                             Err(singleton_error(
                                     ErrorMessage::SemanticError(
@@ -1181,42 +1179,19 @@ fn process_type_expr_as_type(exp : parser::TypeExpr, num_dyn_const : usize,
                                         Ok(val) => dynamic_constants.push(val),
                                     }
                                 },
-                                parser::Kind::Type => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => type_vars.push(typ),
-                                    }
-                                },
-                                parser::Kind::Number => {
+                                _ => {
                                     match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
+                                            arg, num_dyn_const, lexer, stringtab,
+                                            env, types, can_infer) {
                                         Err(mut errs) => errors.append(&mut errs),
                                         Ok(typ) => {
-                                            if types.is_number(typ) {
+                                            if types.unify_kind(typ, *kind) {
                                                 type_vars.push(typ);
                                             } else {
                                                 errors.push_back(
                                                     ErrorMessage::KindError(
                                                         span_to_loc(arg_span, lexer),
-                                                        "number".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                                },
-                                parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
+                                                        kind.to_string(),
                                                         unparse_type(types, typ, stringtab)));
                                             }
                                         },
@@ -1290,7 +1265,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                             None => None,
                             Some(t) =>
                                 Some(process_type(t, num_dyn_const, lexer, 
-                                                  stringtab, env, types)?),
+                                                  stringtab, env, types, true)?),
                         };
 
                     let var = env.uniq();
@@ -1313,7 +1288,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                                                   is_const : false });
 
                     match ty {
-                        Some(ty) if !types.equal(ty, typ) => {
+                        Some(ty) if !types.unify(ty, typ) => {
                             Err(singleton_error(
                                     ErrorMessage::TypeError(
                                         exp_loc,
@@ -1353,7 +1328,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                             None => None,
                             Some(t) =>
                                 Some(process_type(t, num_dyn_const, lexer,
-                                                  stringtab, env, types)?),
+                                                  stringtab, env, types, true)?),
                         };
 
                     let var = env.uniq();
@@ -1376,7 +1351,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                                                   is_const : true });
 
                     match ty {
-                        Some(ty) if !types.equal(ty, typ) => {
+                        Some(ty) if !types.unify(ty, typ) => {
                             Err(singleton_error(
                                     ErrorMessage::TypeError(
                                         exp_loc,
@@ -1404,7 +1379,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
             // Perform the appropriate type checking
             match assign {
                 AssignOp::None   => {
-                    if !types.equal(exp_typ, typ) {
+                    if !types.unify(exp_typ, typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
@@ -1413,14 +1388,14 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                     }
                 },
                 AssignOp::Add | AssignOp::Sub | AssignOp::Mul | AssignOp::Div => {
-                    if !types.equal(exp_typ, typ) {
+                    if !types.unify(exp_typ, typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
                                     unparse_type(types, exp_typ, stringtab),
                                     unparse_type(types, typ, stringtab))))?
                     }
-                    if !types.is_number(exp_typ) {
+                    if !types.unify_kind(exp_typ, parser::Kind::Number) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
@@ -1430,14 +1405,14 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                 },
                 AssignOp::Mod | AssignOp::BitAnd | AssignOp::BitOr | AssignOp::Xor
                     | AssignOp::LShift | AssignOp::RShift => {
-                    if !types.equal(exp_typ, typ) {
+                    if !types.unify(exp_typ, typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
                                     unparse_type(types, exp_typ, stringtab),
                                     unparse_type(types, typ, stringtab))))?
                     }
-                    if !types.is_integer(exp_typ) {
+                    if !types.unify_kind(exp_typ, parser::Kind::Integer) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
@@ -1446,14 +1421,14 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                     }
                 },
                 AssignOp::LogAnd | AssignOp::LogOr => {
-                    if !types.equal(exp_typ, typ) {
+                    if !types.unify(exp_typ, typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
                                     unparse_type(types, exp_typ, stringtab),
                                     unparse_type(types, typ, stringtab))))?
                     }
-                    if !types.is_bool(exp_typ) {
+                    if !types.unify_bool(exp_typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(assign_span, lexer),
@@ -1554,7 +1529,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                 = append_errors3(cond_res, thn_res, els_res)?;
             let cond_typ = cond_exp.get_type();
 
-            if !types.is_bool(cond_typ) {
+            if !types.unify_bool(cond_typ) {
                 Err(singleton_error(
                         ErrorMessage::TypeError(
                             span_to_loc(cond_span, lexer),
@@ -1574,7 +1549,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                         span_to_loc(span, lexer),
                         "match statements".to_string())))
         },
-        parser::Stmt::ForStmt { span: _, var : VarBind { span : v_span, pattern, typ },
+        parser::Stmt::ForStmt { span : _, var : VarBind { span : v_span, pattern, typ },
                                 init, bound, step, body } => {
             let (var, var_name, var_type) =
                 match pattern {
@@ -1591,8 +1566,8 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                             match typ {
                                 None => types.new_primitive(types::Primitive::U64),
                                 Some(t) => {
-                                    let ty = process_type(t, num_dyn_const, lexer, stringtab, env, types)?;
-                                    if !types.is_integer(ty) {
+                                    let ty = process_type(t, num_dyn_const, lexer, stringtab, env, types, true)?;
+                                    if !types.unify_kind(ty, parser::Kind::Integer) {
                                         return Err(singleton_error(
                                                 ErrorMessage::SemanticError(
                                                     span_to_loc(v_span, lexer),
@@ -1649,14 +1624,14 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
 
             // Verify that the types of the initial value and bound are correct
             let mut type_errors = LinkedList::new();
-            if !types.equal(var_type, init_typ) {
+            if !types.unify(var_type, init_typ) {
                 type_errors.push_back(
                     ErrorMessage::TypeError(
                         span_to_loc(init_span, lexer),
                         unparse_type(types, var_type, stringtab),
                         unparse_type(types, init_typ, stringtab)));
             }
-            if !types.equal(var_type, bound_typ) {
+            if !types.unify(var_type, bound_typ) {
                 type_errors.push_back(
                     ErrorMessage::TypeError(
                         span_to_loc(bound_span, lexer),
@@ -1739,7 +1714,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                 = append_errors2(cond_res, body_res)?;
             let cond_typ = cond_val.get_type();
 
-            if !types.is_bool(cond_typ) {
+            if !types.unify_bool(cond_typ) {
                 Err(singleton_error(
                         ErrorMessage::TypeError(
                             span_to_loc(cond_span, lexer),
@@ -1755,7 +1730,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
         },
         parser::Stmt::ReturnStmt { span, expr } => {
             let return_val =
-                if expr.is_none() && types.is_void(return_type) {
+                if expr.is_none() && types.unify_void(return_type) {
                     Expr::Constant {
                         val : (Literal::Unit, return_type),
                         typ : return_type }
@@ -1769,7 +1744,7 @@ fn process_stmt(stmt : parser::Stmt, num_dyn_const : usize,
                     let val = process_expr(expr.unwrap(), num_dyn_const, lexer, stringtab, env,
                                            types)?;
                     let typ = val.get_type();
-                    if !types.equal(return_type, typ) {
+                    if !types.unify(return_type, typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -1966,7 +1941,7 @@ fn process_lexpr(expr : parser::LExpr, num_dyn_const : usize,
                     Err(mut errs) => errors.append(&mut errs),
                     Ok(exp) => {
                         let typ = exp.get_type();
-                        if !types.is_u64(typ) {
+                        if !types.unify_u64(typ) {
                             errors.push_back(
                                 ErrorMessage::TypeError(
                                     span_to_loc(idx_span, lexer),
@@ -2180,6 +2155,12 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     "struct name".to_string(),
                                     "non-struct type".to_string())))?
                     }
+
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if kinds.len() != ty_args.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -2204,47 +2185,24 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     Ok(val) => dyn_consts.push(val),
                                 }
                             },
-                            parser::Kind::Type => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
@@ -2297,7 +2255,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     match process_expr_as_constant(expr, num_dyn_const, lexer, stringtab, env, types) {
                                         Err(mut errs) => errors.append(&mut errs),
                                         Ok((lit, typ)) => {
-                                            if !types.equal(field_typ, typ) {
+                                            if !types.unify(field_typ, typ) {
                                                 // Set the value at this index even though there's
                                                 // an error so that we also report if the field is
                                                 // defined multiple times
@@ -2344,14 +2302,14 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
             let res = u64::from_str_radix(lexer.span_str(span), base.base());
             assert!(res.is_ok(), "Internal Error: Int literal is not an integer");
 
-            let num_typ = types.new_number();
+            let num_typ = types.new_of_kind(parser::Kind::Number, span_to_loc(span, lexer));
             Ok((Literal::Integer(res.unwrap()), num_typ))
         },
         parser::Expr::FloatLit { span } => {
             let res = lexer.span_str(span).parse::<f64>();
             assert!(res.is_ok(), "Internal Error: Float literal is not a float");
 
-            let float_typ = types.new_float();
+            let float_typ = types.new_of_kind(parser::Kind::Float, span_to_loc(span, lexer));
             Ok((Literal::Float(res.unwrap()), float_typ))
         },
         parser::Expr::UnaryExpr { span, op, expr } => {
@@ -2360,7 +2318,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
 
             match op {
                 parser::UnaryOp::Negation => {
-                    if !types.is_number(expr_typ) {
+                    if !types.unify_kind(expr_typ, parser::Kind::Number) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -2375,7 +2333,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                     }
                 },
                 parser::UnaryOp::BitwiseNot => {
-                    if !types.is_integer(expr_typ) {
+                    if !types.unify_kind(expr_typ, parser::Kind::Integer) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -2388,7 +2346,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                     }
                 },
                 parser::UnaryOp::LogicalNot => {
-                    if !types.is_bool(expr_typ) {
+                    if !types.unify_bool(expr_typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -2416,7 +2374,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
             match op {
                 // Equality and inequality work on any types
                 parser::BinaryOp::Eq | parser::BinaryOp::Neq => {
-                    if !types.equal(lhs_typ, rhs_typ) {
+                    if !types.unify(lhs_typ, rhs_typ) {
                         return Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(rhs_span, lexer),
@@ -2429,9 +2387,9 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                 | parser::BinaryOp::Div | parser::BinaryOp::Lt  | parser::BinaryOp::Le
                 | parser::BinaryOp::Gt  | parser::BinaryOp::Ge => {
                     let mut errors = LinkedList::new();
-                    let lhs_number = types.is_number(lhs_typ);
-                    let rhs_number = types.is_number(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_number = types.unify_kind(lhs_typ, parser::Kind::Number);
+                    let rhs_number = types.unify_kind(rhs_typ, parser::Kind::Number);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_number && !equal {
                         errors.push_back(
@@ -2469,9 +2427,9 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                 | parser::BinaryOp::Xor | parser::BinaryOp::LShift | parser::BinaryOp::RShift
                 => {
                     let mut errors = LinkedList::new();
-                    let lhs_integer = types.is_integer(lhs_typ);
-                    let rhs_integer = types.is_integer(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_integer = types.unify_kind(lhs_typ, parser::Kind::Integer);
+                    let rhs_integer = types.unify_kind(rhs_typ, parser::Kind::Integer);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_integer && !equal {
                         errors.push_back(
@@ -2507,9 +2465,9 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                 },
                 parser::BinaryOp::LogAnd | parser::BinaryOp::LogOr => {
                     let mut errors = LinkedList::new();
-                    let lhs_bool = types.is_bool(lhs_typ);
-                    let rhs_bool = types.is_bool(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_bool = types.unify_bool(lhs_typ);
+                    let rhs_bool = types.unify_bool(rhs_typ);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_bool && !equal {
                         errors.push_back(
@@ -2745,11 +2703,13 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
         parser::Expr::CastExpr { span, expr, typ } => {
             // Cast between numeric types
             let expr_res = process_expr_as_constant(*expr, num_dyn_const, lexer, stringtab, env, types);
-            let type_res = process_type(typ, num_dyn_const, lexer, stringtab, env, types);
+            // Inferring the type of a cast seems weird, so not allowing
+            let type_res = process_type(typ, num_dyn_const, lexer, stringtab, env, types, false);
 
             let ((expr_lit, expr_typ), to_typ) = append_errors2(expr_res, type_res)?;
 
-            if !types.is_number(expr_typ) || !types.is_number(to_typ) {
+            if !types.unify_kind(expr_typ, parser::Kind::Number)
+            || !types.unify_kind(to_typ, parser::Kind::Number) {
                 Err(singleton_error(
                         ErrorMessage::SemanticError(
                             span_to_loc(span, lexer),
@@ -2757,13 +2717,15 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     unparse_type(types, expr_typ, stringtab),
                                     unparse_type(types, to_typ, stringtab)))))
             } else {
-                if types.is_integer(to_typ) {
+                if types.unify_kind(to_typ, parser::Kind::Integer) {
                     Ok((match expr_lit {
                          Literal::Integer(i) => Literal::Integer(i),
                          Literal::Float(f)   => Literal::Integer(f as u64),
                          _ => panic!("Incorrect literal constructor"),
                        }, to_typ))
                 } else {
+                    assert!(types.unify_kind(to_typ, parser::Kind::Float),
+                            "Casting to type which is neither integer or float");
                     Ok((match expr_lit {
                          Literal::Integer(i) => Literal::Float(i as f64),
                          Literal::Float(f)   => Literal::Float(f),
@@ -2784,14 +2746,14 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
 
             let mut errors = LinkedList::new();
 
-            if !types.is_bool(cond_typ) {
+            if !types.unify_bool(cond_typ) {
                 errors.push_back(
                     ErrorMessage::TypeError(
                         span_to_loc(cond_span, lexer),
                         "bool".to_string(),
                         unparse_type(types, cond_typ, stringtab)));
             }
-            if !types.equal(thn_typ, els_typ) {
+            if !types.unify(thn_typ, els_typ) {
                 errors.push_back(
                     ErrorMessage::SemanticError(
                         span_to_loc(span, lexer),
@@ -2889,6 +2851,11 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                     
                     // Now, we know that we are constructing some union, we need to verify that
                     // the type arguments are appropriate
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if kinds.len() != ty_args.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -2911,47 +2878,24 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     Ok(val) => dyn_consts.push(val),
                                 }
                             },
-                            parser::Kind::Type => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
@@ -2995,7 +2939,7 @@ fn process_expr_as_constant(expr : parser::Expr, num_dyn_const : usize,
                                     exprs : args.into_iter().map(|(_, a)| a).collect::<Vec<_>>() },
                                 num_dyn_const, lexer, stringtab, env, types)?;
 
-                    if !types.equal(constr_typ, body_typ) {
+                    if !types.unify(constr_typ, body_typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -3115,7 +3059,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                     Err(mut errs) => errors.append(&mut errs),
                     Ok(exp) => {
                         let typ = exp.get_type();
-                        if !types.is_u64(typ) {
+                        if !types.unify_u64(typ) {
                             errors.push_back(
                                 ErrorMessage::TypeError(
                                     span_to_loc(idx_span, lexer),
@@ -3245,6 +3189,12 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                     "struct name".to_string(),
                                     "non-struct type".to_string())))?
                     }
+
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if kinds.len() != ty_args.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -3269,47 +3219,24 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                     Ok(val) => dyn_consts.push(val),
                                 }
                             },
-                            parser::Kind::Type => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
@@ -3363,7 +3290,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                         Err(mut errs) => errors.append(&mut errs),
                                         Ok(val) => {
                                             let val_typ = val.get_type();
-                                            if !types.equal(field_typ, val_typ) {
+                                            if !types.unify(field_typ, val_typ) {
                                                 // Set the value at this index even though there's
                                                 // an error so that we also report if the field is
                                                 // defined multiple times
@@ -3408,7 +3335,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
             let res = u64::from_str_radix(lexer.span_str(span), base.base());
             assert!(res.is_ok(), "Internal Error: Int literal is not an integer");
 
-            let num_typ = types.new_number();
+            let num_typ = types.new_of_kind(parser::Kind::Number, span_to_loc(span, lexer));
             Ok(Expr::Constant {
                 val : (Literal::Integer(res.unwrap()), num_typ),
                 typ : num_typ })
@@ -3417,7 +3344,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
             let res = lexer.span_str(span).parse::<f64>();
             assert!(res.is_ok(), "Internal Error: Float literal is not a float");
 
-            let float_typ = types.new_float();
+            let float_typ = types.new_of_kind(parser::Kind::Float, span_to_loc(span, lexer));
             Ok(Expr::Constant {
                 val : (Literal::Float(res.unwrap()), float_typ),
                 typ : float_typ })
@@ -3428,7 +3355,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
 
             match op {
                 parser::UnaryOp::Negation => {
-                    if !types.is_number(expr_typ) {
+                    if !types.unify_kind(expr_typ, parser::Kind::Number) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -3442,7 +3369,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                     }
                 },
                 parser::UnaryOp::BitwiseNot => {
-                    if !types.is_integer(expr_typ) {
+                    if !types.unify_kind(expr_typ, parser::Kind::Integer) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -3456,7 +3383,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                     }
                 },
                 parser::UnaryOp::LogicalNot => {
-                    if !types.is_bool(expr_typ) {
+                    if !types.unify_bool(expr_typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -3496,7 +3423,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
             match op {
                 // Equality and inequality work on any types
                 parser::BinaryOp::Eq | parser::BinaryOp::Neq => {
-                    if !types.equal(lhs_typ, rhs_typ) {
+                    if !types.unify(lhs_typ, rhs_typ) {
                         return Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(rhs_span, lexer),
@@ -3509,9 +3436,9 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                 | parser::BinaryOp::Div | parser::BinaryOp::Lt  | parser::BinaryOp::Le
                 | parser::BinaryOp::Gt  | parser::BinaryOp::Ge => {
                     let mut errors = LinkedList::new();
-                    let lhs_number = types.is_number(lhs_typ);
-                    let rhs_number = types.is_number(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_number = types.unify_kind(lhs_typ, parser::Kind::Number);
+                    let rhs_number = types.unify_kind(rhs_typ, parser::Kind::Number);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_number && !equal {
                         errors.push_back(
@@ -3550,9 +3477,9 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                 | parser::BinaryOp::Xor | parser::BinaryOp::LShift | parser::BinaryOp::RShift
                 => {
                     let mut errors = LinkedList::new();
-                    let lhs_integer = types.is_integer(lhs_typ);
-                    let rhs_integer = types.is_integer(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_integer = types.unify_kind(lhs_typ, parser::Kind::Integer);
+                    let rhs_integer = types.unify_kind(rhs_typ, parser::Kind::Integer);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_integer && !equal {
                         errors.push_back(
@@ -3589,9 +3516,9 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                 // These work on boolean inputs
                 parser::BinaryOp::LogAnd | parser::BinaryOp::LogOr => {
                     let mut errors = LinkedList::new();
-                    let lhs_bool = types.is_bool(lhs_typ);
-                    let rhs_bool = types.is_bool(rhs_typ);
-                    let equal = types.equal(lhs_typ, rhs_typ);
+                    let lhs_bool = types.unify_bool(lhs_typ);
+                    let rhs_bool = types.unify_bool(rhs_typ);
+                    let equal = types.unify(lhs_typ, rhs_typ);
 
                     if lhs_bool && !equal {
                         errors.push_back(
@@ -3677,12 +3604,14 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
             // For the moment at least, casting is only supported between numeric types, and all
             // numeric types can be cast to each other
             let expr_res = process_expr(*expr, num_dyn_const, lexer, stringtab, env, types);
-            let type_res = process_type(typ, num_dyn_const, lexer, stringtab, env, types);
+            // Inferring the type of a cast seems weird, so not allowing
+            let type_res = process_type(typ, num_dyn_const, lexer, stringtab, env, types, false);
 
             let (expr_val, to_typ) = append_errors2(expr_res, type_res)?;
             let expr_typ = expr_val.get_type();
 
-            if !types.is_number(expr_typ) || !types.is_number(to_typ) {
+            if !types.unify_kind(expr_typ, parser::Kind::Number)
+            || !types.unify_kind(to_typ, parser::Kind::Number) {
                 Err(singleton_error(
                         ErrorMessage::SemanticError(
                             span_to_loc(span, lexer),
@@ -3710,14 +3639,14 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
 
             let mut errors = LinkedList::new();
 
-            if !types.is_bool(cond_typ) {
+            if !types.unify_bool(cond_typ) {
                 errors.push_back(
                     ErrorMessage::TypeError(
                         span_to_loc(cond_span, lexer),
                         "bool".to_string(),
                         unparse_type(types, cond_typ, stringtab)));
             }
-            if !types.equal(thn_typ, els_typ) {
+            if !types.unify(thn_typ, els_typ) {
                 errors.push_back(
                     ErrorMessage::SemanticError(
                         span_to_loc(span, lexer),
@@ -3816,6 +3745,11 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
 
                     // Now, we know that we are constructing some union, we need to verify that
                     // the type arguments are appropriate
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if kinds.len() != ty_args.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -3838,47 +3772,24 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                     Ok(val) => dyn_consts.push(val),
                                 }
                             },
-                            parser::Kind::Type => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
@@ -3922,7 +3833,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                 num_dyn_const, lexer, stringtab, env, types)?;
                     let body_typ = body.get_type();
 
-                    if !types.equal(constr_typ, body_typ) {
+                    if !types.unify(constr_typ, body_typ) {
                         Err(singleton_error(
                                 ErrorMessage::TypeError(
                                     span_to_loc(span, lexer),
@@ -3940,6 +3851,11 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                     let func = *function;
 
                     // Verify that the type arguments are appropriate
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if kinds.len() != ty_args.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -3962,47 +3878,24 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                     Ok(val) => dyn_consts.push(val),
                                 }
                             },
-                            parser::Kind::Type => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
@@ -4064,7 +3957,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                             match process_expr(arg, num_dyn_const, lexer, stringtab, env, types) {
                                 Err(mut errs) => errors.append(&mut errs),
                                 Ok(Expr::Variable { var, typ }) => {
-                                    if !types.equal(arg_typ, typ) {
+                                    if !types.unify(arg_typ, typ) {
                                         errors.push_back(
                                             ErrorMessage::TypeError(
                                                 span_to_loc(arg_span, lexer),
@@ -4085,7 +3978,7 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                             match process_expr(arg, num_dyn_const, lexer, stringtab, env, types) {
                                 Err(mut errs) => errors.append(&mut errs),
                                 Ok(exp) => {
-                                    if !types.equal(arg_typ, exp.get_type()) {
+                                    if !types.unify(arg_typ, exp.get_type()) {
                                         errors.push_back(
                                             ErrorMessage::TypeError(
                                                 span_to_loc(arg_span, lexer),
@@ -4129,6 +4022,12 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                                 format!("Undefined intrinsic {}", nm)))),
                 Some(intrinsic) => {
                     let kinds = intrinsic.kinds;
+
+                    let ty_args =
+                        ty_args.unwrap_or_else(
+                            || vec! [ parser::TypeExpr::WildcardType { span : span }
+                                    ; kinds.len() ]);
+
                     if ty_args.len() != kinds.len() {
                         Err(singleton_error(
                                 ErrorMessage::SemanticError(
@@ -4138,122 +4037,66 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                     }
 
                     let mut type_vars = vec![];
-                    let mut dyn_consts = vec![];
                     let mut errors = LinkedList::new();
 
                     for (arg, kind) in ty_args.into_iter().zip(kinds.iter()) {
                         let arg_span = arg.span();
                         match kind {
                             parser::Kind::USize => {
-                                match process_type_expr_as_expr(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(val) => dyn_consts.push(val),
-                                }
+                                panic!("Intrinsics do not support dynamic constants");
                             },
-                            parser::Kind::Type => {
+                            _ => {
                                 match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
-                                    Err(mut errs) => errors.append(&mut errs),
-                                    Ok(typ) => type_vars.push(typ),
-                                }
-                            },
-                            parser::Kind::Number => {
-                                match process_type_expr_as_type(
-                                        arg, num_dyn_const, lexer, stringtab, env, types) {
+                                        arg, num_dyn_const, lexer, stringtab, env, types,
+                                        true) {
                                     Err(mut errs) => errors.append(&mut errs),
                                     Ok(typ) => {
-                                        if types.is_number(typ) {
+                                        if types.unify_kind(typ, *kind) {
                                             type_vars.push(typ);
                                         } else {
                                             errors.push_back(
                                                 ErrorMessage::KindError(
                                                     span_to_loc(arg_span, lexer),
-                                                    "number".to_string(),
+                                                    kind.to_string(),
                                                     unparse_type(types, typ, stringtab)));
                                         }
                                     },
                                 }
                             },
-                            parser::Kind::Integer => {
-                                    match process_type_expr_as_type(
-                                            arg, num_dyn_const, lexer, stringtab, env, types) {
-                                        Err(mut errs) => errors.append(&mut errs),
-                                        Ok(typ) => {
-                                            if types.is_integer(typ) {
-                                                type_vars.push(typ);
-                                            } else {
-                                                errors.push_back(
-                                                    ErrorMessage::KindError(
-                                                        span_to_loc(arg_span, lexer),
-                                                        "integer".to_string(),
-                                                        unparse_type(types, typ, stringtab)));
-                                            }
-                                        },
-                                    }
-                            },
                         }
                     }
 
                     if !errors.is_empty() { return Err(errors); }
 
-                    let arg_types = (intrinsic.args)(&type_vars, types);
-                    let return_typ = (intrinsic.ret_typ)(&type_vars, types);
+                    let (arg_types, return_typ) = (intrinsic.typ)(&type_vars, types);
 
                     // Now, process the arguments to ensure they has the type needed by this
-                    // constructor
-                    let mut arg_vals : Vec<Either<Expr, usize>> = vec![];
+                    // intrinsic
+                    let mut arg_vals : Vec<Expr> = vec![];
                     let mut errors = LinkedList::new();
 
-                    for ((is_inout, arg), (arg_typ, expect_inout))
+                    for ((is_inout, arg), arg_typ)
                         in args.into_iter().zip(arg_types.into_iter()) {
                     
                         let arg_span = arg.span();
 
-                        if is_inout && !expect_inout {
-                            errors.push_back(
-                                ErrorMessage::SemanticError(
-                                    span_to_loc(arg_span, lexer),
-                                    format!("Argument should be inout")));
-                        } else if !is_inout && expect_inout {
+                        if is_inout {
                             errors.push_back(
                                 ErrorMessage::SemanticError(
                                     span_to_loc(arg_span, lexer),
-                                    format!("Argument should not be inout")));
-                        } else if is_inout {
-                            // If the argument is an inout then it needs to just be a variable
-                            match process_expr(arg, num_dyn_const, lexer, stringtab, env, types) {
-                                Err(mut errs) => errors.append(&mut errs),
-                                Ok(Expr::Variable { var, typ }) => {
-                                    if !types.equal(arg_typ, typ) {
-                                        errors.push_back(
-                                            ErrorMessage::TypeError(
-                                                span_to_loc(arg_span, lexer),
-                                                unparse_type(types, arg_typ, stringtab),
-                                                unparse_type(types, typ, stringtab)));
-                                    } else {
-                                        arg_vals.push(Either::Right(var));
-                                    }
-                                },
-                                Ok(_) => {
-                                    errors.push_back(
-                                        ErrorMessage::SemanticError(
-                                            span_to_loc(arg_span, lexer),
-                                            format!("An inout argument must just be a variable")));
-                                },
-                            }
+                                    format!("Arguments to intrinsics cannot be inout")));
                         } else {
                             match process_expr(arg, num_dyn_const, lexer, stringtab, env, types) {
                                 Err(mut errs) => errors.append(&mut errs),
                                 Ok(exp) => {
-                                    if !types.equal(arg_typ, exp.get_type()) {
+                                    if !types.unify(arg_typ, exp.get_type()) {
                                         errors.push_back(
                                             ErrorMessage::TypeError(
                                                 span_to_loc(arg_span, lexer),
                                                 unparse_type(types, arg_typ, stringtab),
                                                 unparse_type(types, exp.get_type(), stringtab)));
                                     } else {
-                                        arg_vals.push(Either::Left(exp));
+                                        arg_vals.push(exp);
                                     }
                                 },
                             }
@@ -4266,7 +4109,6 @@ fn process_expr(expr : parser::Expr, num_dyn_const : usize,
                         Ok(Expr::Intrinsic {
                             id         : intrinsic.id,
                             ty_args    : type_vars,
-                            dyn_consts : dyn_consts,
                             args       : arg_vals,
                             typ        : return_typ })
                     }
diff --git a/juno_frontend/src/types.rs b/juno_frontend/src/types.rs
index d6e87666..53adbb57 100644
--- a/juno_frontend/src/types.rs
+++ b/juno_frontend/src/types.rs
@@ -3,6 +3,8 @@ use std::collections::{HashMap, HashSet, VecDeque};
 use crate::hercules_ir::ir::*;
 use crate::hercules_ir::build::*;
 use crate::dynconst::DynConst;
+use crate::parser;
+use crate::locs::Location;
 
 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
 pub enum Either<A, B> {
@@ -10,33 +12,88 @@ pub enum Either<A, B> {
     Right(B)
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, Debug)]
-pub enum Primitive { Bool, U8, I8, U16, I16, U32, I32, U64, I64, F32, F64, Unit }
-
-impl Primitive {
-    fn is_number(&self) -> bool {
-        match &self {
-            Primitive::U8 | Primitive::I8 | Primitive::U16
-                | Primitive::I16 | Primitive::U32 | Primitive::I32
-                | Primitive::U64 | Primitive::I64 | Primitive::F32
-                | Primitive::F64 => true,
-            _ => false,
+impl parser::Kind {
+    fn is_a(&self, other : parser::Kind) -> bool {
+        match other {
+            parser::Kind::USize => false,
+            parser::Kind::Type => true,
+            parser::Kind::Number =>
+                match self { parser::Kind::Number | parser::Kind::Integer
+                           | parser::Kind::Float => true,
+                             _ => false },
+            parser::Kind::Integer =>
+                match self { parser::Kind::Integer => true,
+                             _ => false },
+            parser::Kind::Float =>
+                match self { parser::Kind::Float => true,
+                             _ => false },
+        }
+    }
+
+    fn unify(&self, other : parser::Kind) -> Option<parser::Kind> {
+        match self {
+            parser::Kind::USize => None,
+            parser::Kind::Type => Some(other),
+            parser::Kind::Number =>
+                match other {
+                    parser::Kind::USize => None,
+                    parser::Kind::Type | parser::Kind::Number => Some(parser::Kind::Number),
+                    parser::Kind::Integer => Some(parser::Kind::Integer),
+                    parser::Kind::Float => Some(parser::Kind::Float),
+                },
+            parser::Kind::Integer =>
+                match other {
+                    parser::Kind::USize => None,
+                    parser::Kind::Type | parser::Kind::Number | parser::Kind::Integer
+                        => Some(parser::Kind::Integer),
+                    parser::Kind::Float => None,
+                },
+            parser::Kind::Float =>
+                match other {
+                    parser::Kind::USize => None,
+                    parser::Kind::Type | parser::Kind::Number | parser::Kind::Float
+                        => Some(parser::Kind::Float),
+                    parser::Kind::Integer => None,
+                },
         }
     }
-    
-    fn is_integer(&self) -> bool {
-        match &self {
-            Primitive::U8 | Primitive::I8 | Primitive::U16
-                | Primitive::I16 | Primitive::U32 | Primitive::I32
-                | Primitive::U64 | Primitive::I64 => true,
-            _ => false,
+
+    pub fn to_string(&self) -> String {
+        match self {
+            parser::Kind::USize     => "usize".to_string(),
+            parser::Kind::Type      => "type".to_string(),
+            parser::Kind::Number    => "number".to_string(),
+            parser::Kind::Integer   => "integer".to_string(),
+            parser::Kind::Float     => "float".to_string(),
         }
     }
-    
-    fn is_float(&self) -> bool {
-        match &self {
-            Primitive::F32 | Primitive::F64 => true,
-            _ => false,
+}
+
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
+pub enum Primitive { Bool, U8, I8, U16, I16, U32, I32, U64, I64, F32, F64, Unit }
+
+impl Primitive {
+    fn is_kind(&self, kind : parser::Kind) -> bool {
+        match kind {
+            parser::Kind::Type => true,
+            parser::Kind::USize => false,
+
+            parser::Kind::Number =>
+                match self { Primitive::U8  | Primitive::I8
+                           | Primitive::U16 | Primitive::I16
+                           | Primitive::U32 | Primitive::I32
+                           | Primitive::U64 | Primitive::I64
+                           | Primitive::F32 | Primitive::F64 => true,
+                           | _ => false },
+            parser::Kind::Integer =>
+                match self { Primitive::U8  | Primitive::I8
+                           | Primitive::U16 | Primitive::I16
+                           | Primitive::U32 | Primitive::I32
+                           | Primitive::U64 | Primitive::I64 => true,
+                           | _ => false },
+            parser::Kind::Float =>
+                match self { Primitive::F32 | Primitive::F64 => true,
+                           | _ => false },
         }
     }
 
@@ -67,16 +124,16 @@ pub struct Type { val : usize }
 // and tuples
 #[derive(Clone, Debug)]
 enum TypeForm {
-    Primitive(Primitive),
-    Tuple(Vec<Type>),
-    Array(Type, Vec<DynConst>),
+    Primitive { prim : Primitive },
+    Tuple { fields : Vec<Type> },
+    Array { elem : Type, dims : Vec<DynConst> },
 
     // This type is the same type as another type
-    OtherType(Type),
+    OtherType { other : Type },
 
     // For type variables, we record its name, its index (in the list of type variables in this
     // context), and anything we know about it (is it a number, is it an integer)
-    TypeVar { name : usize, index : usize, is_num : bool, is_int : bool },
+    TypeVar { name : usize, index : usize, kind : parser::Kind },
 
     // For structs and unions we record the name (via its interned representation), a UID, and the
     // types of its fields/constructors in a set order and a map from field/constructor names to
@@ -85,12 +142,13 @@ enum TypeForm {
     Union  { name : usize, id : usize, constr : Vec<Type>, names : HashMap<usize, usize> },
 
     // Constrained types
-    AnyNumber, AnyInteger, AnyFloat,
+    AnyOfKind { kind : parser::Kind, loc : Location },
 }
 
 #[derive(Debug)]
 pub struct TypeSolver {
     types : Vec<TypeForm>,
+    solved : usize, // which types have been "solved" (i.e. are known not to be AnyOfKinds)
 }
 
 #[derive(Debug)]
@@ -104,45 +162,36 @@ pub struct TypeSolverInst<'a> {
 
 impl TypeSolver {
     pub fn new() -> TypeSolver {
-        TypeSolver { types : vec![] }
-    }
-
-    pub fn new_number(&mut self) -> Type {
-        self.create_type(TypeForm::AnyNumber)
-    }
-
-    pub fn new_integer(&mut self) -> Type {
-        self.create_type(TypeForm::AnyInteger)
+        TypeSolver { types : vec![], solved : 0 }
     }
 
-    pub fn new_float(&mut self) -> Type {
-        self.create_type(TypeForm::AnyFloat)
+    pub fn new_of_kind(&mut self, kind : parser::Kind, loc : Location) -> Type {
+        self.create_type(TypeForm::AnyOfKind { kind, loc })
     }
 
-    pub fn new_primitive(&mut self, p : Primitive) -> Type {
-        self.create_type(TypeForm::Primitive(p))
+    pub fn new_primitive(&mut self, prim : Primitive) -> Type {
+        self.create_type(TypeForm::Primitive { prim })
     }
 
     pub fn new_tuple(&mut self, fields : Vec<Type>) -> Type {
-        self.create_type(TypeForm::Tuple(fields))
+        self.create_type(TypeForm::Tuple { fields })
     }
 
-    pub fn new_array(&mut self, element : Type, dims : Vec<DynConst>) -> Type {
-        self.create_type(TypeForm::Array(element, dims))
+    pub fn new_array(&mut self, elem : Type, dims : Vec<DynConst>) -> Type {
+        self.create_type(TypeForm::Array { elem, dims })
     }
 
-    pub fn new_type_var(&mut self, name : usize, index : usize, is_num : bool,
-                    is_int : bool) -> Type {
-        self.create_type(TypeForm::TypeVar { name, index, is_num, is_int })
+    pub fn new_type_var(&mut self, name : usize, index : usize, kind : parser::Kind) -> Type {
+        self.create_type(TypeForm::TypeVar { name, index, kind })
     }
 
     pub fn new_struct(&mut self, name : usize, id : usize, fields : Vec<Type>,
-                  names : HashMap<usize, usize>) -> Type {
+                      names : HashMap<usize, usize>) -> Type {
         self.create_type(TypeForm::Struct { name, id, fields, names })
     }
 
     pub fn new_union(&mut self, name : usize, id : usize, constr : Vec<Type>,
-                  names : HashMap<usize, usize>) -> Type {
+                     names : HashMap<usize, usize>) -> Type {
         self.create_type(TypeForm::Union { name, id, constr, names })
     }
 
@@ -152,78 +201,174 @@ impl TypeSolver {
         Type { val : idx }
     }
 
-    pub fn create_instance(&self, type_vars : Vec<TypeID>) -> TypeSolverInst {
-        let num_vars = self.types.len();
-        TypeSolverInst { solver    : self,
-                         type_vars : type_vars,
-                         solved    : vec![None; num_vars] }
-    }
-
-    pub fn is_u64(&mut self, Type { val } : Type) -> bool {
+    pub fn unify_void(&mut self, Type { val } : Type) -> bool {
         match &self.types[val] {
-            TypeForm::Primitive(Primitive::U64) => true,
-            TypeForm::OtherType(t) => self.is_u64(*t),
-            TypeForm::AnyNumber | TypeForm::AnyInteger => {
-                self.types[val] = TypeForm::Primitive(Primitive::U64);
+            TypeForm::Primitive { prim : Primitive::Unit, .. } => true,
+            TypeForm::OtherType { other, .. } => self.unify_void(*other),
+            TypeForm::AnyOfKind { kind : parser::Kind::Type, .. } => {
+                self.types[val] = TypeForm::Primitive { prim : Primitive::Unit };
                 true
             },
             _ => false,
         }
     }
 
-    pub fn is_bool(&mut self, Type { val } : Type) -> bool {
+    pub fn is_array(&self, Type { val } : Type) -> bool {
         match &self.types[val] {
-            TypeForm::Primitive(Primitive::Bool) => true,
-            TypeForm::OtherType(t) => self.is_bool(*t),
+            TypeForm::Array { .. } => true,
+            TypeForm::OtherType { other, .. } => self.is_array(*other),
             _ => false,
         }
     }
 
-    pub fn is_void(&mut self, Type { val } : Type) -> bool {
+    pub fn get_element_type(&self, Type { val } : Type) -> Option<Type> {
         match &self.types[val] {
-            TypeForm::Primitive(Primitive::Unit) => true,
-            TypeForm::OtherType(t) => self.is_void(*t),
-            _ => false,
+            TypeForm::Array { elem, .. } => Some(*elem),
+            TypeForm::OtherType { other, .. } => self.get_element_type(*other),
+            _ => None,
         }
     }
 
-    pub fn is_number(&mut self, Type { val } : Type) -> bool {
+    pub fn get_dimensions(&self, Type { val } : Type) -> Option<Vec<DynConst>> {
         match &self.types[val] {
-            TypeForm::Primitive(p) => p.is_number(),
-            TypeForm::OtherType(t) => self.is_number(*t),
-            TypeForm::AnyNumber | TypeForm::AnyInteger | TypeForm::AnyFloat => true,
-            TypeForm::TypeVar { name : _, index : _, is_num, .. } => *is_num,
-            _ => false,
+            TypeForm::Array { elem : _, dims, .. } => Some(dims.to_vec()),
+            TypeForm::OtherType { other, .. } => self.get_dimensions(*other),
+            _ => None,
         }
     }
 
-    pub fn is_integer(&mut self, Type { val } : Type) -> bool {
+    pub fn unify_bool(&mut self, Type { val } : Type) -> bool {
         match &self.types[val] {
-            TypeForm::Primitive(p) => p.is_integer(),
-            TypeForm::OtherType(t) => self.is_integer(*t),
-            TypeForm::TypeVar { name : _, index : _, is_num : _, is_int } => *is_int,
-            TypeForm::AnyInteger => true,
-            TypeForm::AnyNumber => {
-                self.types[val] = TypeForm::AnyInteger;
+            TypeForm::Primitive { prim : Primitive::Bool, .. } => true,
+            TypeForm::OtherType { other, .. } => self.unify_bool(*other),
+            TypeForm::AnyOfKind { kind : parser::Kind::Type, .. } => {
+                self.types[val] = TypeForm::Primitive { prim : Primitive::Bool };
                 true
             },
             _ => false,
         }
     }
-   
-    pub fn is_float(&mut self, Type { val } : Type) -> bool {
+
+    pub fn unify_u64(&mut self, Type { val } : Type) -> bool {
         match &self.types[val] {
-            TypeForm::Primitive(p) => p.is_float(),
-            TypeForm::OtherType(t) => self.is_float(*t),
-            TypeForm::AnyFloat => true,
-            TypeForm::AnyNumber => {
-                self.types[val] = TypeForm::AnyFloat;
-                true
+            TypeForm::Primitive { prim : Primitive::U64, .. } => true,
+            TypeForm::OtherType { other, .. } => self.unify_u64(*other),
+
+            TypeForm::AnyOfKind { kind, .. } => {
+                match kind {
+                    parser::Kind::Type | parser::Kind::Number
+                    | parser::Kind::Integer => {
+                        self.types[val] = TypeForm::Primitive { prim : Primitive::U64 };
+                        true
+                    },
+                    _ => false,
+                }
+            },
+
+            _ => false,
+        }
+    }
+
+    pub fn unify_kind(&mut self, Type { val } : Type, kind : parser::Kind) -> bool {
+        match &self.types[val] {
+            TypeForm::Primitive{ prim, .. } => prim.is_kind(kind),
+            TypeForm::OtherType { other, .. } => self.unify_kind(*other, kind),
+            TypeForm::TypeVar { name : _, index : _, kind : var_kind, .. } =>
+                var_kind.is_a(kind),
+
+            TypeForm::AnyOfKind { kind : ty_kind, loc } => {
+                match ty_kind.unify(kind) {
+                    None => false,
+                    Some(unified) => {
+                        self.types[val]
+                            = TypeForm::AnyOfKind { kind : unified, loc : *loc };
+                        true
+                    }
+                }
             },
+
             _ => false,
         }
     }
 
+    pub fn unify(&mut self, Type { val : ty1 } : Type, Type { val : ty2 } : Type) -> bool {
+        if let TypeForm::OtherType { other, .. } = self.types[ty1] {
+            return self.unify(other, Type { val : ty2 });
+        }
+        if let TypeForm::OtherType { other, .. } = self.types[ty2] {
+            return self.unify(Type { val : ty1 }, other);
+        }
+
+        match (&self.types[ty1], &self.types[ty2]) {
+            (TypeForm::Primitive { prim : p1, .. },
+             TypeForm::Primitive { prim : p2, .. }) => p1 == p2,
+
+            (TypeForm::Primitive { prim, .. },
+             TypeForm::AnyOfKind { kind, .. }) if prim.is_kind(*kind) => {
+                self.types[ty2] = TypeForm::OtherType { other : Type { val : ty1 } };
+                true
+            },
+            (TypeForm::TypeVar { name : _, index : _, kind : var_kind, .. },
+             TypeForm::AnyOfKind { kind, .. }) if var_kind.is_a(*kind) => {
+                self.types[ty2] = TypeForm::OtherType { other : Type { val : ty1 } };
+                true
+            },
+
+            (TypeForm::AnyOfKind { kind, .. },
+             TypeForm::Primitive { prim, .. }) if prim.is_kind(*kind) => {
+                self.types[ty1] = TypeForm::OtherType { other : Type { val : ty2 } };
+                true
+            },
+            (TypeForm::AnyOfKind { kind, .. },
+             TypeForm::TypeVar { name : _, index : _, kind : var_kind, .. })
+             if var_kind.is_a(*kind) => {
+                self.types[ty1] = TypeForm::OtherType { other : Type { val : ty2 } };
+                true
+            },
+
+            (TypeForm::Tuple { fields : f1, .. }, TypeForm::Tuple { fields : f2, .. })
+                if f1.len() == f2.len() => {
+                for (t1, t2) in f1.clone().iter().zip(f2.clone().iter()) {
+                    if !self.unify(*t1, *t2) { return false; }
+                }
+                true
+            },
+
+            (TypeForm::Array { elem : t1, dims : dm1, .. },
+             TypeForm::Array { elem : t2, dims : dm2, .. }) =>
+                dm1 == dm2 && self.unify(*t1, *t2),
+
+            (TypeForm::TypeVar { name : _, index : idx1, .. },
+             TypeForm::TypeVar { name : _, index : idx2, .. }) => idx1 == idx2,
+
+            (TypeForm::Struct { name : _, id : id1, fields : fs1, .. },
+             TypeForm::Struct { name : _, id : id2, fields : fs2, .. })
+            | (TypeForm::Union {name : _, id : id1, constr : fs1, .. },
+               TypeForm::Union {name : _, id : id2, constr : fs2, .. })
+              if id1 == id2 && fs1.len() == fs2.len() => {
+                for (t1, t2) in fs1.clone().iter().zip(fs2.clone().iter()) {
+                    if !self.unify(*t1, *t2) { return false; }
+                }
+                true
+            },
+
+            (TypeForm::AnyOfKind { kind : k1, loc : l1  },
+             TypeForm::AnyOfKind { kind : k2, .. }) => {
+                match k1.unify(*k2) {
+                    None => false,
+                    Some(kind) => {
+                        let loc = *l1;
+                        self.types[ty1] = TypeForm::AnyOfKind { kind, loc };
+                        self.types[ty2] = TypeForm::OtherType { other : Type { val : ty1 } };
+                        true
+                    },
+                }
+            },
+
+            _ => false,
+        }
+    }
+/*
     pub fn is_tuple(&self, Type { val } : Type) -> bool {
         match &self.types[val] {
             TypeForm::Tuple(_) => true,
@@ -247,11 +392,13 @@ impl TypeSolver {
             _ => panic!("Internal function get_fields used on non-tuple"),
         }
     }
+*/
 
+    // Return the type of the field (in a tuple) at a particular index
     pub fn get_index(&self, Type { val } : Type, idx : usize) -> Option<Type> {
         match &self.types[val] {
-            TypeForm::Tuple(fields) => fields.get(idx).copied(),
-            TypeForm::OtherType(t) => self.get_index(*t, idx),
+            TypeForm::Tuple { fields, .. } => fields.get(idx).copied(),
+            TypeForm::OtherType { other, .. } => self.get_index(*other, idx),
             _ => None,
         }
     }
@@ -259,7 +406,7 @@ impl TypeSolver {
     pub fn is_struct(&self, Type { val } : Type) -> bool {
         match &self.types[val] {
             TypeForm::Struct { .. } => true,
-            TypeForm::OtherType(t) => self.is_struct(*t),
+            TypeForm::OtherType { other, .. } => self.is_struct(*other),
             _ => false,
         }
     }
@@ -268,7 +415,7 @@ impl TypeSolver {
     pub fn get_num_struct_fields(&self, Type { val } : Type) -> Option<usize> {
         match &self.types[val] {
             TypeForm::Struct { name : _, id : _, fields, .. } => Some(fields.len()),
-            TypeForm::OtherType(t) => self.get_num_struct_fields(*t),
+            TypeForm::OtherType { other, .. } => self.get_num_struct_fields(*other),
             _ => None,
         }
     }
@@ -276,10 +423,10 @@ impl TypeSolver {
     // Returns the position and type of a field in a type (if it exists)
     pub fn get_field(&self, Type { val } : Type, name : usize) -> Option<(usize, Type)> {
         match &self.types[val] {
-            TypeForm::Struct { name : _, id : _, fields, names } => {
+            TypeForm::Struct { name : _, id : _, fields, names, .. } => {
                 names.get(&name).map(|idx| (*idx, fields[*idx]))
             },
-            TypeForm::OtherType(t) => self.get_field(*t, name),
+            TypeForm::OtherType { other, .. } => self.get_field(*other, name),
             _ => None,
         }
     }
@@ -289,11 +436,12 @@ impl TypeSolver {
         match &self.types[val] {
             TypeForm::Struct { name : _, id : _, fields, .. } =>
                 fields.get(idx).copied(),
-            TypeForm::OtherType(t) => self.get_struct_field_type(*t, idx),
+            TypeForm::OtherType { other, .. } => self.get_struct_field_type(*other, idx),
             _ => None,
         }
     }
 
+/*
     pub fn get_field_names(&self, Type { val } : Type) -> Option<Vec<usize>> {
         match &self.types[val] {
             TypeForm::Struct { name : _, id : _, fields : _, names } => {
@@ -303,47 +451,36 @@ impl TypeSolver {
             _ => None,
         }
     }
+*/
 
-    pub fn is_array(&self, Type { val } : Type) -> bool {
-        match &self.types[val] {
-            TypeForm::Array(_, _) => true,
-            TypeForm::OtherType(t) => self.is_array(*t),
-            _ => false,
-        }
-    }
-
-    pub fn get_element_type(&self, Type { val } : Type) -> Option<Type> {
+    pub fn get_num_dimensions(&self, Type { val } : Type) -> Option<usize> {
         match &self.types[val] {
-            TypeForm::Array(elem, _) => Some(*elem),
-            TypeForm::OtherType(t) => self.get_element_type(*t),
+            TypeForm::Array { elem : _, dims, .. } => Some(dims.len()),
+            TypeForm::OtherType { other, .. } => self.get_num_dimensions(*other),
             _ => None,
         }
     }
 
-    pub fn get_dimensions(&self, Type { val } : Type) -> Option<Vec<DynConst>> {
+    pub fn is_union(&self, Type { val } : Type) -> bool {
         match &self.types[val] {
-            TypeForm::Array(_, dims) => Some(dims.to_vec()),
-            TypeForm::OtherType(t) => self.get_dimensions(*t),
-            _ => None,
+            TypeForm::Union { .. } => true,
+            TypeForm::OtherType { other, .. } => self.is_union(*other),
+            _ => false,
         }
     }
 
-    pub fn get_num_dimensions(&self, Type { val } : Type) -> Option<usize> {
+    pub fn get_constructor_info(&self, Type { val } : Type, name : usize) 
+        -> Option<(usize, Type)> {
         match &self.types[val] {
-            TypeForm::Array(_, dims) => Some(dims.len()),
-            TypeForm::OtherType(t) => self.get_num_dimensions(*t),
+            TypeForm::Union { name : _, id : _, constr, names, .. } => {
+                names.get(&name).map(|idx| (*idx, constr[*idx]))
+            },
+            TypeForm::OtherType { other, .. } => self.get_constructor_info(*other, name),
             _ => None,
         }
     }
 
-    pub fn is_union(&self, Type { val } : Type) -> bool {
-        match &self.types[val] {
-            TypeForm::Union { .. } => true,
-            TypeForm::OtherType(t) => self.is_union(*t),
-            _ => false,
-        }
-    }
-    
+/*
     pub fn get_constructor_list(&self, Type { val } : Type) -> Option<Vec<usize>> {
         match &self.types[val] {
             TypeForm::Union { name : _, id : _, constr : _, names } => {
@@ -354,16 +491,6 @@ impl TypeSolver {
         }
     }
 
-    pub fn get_constructor_info(&self, Type { val } : Type, name : usize) 
-        -> Option<(usize, Type)> {
-        match &self.types[val] {
-            TypeForm::Union { name : _, id : _, constr, names} => {
-                names.get(&name).map(|idx| (*idx, constr[*idx]))
-            },
-            TypeForm::OtherType(t) => self.get_constructor_info(*t, name),
-            _ => None,
-        }
-    }
 
     fn is_type_var_num(&self, num : usize, Type { val } : Type) -> bool {
         match &self.types[val] {
@@ -372,130 +499,31 @@ impl TypeSolver {
             _ => false,
         }
     }
-
-    pub fn equal(&mut self, Type { val : ty1 } : Type, Type { val : ty2 } : Type) -> bool {
-        if let TypeForm::OtherType(ty) = self.types[ty1] {
-            return self.equal(ty, Type { val : ty2 });
-        }
-        if let TypeForm::OtherType(ty) = self.types[ty2] {
-            return self.equal(Type { val : ty1 }, ty);
-        }
-
-        match (self.types[ty1].clone(), self.types[ty2].clone()) {
-            (TypeForm::Primitive(p1), TypeForm::Primitive(p2)) => p1 == p2,
-
-            (TypeForm::Primitive(p), TypeForm::AnyNumber)  if p.is_number() => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-            (TypeForm::TypeVar { name : _, index : _, is_num, .. }, TypeForm::AnyNumber) if is_num => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-
-            (TypeForm::Primitive(p), TypeForm::AnyInteger) if p.is_integer() => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-            (TypeForm::TypeVar { name : _, index : _, is_num : _, is_int }, TypeForm::AnyInteger) if is_int => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-
-            (TypeForm::Primitive(p), TypeForm::AnyFloat)   if p.is_float() => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-
-            (TypeForm::AnyNumber,  TypeForm::Primitive(p)) if p.is_number() => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-            (TypeForm::AnyNumber, TypeForm::TypeVar { name : _, index : _, is_num, .. }) if is_num => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-            
-            (TypeForm::AnyInteger, TypeForm::Primitive(p)) if p.is_number() => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-            (TypeForm::AnyInteger, TypeForm::TypeVar { name : _, index : _, is_num : _, is_int }) if is_int => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-            
-            (TypeForm::AnyFloat,   TypeForm::Primitive(p)) if p.is_float() => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-
-            (TypeForm::Tuple(f1), TypeForm::Tuple(f2)) if f1.len() == f2.len() => {
-                for (t1, t2) in f1.iter().zip(f2.iter()) {
-                    if !self.equal(*t1, *t2) { return false; }
-                }
-                true
-            },
-
-            (TypeForm::Array(t1, dm1), TypeForm::Array(t2, dm2)) =>
-                self.equal(t1, t2) && dm1 == dm2,
-
-            (TypeForm::TypeVar { name : _, index : idx1, .. },
-             TypeForm::TypeVar { name : _, index : idx2, .. }) => idx1 == idx2,
-
-            (TypeForm::Struct { name : _, id : id1, fields : fs1, .. },
-             TypeForm::Struct { name : _, id : id2, fields : fs2, .. })
-            | (TypeForm::Union {name : _, id : id1, constr : fs1, .. },
-               TypeForm::Union {name : _, id : id2, constr : fs2, .. })
-              if id1 == id2 && fs1.len() == fs2.len() => {
-                for (t1, t2) in fs1.iter().zip(fs2.iter()) {
-                    if !self.equal(*t1, *t2) { return false; }
-                }
-                true
-            },
-
-            (TypeForm::AnyNumber | TypeForm::AnyInteger | TypeForm::AnyFloat, 
-             TypeForm::AnyNumber)
-            | (TypeForm::AnyInteger, TypeForm::AnyInteger)
-            | (TypeForm::AnyFloat,   TypeForm::AnyFloat) => {
-                self.types[ty2] = TypeForm::OtherType(Type { val : ty1 });
-                true
-            },
-            (TypeForm::AnyNumber, TypeForm::AnyInteger)
-            | (TypeForm::AnyNumber, TypeForm::AnyFloat) => {
-                self.types[ty1] = TypeForm::OtherType(Type { val : ty2 });
-                true
-            },
-
-            _ => false,
-        }
-    }
+*/
 
     pub fn to_string(&self, Type { val } : Type, stringtab : &dyn Fn(usize) -> String) 
         -> String {
         match &self.types[val] {
-            TypeForm::Primitive(p) => p.to_string(),
-            TypeForm::Tuple(fields) => {
+            TypeForm::Primitive { prim, .. } => prim.to_string(),
+            TypeForm::Tuple { fields, .. } => {
                 "(" .to_string()
                 + &fields.iter().map(|t| self.to_string(*t, stringtab)).collect::<Vec<_>>().join(", ")
                 + ")"
             },
-            TypeForm::Array(elem, dims) => {
+            TypeForm::Array { elem, dims, .. } => {
                 self.to_string(*elem, stringtab)
                 + "["
                 + &dims.iter().map(|d| d.to_string(stringtab)).collect::<Vec<_>>().join(", ")
                 + "]"
             },
-            TypeForm::OtherType(typ) => {
-                self.to_string(*typ, stringtab)
+            TypeForm::OtherType { other, .. } => {
+                self.to_string(*other, stringtab)
             },
             TypeForm::TypeVar { name, .. } | TypeForm::Struct { name, .. }
                 | TypeForm::Union { name, .. } => {
                 stringtab(*name)
             },
-            TypeForm::AnyNumber => "number".to_string(),
-            TypeForm::AnyInteger => "integer".to_string(),
-            TypeForm::AnyFloat => "float".to_string(),
+            TypeForm::AnyOfKind { kind, .. } => kind.to_string(),
         }
     }
 
@@ -504,13 +532,13 @@ impl TypeSolver {
     pub fn instantiate(&mut self, Type { val } : Type, type_vars : &Vec<Type>,
                        dynamic_constants : &Vec<DynConst>) -> Option<Type> {
         match self.types[val].clone() {
-            TypeForm::Primitive(_) => Some(Type { val }),
-            TypeForm::AnyNumber | TypeForm::AnyInteger | TypeForm::AnyFloat => {
-                Some(self.create_type(self.types[val].clone()))
+            TypeForm::Primitive { .. } => Some(Type { val }),
+            TypeForm::AnyOfKind { kind, loc } => {
+                Some(self.new_of_kind(kind, loc))
             },
-            TypeForm::OtherType(t) =>
-                self.instantiate(t, type_vars, dynamic_constants),
-            TypeForm::Tuple(fields) => {
+            TypeForm::OtherType { other, .. } =>
+                self.instantiate(other, type_vars, dynamic_constants),
+            TypeForm::Tuple { fields } => {
                 let mut types = vec![];
                 let mut changed = false;
                 for typ in fields {
@@ -518,10 +546,10 @@ impl TypeSolver {
                     changed = changed || typ.val != inst.val;
                     types.push(inst);
                 }
-                if changed { Some(self.create_type(TypeForm::Tuple(types))) }
+                if changed { Some(self.new_tuple(types)) }
                 else { Some(Type { val }) }
             },
-            TypeForm::Array(elem, dims) => {
+            TypeForm::Array { elem, dims } => {
                 let elem_typ = self.instantiate(elem, type_vars, dynamic_constants)?;
                 let mut subst_dims = vec![];
 
@@ -529,12 +557,11 @@ impl TypeSolver {
                     subst_dims.push(c.subst(dynamic_constants)?);
                 }
 
-                Some(self.create_type(TypeForm::Array(elem_typ, subst_dims)))
+                Some(self.new_array(elem_typ, subst_dims))
             },
-            TypeForm::TypeVar { name : _, index, is_num, is_int } => {
+            TypeForm::TypeVar { name : _, index, kind, .. } => {
                 let typ = type_vars[index];
-                assert!(!is_num || self.is_number(typ));
-                assert!(!is_int || self.is_integer(typ));
+                assert!(self.unify_kind(typ, kind));
                 Some(typ)
             },
             TypeForm::Struct { name, id, fields, names } => {
@@ -569,6 +596,29 @@ impl TypeSolver {
             },
         }
     }
+
+    // Used as type and function boundaries to ensure that no uncounstrained
+    // types remain
+    pub fn solve(&mut self) -> Result<(), (parser::Kind, Location)> {
+        for i in self.solved..self.types.len() {
+            match self.types[i] {
+                TypeForm::AnyOfKind { kind, loc } => return Err((kind, loc)),
+                _ => (),
+            }
+        }
+
+        self.solved = self.types.len();
+        Ok(())
+    }
+
+    pub fn create_instance(&self, type_vars : Vec<TypeID>) -> TypeSolverInst {
+        let num_vars = self.types.len();
+        assert!(self.solved == num_vars, "Cannot instantiate with unsolved variables");
+
+        TypeSolverInst { solver    : self,
+                         type_vars : type_vars,
+                         solved    : vec![None; num_vars] }
+    }
 }
 
 impl TypeSolverInst<'_> {
@@ -590,8 +640,9 @@ impl TypeSolverInst<'_> {
 
             let solution : Either<TypeID, usize> =
                 match &self.solver.types[typ] {
-                    TypeForm::Primitive(p) => Either::Left(Self::build_primitive(builder, *p)),
-                    TypeForm::Tuple(fields) => {
+                    TypeForm::Primitive { prim, .. } =>
+                        Either::Left(Self::build_primitive(builder, *prim)),
+                    TypeForm::Tuple { fields, .. } => {
                         let mut needs = None;
                         let mut i_fields = vec![];
 
@@ -608,14 +659,14 @@ impl TypeSolverInst<'_> {
                             Either::Left(Self::build_product(builder, i_fields))
                         }
                     },
-                    TypeForm::Array(Type { val }, dims) => {
+                    TypeForm::Array { elem : Type { val }, dims, .. } => {
                         match &self.solved[*val] {
                             Some(ty) =>
                                 Either::Left(Self::build_array(builder, *ty, dims)),
                             None => Either::Right(*val),
                         }
                     },
-                    TypeForm::OtherType(Type { val }) => {
+                    TypeForm::OtherType { other : Type { val }, .. } => {
                         match &self.solved[*val] {
                             Some(ty) => Either::Left(*ty), 
                             None => Either::Right(*val),
@@ -658,10 +709,9 @@ impl TypeSolverInst<'_> {
                             Either::Left(Self::build_union(builder, i_constr))
                         }
                     },
-                    TypeForm::AnyNumber | TypeForm::AnyInteger =>
-                        Either::Left(Self::build_primitive(builder, Primitive::I64)),
-                    TypeForm::AnyFloat =>
-                        Either::Left(Self::build_primitive(builder, Primitive::F64)),
+                    TypeForm::AnyOfKind { .. } => {
+                        panic!("TypeSolverInst only works on solved types which do not have AnyOfKinds")
+                    },
                 };
 
             match solution {
-- 
GitLab