Change the function type in the AST

Changes the representation of function types in the ast from

Typ_fn : typ -> typ

to

Typ_fn : typ list -> typ

to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just
multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to
forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...).

In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so

f : (x, y) -> z
f _ = ...

would be disallowed (as _ matches both x and y), forcing

f(_, _) = z

this would simply quite a few things,

Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax
how it is now.

Some issues I noticed when doing this refactoring:

Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function
arguments so maybe it still is.

Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong.

Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same.

14 files changed, 206 insertions, 207 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index b9ab21b2..1d0689e4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -296,7 +296,7 @@ let bool_typ = mk_id_typ (mk_id "bool")
 let string_typ = mk_id_typ (mk_id "string")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
 let tuple_typ typs = mk_typ (Typ_tup typs)
-let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff))
+let function_typ arg_typs ret_typ eff = mk_typ (Typ_fn (arg_typs, ret_typ, eff))
 
 let vector_typ n ord typ =
   mk_typ (Typ_app (mk_id "vector",
@@ -613,8 +613,11 @@ and string_of_typ_aux = function
   | Typ_var kid -> string_of_kid kid
   | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")"
   | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
-  | Typ_fn (typ_arg, typ_ret, eff) ->
-     string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+  | Typ_fn ([typ_arg], typ_ret, eff) ->
+     string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff     
+  | Typ_fn (typ_args, typ_ret, eff) ->
+     "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> "
+     ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
   | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2
   | Typ_exist (kids, nc, typ) ->
      "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"
@@ -901,8 +904,8 @@ module Typ = struct
     | Typ_internal_unknown, Typ_internal_unknown -> 0
     | Typ_id id1, Typ_id id2 -> Id.compare id1 id2
     | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2
-    | Typ_fn (t1,t2,e1), Typ_fn (t3,t4,e2) ->
-       (match compare t1 t3 with
+    | Typ_fn (ts1,t2,e1), Typ_fn (ts3,t4,e2) ->
+       (match Util.compare_list compare ts1 ts3 with
        | 0 -> (match compare t2 t4 with
          | 0 -> effect_compare e1 e2
          | n -> n)
@@ -1084,7 +1087,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) =
   | Typ_internal_unknown -> KidSet.empty
   | Typ_id _ -> KidSet.empty
   | Typ_var kid -> KidSet.singleton kid
-  | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
+  | Typ_fn (ts, t, _) -> List.fold_left KidSet.union (tyvars_of_typ t) (List.map tyvars_of_typ ts)
   | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t))
@@ -1345,7 +1348,8 @@ let rec locate_typ l (Typ_aux (typ_aux, _)) =
     | Typ_internal_unknown -> Typ_internal_unknown
     | Typ_id id -> Typ_id (locate_id l id)
     | Typ_var kid -> Typ_var (locate_kid l kid)
-    | Typ_fn (arg_typ, ret_typ, effect) -> Typ_fn (locate_typ l arg_typ, locate_typ l ret_typ, locate_effect l effect)
+    | Typ_fn (arg_typs, ret_typ, effect) ->
+       Typ_fn (List.map (locate_typ l) arg_typs, locate_typ l ret_typ, locate_effect l effect)
     | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ l typ1, locate_typ l typ2)
     | Typ_tup typs -> Typ_tup (List.map (locate_typ l) typs)
     | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid l) kids, locate_nc l constr, locate_typ l typ)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 9dafbcd8..bbe9463e 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -132,7 +132,7 @@ val vector_typ : nexp -> order -> typ -> typ
 val list_typ : typ -> typ
 val exc_typ : typ
 val tuple_typ : typ list -> typ
-val function_typ : typ -> typ -> effect -> typ
+val function_typ : typ list -> typ -> effect -> typ
 
 val no_effect : effect
 val mk_effect : base_effect_aux list -> effect
diff --git a/src/c_backend.ml b/src/c_backend.ml
index d58094ca..d825bbae 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -568,8 +568,7 @@ let cdef_ctyps ctx = function
   | CDEF_fundef (id, _, _, instrs) ->
      let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in
@@ -803,8 +802,7 @@ let compile_funcall l ctx id args typ =
       c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env
   in
   let arg_typs, ret_typ = match fn_typ with
-    | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-    | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+    | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
     | _ -> assert false
   in
   let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
@@ -1304,7 +1302,6 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
 
   | TD_variant (id, _, _, tus, _) ->
      let compile_tu = function
-       | Tu_aux (Tu_ty_id (Typ_aux (Typ_fn (typ, _, _), _), id), _) -> ctyp_of_typ ctx typ, id
        | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
      in
      let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
@@ -1540,8 +1537,7 @@ let rec compile_def ctx = function
      c_debug (lazy "Compiling VS");
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
@@ -1556,8 +1552,8 @@ let rec compile_def ctx = function
        with Type_error _ ->
          c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env
      in
-     let arg_typ, ret_typ = match fn_typ with
-       | Typ_fn (arg_typ, ret_typ, _) -> arg_typ, ret_typ
+     let arg_typs, ret_typ = match fn_typ with
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
 
@@ -1567,10 +1563,7 @@ let rec compile_def ctx = function
      (* The context must be updated before we call ctyp_of_typ on the argument types. *)
      let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
 
-     let arg_ctyps = match arg_typ with
-       | Typ_aux (Typ_tup arg_typs, _) -> List.map (ctyp_of_typ ctx) arg_typs
-       | _ -> [ctyp_of_typ ctx arg_typ]
-     in
+     let arg_ctyps =  List.map (ctyp_of_typ ctx) arg_typs in
      let ret_ctyp = ctyp_of_typ ctx ret_typ in
 
      (* Optimize and compile the expression to ANF. *)
@@ -2790,8 +2783,7 @@ let codegen_def' ctx = function
      (* Extract type information about the function from the environment. *)
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index dcb7a925..4e6e941d 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -182,9 +182,16 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
                                  | K_infer -> k.k <- K_Typ; Typ_var v
                                  | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
                    | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-               | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg),
-                                                            (to_ast_typ k_env def_ord ret),
-                                                            (to_ast_effects k_env efct))
+               | Parse_ast.ATyp_fn(arg,ret,efct) ->
+                  begin match arg with
+                  | Parse_ast.ATyp_aux (Parse_ast.ATyp_tup args, _) ->
+                     Typ_fn (List.map (to_ast_typ k_env def_ord) args,
+                             (to_ast_typ k_env def_ord ret),
+                             (to_ast_effects k_env efct))
+                  | _ -> Typ_fn ([to_ast_typ k_env def_ord arg],
+                                 (to_ast_typ k_env def_ord ret),
+                                 (to_ast_effects k_env efct))
+                  end
                | Parse_ast.ATyp_bidir (typ1, typ2) -> Typ_bidir ( (to_ast_typ k_env def_ord typ1),
                                                                   (to_ast_typ k_env def_ord typ2))
                | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs)
@@ -1093,11 +1100,11 @@ let quant_item_arg = function
 let undefined_typschm id typq =
   let qis = quant_items typq in
   if qis = [] then
-    mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef])))
+    mk_typschm typq (function_typ [unit_typ] (mk_typ (Typ_id id)) (mk_effect [BE_undef]))
   else
-    let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in
+    let arg_typs = List.concat (List.map quant_item_typ qis) in
     let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
-    mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
+    mk_typschm typq (function_typ arg_typs ret_typ (mk_effect [BE_undef]))
 
 let have_undefined_builtins = ref false
 
@@ -1132,6 +1139,10 @@ let generate_undefineds vs_ids (Defs defs) =
        mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
     | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
   in
+  let p_tup = function
+    | [pat] -> pat
+    | pats -> mk_pat (P_tup pats)
+  in
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
@@ -1144,13 +1155,13 @@ let generate_undefineds vs_ids (Defs defs) =
                                mk_exp (E_app (mk_id "internal_pick",
                                               [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
-       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
-       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        let body =
          if !opt_fast_undefined && List.length tus > 0 then
            undefined_tu (List.hd tus)
@@ -1256,7 +1267,7 @@ let generate_enum_functions vs_ids (Defs defs) =
          else
            [ enum_val_spec name
               [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)]
-              (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
+              (function_typ [atom_typ (nvar kid)] (mk_typ (Typ_id id)) no_effect);
              mk_fundef [funcl] ]
        in
 
@@ -1273,7 +1284,7 @@ let generate_enum_functions vs_ids (Defs defs) =
          in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect);
+           [ enum_val_spec name [] (function_typ [mk_typ (Typ_id id)] to_typ no_effect);
              mk_fundef [funcl] ]
        in
        enum :: to_enum @ from_enum @ gen_enums defs
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index aaf1672a..f7a481e6 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -135,7 +135,7 @@ let subst_src_typ substs t =
     | Typ_id _
     | Typ_var _
       -> ty
-    | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp substs t1, s_styp substs t2,e))
+    | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e))
     | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
     | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
     | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
@@ -353,7 +353,7 @@ let rec contains_exist (Typ_aux (ty,l)) =
   | Typ_id _
   | Typ_var _
     -> false
-  | Typ_fn (t1,t2,_) -> contains_exist t1 || contains_exist t2
+  | Typ_fn (t1,t2,_) -> List.exists contains_exist t1 || contains_exist t2
   | Typ_bidir (t1, t2) -> contains_exist t1 || contains_exist t2
   | Typ_tup ts -> List.exists contains_exist ts
   | Typ_app (_,args) -> List.exists contains_exist_arg args
@@ -519,7 +519,8 @@ let refine_constructor refinements l env id args =
   | (_,irefinements) -> begin
     let (_,constr_ty) = Env.get_val_spec id env in
     match constr_ty with
-    | Typ_aux (Typ_fn (constr_ty,_,_),_) -> begin
+    (* A constructor should always have a single argument. *)
+    | Typ_aux (Typ_fn ([constr_ty],_,_),_) -> begin
        let arg_ty = typ_of_args args in
        match Type_check.destruct_exist env constr_ty with
        | None -> None
@@ -2302,14 +2303,9 @@ let rewrite_size_parameters env (Defs defs) =
     let pat,guard,exp,pannot = destruct_pexp pexp in
     let env = env_of_annot (l,ann) in
     let _, typ = Env.get_val_spec_orig id env in
-    let typ = match typ with
-      | Typ_aux (Typ_fn (arg_typ,_,_),_) -> arg_typ
-      | _ -> typ (* TODO: error *)
-    in
-    let types =
-      match pat, Env.expand_synonyms env typ with
-      | P_aux (P_tup ps,_), Typ_aux (Typ_tup ts,_) -> ts
-      | _, _ -> [typ]
+    let types = match typ with
+      | Typ_aux (Typ_fn (arg_typs,_,_),_) -> List.map (Env.expand_synonyms env) arg_typs
+      | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function clause does not have a function type")
     in
     let add_parameter (i,nmap) typ =
       let nmap =
@@ -2451,10 +2447,8 @@ in *)
             let typschm = match typschm with
               | TypSchm_aux (TypSchm_ts (tq,typ),l) ->
                  let typ = match typ with
-                   | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) ->
-                      Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2)
-                   | Typ_aux (Typ_fn (typ,t2,eff),l2) ->
-                      Typ_aux (Typ_fn (replace_type env typ,t2,eff),l2)
+                   | Typ_aux (Typ_fn (ts,t2,eff),l2) ->
+                      Typ_aux (Typ_fn (mapat (replace_type env) to_change ts,t2,eff),l2)
                    | _ -> replace_type env typ
                  in TypSchm_aux (TypSchm_ts (tq,typ),l)
             in
@@ -4168,9 +4162,10 @@ let replace_nexp_in_typ env typ orig new_nexp =
     | Typ_var _
         -> false, typ
     | Typ_fn (arg,res,eff) ->
-       let f1, arg = aux arg in
+       let arg' = List.map aux arg in
+       let f1 = List.exists fst arg' in
        let f2, res = aux res in
-       f1 || f2, Typ_aux (Typ_fn (arg, res, eff),l)
+       f1 || f2, Typ_aux (Typ_fn (List.map snd arg', res, eff),l)
     | Typ_bidir (t1, t2) ->
        let f1, t1 = aux t1 in
        let f2, t2 = aux t2 in
@@ -4223,9 +4218,10 @@ let rewrite_toplevel_nexps (Defs defs) =
   let rec rewrite_typ_in_spec env nexp_map (Typ_aux (t,ann) as typ_full) =
     match t with
     | Typ_fn (args,res,eff) ->
-       let nexp_map, args = rewrite_typ_in_spec env nexp_map args in
+       let args' = List.map (rewrite_typ_in_spec env nexp_map) args in
+       let nexp_map = List.concat (List.map fst args') in
        let nexp_map, res = rewrite_typ_in_spec env nexp_map res in
-       nexp_map, Typ_aux (Typ_fn (args,res,eff),ann)
+       nexp_map, Typ_aux (Typ_fn (List.map snd args',res,eff),ann)
     | Typ_tup typs ->
        let nexp_map, typs =
          List.fold_right (fun typ (nexp_map,t) ->
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 5df41a80..62a56c3d 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -142,7 +142,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
   | Typ_app (id, []) -> ocaml_typ_id ctx id
   | Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
   | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
-  | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
+  | Typ_fn (typs, typ, _) -> separate space [ocaml_typ ctx (Typ_aux (Typ_tup typs, l)); string "->"; ocaml_typ ctx typ]
   | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types")
   | Typ_var kid -> zencode_kid kid
   | Typ_exist _ -> assert false
@@ -455,15 +455,15 @@ let ocaml_funcls ctx =
   function
   | [] -> failwith "Ocaml: empty function"
   | [FCL_aux (FCL_Funcl (id, pexp),_)] ->
-     let typ1, typ2 =
+     let arg_typs, ret_typ =
        match Bindings.find id ctx.val_specs with
-       | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+       | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
        | _ -> failwith "Found val spec which was not a function!"
      in
      (* Any remaining type variables after simple_typ rewrite should
         indicate Type-polymorphism. If we have it, we need to generate
         explicit type signatures with universal quantification. *)
-     let kids = KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2) in
+     let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
      let pat_sym = gensym () in
      let pat, exp =
        match pexp with
@@ -473,7 +473,7 @@ let ocaml_funcls ctx =
      let annot_pat =
        let pat =
          if KidSet.is_empty kids then
-           parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1)
+           parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
          else
            ocaml_pat ctx pat
        in
@@ -482,18 +482,18 @@ let ocaml_funcls ctx =
        else pat
      in
      let call_header = function_header () in
-     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
+     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
      let call =
        if KidSet.is_empty kids then
          separate space [call_header; zencode ctx id;
-                         annot_pat; colon; ocaml_typ ctx typ2; equals;
+                         annot_pat; colon; ocaml_typ ctx ret_typ; equals;
                          sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
          ^//^ ocaml_exp ctx exp
          ^^ rparen
        else
          separate space [call_header; zencode ctx id; colon;
                          separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
-                         ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2; equals;
+                         ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
                          string "fun"; annot_pat; string "->";
                          sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
          ^//^ ocaml_exp ctx exp
@@ -502,18 +502,18 @@ let ocaml_funcls ctx =
      ocaml_funcl call string_of_arg string_of_ret
   | funcls ->
      let id = funcls_id funcls in
-     let typ1, typ2 =
+     let arg_typs, ret_typ =
        match Bindings.find id ctx.val_specs with
-       | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+       | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
        | _ -> failwith "Found val spec which was not a function!"
      in
-     let kids = KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2) in
+     let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
      if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
      let pat_sym = gensym () in
      let call_header = function_header () in
-     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
+     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
      let call =
-       separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); equals;
+       separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
                        sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
        ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
        ^^ rparen
@@ -806,8 +806,7 @@ let ocaml_pp_generators ctx defs orig_types required =
       in
       let make_variant (Tu_aux (Tu_ty_id (typ,id),_)) =
         let arg_typs = match typ with
-          | Typ_aux (Typ_fn (Typ_aux (Typ_tup typs,_),_,_),_) -> typs
-          | Typ_aux (Typ_fn (typ,_,_),_) -> [typ]
+          | Typ_aux (Typ_fn (typs,_,_),_) -> typs
           | Typ_aux (Typ_tup typs,_) -> typs
           | _ -> [typ]
         in
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 2c6c1381..1fb35158 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -128,8 +128,8 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   (* following the structure of parser for precedence *)
   let rec typ ty = fn_typ ty
   and fn_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_fn(arg,ret,efct) ->
-     separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct]
+  | Typ_fn(args,ret,efct) ->
+     separate space [parens (separate_map (comma ^^ space) tup_typ args); arrow; fn_typ ret; string "effect"; doc_effects efct]
   | Typ_bidir (t1, t2) ->
      separate space [tup_typ t1; bidir; tup_typ t2]
   | _ -> tup_typ ty
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b4fc4a72..806234d6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -264,7 +264,7 @@ let rec coq_nvars_of_typ (Typ_aux (t,l)) =
   match t with
   | Typ_id _ -> KidSet.empty
   | Typ_var kid -> tyvars_of_nexp (orig_nexp (nvar kid))
-  | Typ_fn (t1,t2,_) -> KidSet.union (trec t1) (trec t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left KidSet.union (trec t2) (List.map trec t1)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KidSet.union s (trec t))
        KidSet.empty ts
@@ -395,15 +395,12 @@ let doc_typ, doc_atomic_typ =
   let rec typ ty = fn_typ true ty
     and typ' ty = fn_typ false ty
     and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_fn(arg,ret,efct) ->
+      | Typ_fn(args,ret,efct) ->
          let ret_typ =
            if effectful efct
            then separate space [string "M"; fn_typ true ret]
            else separate space [fn_typ false ret] in
-         let arg_typs = match arg with
-           | Typ_aux (Typ_tup typs, _) ->
-              List.map (app_typ false) typs
-           | _ -> [tup_typ false arg] in
+         let arg_typs = List.map (app_typ false) args in
          let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in
          (* once we have proper excetions we need to know what the exceptions type is *)
          if atyp_needed then parens tpp else tpp
@@ -641,7 +638,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
   | Typ_id _
   | Typ_var _
     -> NexpSet.empty
-  | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1)
   | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
   | Typ_app (Id_aux (Id "vector",_),
              [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
@@ -689,18 +686,12 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
         (* Following the type checker to get the subpattern types, TODO perhaps ought
            to persuade the type checker to output these somehow. *)
        let (typq, ctor_typ) = Env.get_val_spec id env in
-       let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
-         | Typ_tup [Typ_aux (Typ_tup typs,_)] -> typs
-         | Typ_tup typs -> typs
-         | _ -> [typ]
-       in
        let arg_typs =
          match Env.expand_synonyms env ctor_typ with
-         | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+         | Typ_aux (Typ_fn (arg_typs, ret_typ, _), _) ->
             (* The FIXME comes from the typechecker code, not sure what it's about... *)
             let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
-            let arg_typ' = subst_unifiers unifiers arg_typ in
-            untuple arg_typ'
+            List.map (subst_unifiers unifiers) arg_typs
          | _ -> assert false
        in
        let ppp = doc_unop (doc_id_ctor id)
@@ -1144,10 +1135,7 @@ let doc_exp, doc_let =
             else doc_id f, false, false in
           let (tqs,fn_ty) = Env.get_val_spec_orig f env in
           let arg_typs, ret_typ, eff = match fn_ty with
-            | Typ_aux (Typ_fn (arg_typ,ret_typ,eff),_) ->
-               (match arg_typ with
-               | Typ_aux (Typ_tup typs,_) -> typs, ret_typ, eff
-               | _ -> [arg_typ], ret_typ, eff)
+            | Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff
             | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type")
           in
           let inst =
@@ -1923,8 +1911,8 @@ let merge_var_patterns map pats =
 let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let env = env_of_annot annot in
   let (tq,typ) = Env.get_val_spec_orig id env in
-  let (arg_typ, ret_typ, eff) = match typ with
-    | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff
+  let (arg_typs, ret_typ, eff) = match typ with
+    | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff
     | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
   in
   let build_ex, ret_typ = replace_atom_return_type ret_typ in
@@ -1935,7 +1923,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
-  let pats, bind = untuple_args_pat arg_typ pat in
+  let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *)
   let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
   let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
   let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
@@ -2135,7 +2123,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
 let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
   let typ_env = add_typquant l tqs typ_env in
   match typ with
-  | Typ_aux (Typ_fn (args_ty, ret_ty, eff),l') ->
+  | Typ_aux (Typ_fn (typs, ret_ty, eff),l') ->
      let check_typ (args,used) typ =
        match Type_check.destruct_atom_nexp typ_env typ with
        | Some (Nexp_aux (Nexp_var kid,_)) ->
@@ -2144,7 +2132,6 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
        | Some _ -> args, used
        | _ -> args, KidSet.union used (tyvars_of_typ typ)
      in
-     let typs = match args_ty with Typ_aux (Typ_tup typs,_) -> typs | _ -> [args_ty] in
      let args, used = List.fold_left check_typ (KidSet.empty, KidSet.empty) typs in
      let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in
      let tqs = match tqs with
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index d7f403a4..232c3aee 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -219,7 +219,7 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
   match t with
   | Typ_id _ -> NexpSet.empty
   | Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid))
-  | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (trec t2) (List.map trec t1)
   | Typ_tup ts ->
      List.fold_left (fun s t -> NexpSet.union s (trec t))
        NexpSet.empty ts
@@ -258,15 +258,12 @@ let doc_typ_lem, doc_atomic_typ_lem =
   let rec typ ty = fn_typ true ty
     and typ' ty = fn_typ false ty
     and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_fn(arg,ret,efct) ->
+      | Typ_fn(args,ret,efct) ->
          let ret_typ =
            if effectful efct
            then separate space [string "M"; fn_typ true ret]
            else separate space [fn_typ false ret] in
-         let arg_typs = match arg with
-           | Typ_aux (Typ_tup typs, _) ->
-              List.map (app_typ false) typs
-           | _ -> [tup_typ false arg] in
+         let arg_typs = List.map (app_typ false) args in
          let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in
          (* once we have proper excetions we need to know what the exceptions type is *)
          if atyp_needed then parens tpp else tpp
@@ -443,7 +440,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
     | Typ_id _
     | Typ_var _
       -> NexpSet.empty
-    | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2)
+    | Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts)
     | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
     | Typ_app (Id_aux (Id "vector",_),
                [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
@@ -531,7 +528,7 @@ let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
   | Typ_tup ts -> List.exists typ_needs_printed ts
   | Typ_app (Id_aux (Id "itself",_),_) -> true
   | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs
-  | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2
+  | Typ_fn (ts,t,_) -> List.exists typ_needs_printed ts || typ_needs_printed t
   | Typ_exist (kids,_,t) ->
      let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in
      typ_needs_printed t && KidSet.is_empty visible_kids
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7b843ebe..8f78b7dc 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -134,7 +134,7 @@ let doc_nc =
     | _ -> atomic_nc nc
   in
   nc0
-
+  
 let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -154,11 +154,11 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
      braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
-  | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) ->
-     separate space [doc_typ typ1; string "->"; doc_typ typ2]
-  | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) ->
+  | Typ_fn (typs, typ, Effect_aux (Effect_set [], _)) ->
+     separate space [doc_arg_typs typs; string "->"; doc_typ typ]
+  | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
      let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in
-     separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff]
+     separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
   | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
@@ -167,6 +167,9 @@ and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
   | Typ_arg_typ typ -> doc_typ typ
   | Typ_arg_nexp nexp -> doc_nexp nexp
   | Typ_arg_order o -> doc_ord o
+and doc_arg_typs = function
+  | [typ] -> doc_typ typ
+  | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 7a085213..6203dedf 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -255,8 +255,8 @@ let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
 
 let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
   let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with
-    | Typ_fn (arg_t, ret_t, eff) ->
-       Typ_aux (Typ_fn (rewrite_typ env arg_t, rewrite_typ env ret_t, eff), l)
+    | Typ_fn (arg_ts, ret_t, eff) ->
+       Typ_aux (Typ_fn (List.map (rewrite_typ env) arg_ts, rewrite_typ env ret_t, eff), l)
     | Typ_tup ts ->
        Typ_aux (Typ_tup (List.map (rewrite_typ env) ts), l)
     | Typ_exist (kids, c, typ) ->
@@ -658,14 +658,8 @@ let rewrite_sizeof (Defs defs) =
         let kid_typs = List.map (fun kid -> atom_typ (nvar kid))
                                 (KidSet.elements (Bindings.find id params_map)) in
         let typ' = match typ with
-          | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) ->
-             let vtyp_arg' = begin
-                 match vtyp_arg with
-                 | Typ_aux (Typ_tup typs, vl) ->
-                    Typ_aux (Typ_tup (kid_typs @ typs), vl)
-                 | _ -> Typ_aux (Typ_tup (kid_typs @ [vtyp_arg]), vl)
-               end in
-             Typ_aux (Typ_fn (vtyp_arg', vtyp_ret, declared_eff), vl)
+          | Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) ->
+             Typ_aux (Typ_fn (kid_typs @ vtyp_args, vtyp_ret, declared_eff), vl)
           | _ ->
             raise (Reporting_basic.err_typ l "val spec with non-function type") in
         TypSchm_aux (TypSchm_ts (tq, typ'), l)
@@ -2139,7 +2133,11 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
              | P_aux (P_app (constr_id, args), pannot) ->
                 let argstup_typ = tuple_typ (List.map pat_typ_of args) in
                 let pannot' = swaptyp argstup_typ pannot in
-                let pat' = P_aux (P_tup args, pannot') in
+                let pat' =
+                  match args with
+                  | [arg] -> arg
+                  | _ -> P_aux (P_tup args, pannot')
+                in
                 let pexp' = construct_pexp (pat', guard, exp, annot) in
                 let aux_fun_id = prepend_id (fun_name ^ "_") constr_id in
                 let aux_funcl = FCL_aux (FCL_Funcl (aux_fun_id, pexp'), pannot') in
@@ -2185,7 +2183,15 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
            union_effects eff (effect_of exp))
         no_effect funcls
       in
-      let fun_typ = function_typ args_typ ret_typ eff in
+      let fun_typ =
+        (* Because we got the argument type from a pattern we need to
+           do this. *)
+        match args_typ with
+        | Typ_aux (Typ_tup (args_typs), _) ->
+           function_typ args_typs ret_typ eff
+        | _ ->
+           function_typ [args_typ] ret_typ eff
+      in
       let quant_new_tyvars qis =
         let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in
         let typ_tyvars = tyvars_of_typ fun_typ in
@@ -2283,7 +2289,7 @@ let rewrite_fix_val_specs (Defs defs) =
             type synonyms nested in existentials might cause problems).
             A more robust solution would be to make the (global) environment
             more easily available to the pretty-printer. *)
-         let args_t' = Env.expand_synonyms (env_of exp) args_t in
+         let args_t' = List.map (Env.expand_synonyms (env_of exp)) args_t in
          let ret_t' = Env.expand_synonyms (env_of exp) ret_t in
          (tq, Typ_aux (Typ_fn (args_t', ret_t', eff'), a)), eff'
       | _ -> assert false (* find_vs must return a function type *)
@@ -2457,7 +2463,7 @@ and simple_typ_aux = function
   | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
      Typ_id (mk_id "int")
   | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map simple_typ arg_typs, simple_typ ret_typ, effs)
   | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
   | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
   | typ_aux -> typ_aux
@@ -3145,7 +3151,7 @@ let construct_toplevel_string_append_func env f_id pat =
                                                                        | typs -> tuple_typ typs
                                                             ), unk)]
   in
-  let fun_typ = (mk_typ (Typ_fn (string_typ, option_typ, no_effect))) in
+  let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in
   let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
@@ -4028,7 +4034,7 @@ let remove_reference_types exp =
     | Typ_app (Id_aux (Id "reg",_), [Typ_arg_aux (Typ_arg_typ (Typ_aux (t_aux2, _)), _)]) ->
       rewrite_t_aux t_aux2
     | Typ_app (name,t_args) -> Typ_app (name,List.map rewrite_t_arg t_args)
-    | Typ_fn (t1,t2,eff) -> Typ_fn (rewrite_t t1,rewrite_t t2,eff)
+    | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map rewrite_t arg_typs, rewrite_t ret_typ, eff)
     | Typ_tup ts -> Typ_tup (List.map rewrite_t ts)
     | _ -> t_aux
   and rewrite_t_arg t_arg = match t_arg with
@@ -4336,10 +4342,10 @@ let rewrite_defs_realise_mappings (Defs defs) =
       | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l
       | _ -> Type_check.typ_error l "non-bidir type of mapping?"
     in
-    let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), l) in
-    let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), l) in
-    let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), l) in
-    let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), l) in
+    let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), l) in
+    let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), l) in
+    let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in
+    let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in
 
     let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
     let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
@@ -4377,7 +4383,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
     let prefix_wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_exp (E_lit (mk_lit L_unit))])))) in
     let string_defs =
       begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
-              let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
@@ -4387,7 +4393,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
               forwards_prefix_spec @ forwards_prefix_fun
             else
               if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
-                let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+                let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
@@ -4512,9 +4518,7 @@ let make_cstr_mappings env ids m =
     (fun id ->
       let _,ty = Env.get_val_spec id env in
       let args = match ty with
-        | Typ_aux (Typ_fn (Typ_aux (Typ_tup [Typ_aux (Typ_tup tys,_)],_),_,_),_)
-        | Typ_aux (Typ_fn (Typ_aux (Typ_tup tys,_),_,_),_)
-          -> List.map (fun _ -> RP_any) tys
+        | Typ_aux (Typ_fn (tys,_,_),_) -> List.map (fun _ -> RP_any) tys
         | _ -> [RP_any]
       in RP_app (id,args)) ids in
   let rec aux ids acc l =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 44440ecf..56c488ff 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -88,8 +88,8 @@ let nameset_bigunion = List.fold_left Nameset.union mt
 let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with
   | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt
   | Typ_id name -> Nameset.add (string_of_id name) mt
-  | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1)
-                          (free_type_names_t consider_var t2)
+  | Typ_fn (arg_typs,ret_typ,_) ->
+     List.fold_left Nameset.union (free_type_names_t consider_var ret_typ) (List.map (free_type_names_t consider_var) arg_typs)
   | Typ_bidir (t1, t2) -> Nameset.union (free_type_names_t consider_var t1)
                                         (free_type_names_t consider_var t2)
   | Typ_tup ts -> free_type_names_ts consider_var ts
@@ -120,7 +120,8 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
     then conditional_add_typ bound used (Ast.Id_aux (Ast.Id v,l))
     else used
   | Typ_id id -> conditional_add_typ bound used id
-  | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret
+  | Typ_fn(arg,ret,_) ->
+     fv_of_typ consider_var bound (List.fold_left Nameset.union Nameset.empty (List.map (fv_of_typ consider_var bound used) arg)) ret
   | Typ_bidir(t1, t2) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *)
   | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used
   | Typ_app(id,targs) ->
diff --git a/src/specialize.ml b/src/specialize.ml
index 81c8b0b0..4d7a997f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -65,7 +65,8 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
     | Typ_tup typs -> Typ_tup (List.map nexp_simp_typ typs)
     | Typ_app (f, args) -> Typ_app (f, List.map nexp_simp_typ_arg args)
     | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ)
-    | Typ_fn (typ1, typ2, effect) -> Typ_fn (nexp_simp_typ typ1, nexp_simp_typ typ2, effect)
+    | Typ_fn (arg_typs, ret_typ, effect) ->
+       Typ_fn (List.map nexp_simp_typ arg_typs, nexp_simp_typ ret_typ, effect)
     | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2)
     | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   in
@@ -137,8 +138,8 @@ let string_of_instantiation instantiation =
     | Typ_var kid -> kid_name kid
     | Typ_tup typs -> "(" ^ Util.string_of_list ", " string_of_typ typs ^ ")"
     | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
-    | Typ_fn (typ_arg, typ_ret, eff) ->
-       string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+    | Typ_fn (arg_typs, ret_typ, eff) ->
+       "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff
     | Typ_bidir (t1, t2) ->
        string_of_typ t1 ^ " <-> " ^ string_of_typ t2
     | Typ_exist (kids, nc, typ) ->
@@ -257,7 +258,8 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
   | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
@@ -273,7 +275,8 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_int_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_int_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_int_frees ~exs:exs typ1) (typ_int_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.fold_left KidSet.union (typ_int_frees ~exs:exs ret_typ) (List.map (typ_int_frees ~exs:exs) arg_typs)
   | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_int_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 565d1eed..e1232046 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -183,7 +183,7 @@ and strip_typ_aux : typ_aux -> typ_aux = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id id -> Typ_id (strip_id id)
   | Typ_var kid -> Typ_var (strip_kid kid)
-  | Typ_fn (typ1, typ2, effect) -> Typ_fn (strip_typ typ1, strip_typ typ2, strip_effect effect)
+  | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map strip_typ arg_typs, strip_typ ret_typ, strip_effect effect)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (strip_typ typ1, strip_typ typ2)
   | Typ_tup typs -> Typ_tup (List.map strip_typ typs)
   | Typ_exist (kids, constr, typ) -> Typ_exist ((List.map strip_kid kids), strip_n_constraint constr, strip_typ typ)
@@ -253,7 +253,7 @@ and typ_subst_nexp_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
@@ -270,7 +270,7 @@ and typ_subst_typ_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args)
@@ -293,7 +293,7 @@ and typ_subst_order_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args)
@@ -309,7 +309,7 @@ and typ_subst_kid_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args)
@@ -602,7 +602,7 @@ end = struct
     match typ with
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
-    | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
+    | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ, effs), l)
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l)
     | Typ_app (id, args) ->
        begin
@@ -658,7 +658,7 @@ end = struct
     match typ_aux with
     | Typ_internal_unknown
     | Typ_id _ | Typ_var _ -> typ
-    | Typ_fn (arg_typ, ret_typ, effect) -> Typ_aux (Typ_fn (map_nexps f arg_typ, map_nexps f ret_typ, effect), l)
+    | Typ_fn (arg_typs, ret_typ, effect) -> Typ_aux (Typ_fn (List.map (map_nexps f) arg_typs, map_nexps f ret_typ, effect), l)
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2), l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (map_nexps f) typs), l)
     | Typ_exist (kids, nc, typ) -> Typ_aux (Typ_exist (kids, nc, map_nexps f typ), l)
@@ -699,8 +699,8 @@ end = struct
 
   let rec canonicalize env typ =
     match typ with
-    | Typ_aux (Typ_fn (arg_typ, ret_typ, effects), l) when is_canonical env arg_typ ->
-       Typ_aux (Typ_fn (arg_typ, canonicalize env ret_typ, effects), l)
+    | Typ_aux (Typ_fn (arg_typs, ret_typ, effects), l) when List.for_all (is_canonical env) arg_typs ->
+       Typ_aux (Typ_fn (arg_typs, canonicalize env ret_typ, effects), l)
     | Typ_aux (Typ_fn _, l) -> typ_error l ("Function type " ^ string_of_typ typ ^ " is not canonical")
     | _ ->
        let existentials, constrs, (Typ_aux (typ_aux, l) as typ) = canonical env typ in
@@ -735,7 +735,7 @@ end = struct
       | exception Not_found ->
          typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
-    | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret
+    | Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ
     | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 ->
        typ_error l "Bidirectional types cannot be the same on both sides"
     | Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2
@@ -859,10 +859,10 @@ end = struct
       let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
       let backwards_id = mk_id (string_of_id id ^ "_backwards") in
       let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
-      let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), Parse_ast.Unknown) in
-      let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), Parse_ast.Unknown) in
-      let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), Parse_ast.Unknown) in
-      let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), Parse_ast.Unknown) in
+      let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in
+      let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in
+      let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in
+      let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in
       let env =
         { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings }
         |> add_val_spec forwards_id (typq, forwards_typ)
@@ -872,10 +872,10 @@ end = struct
       in
       let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
       begin if strip_typ typ1 = string_typ then
-              let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               add_val_spec prefix_id (typq, forwards_prefix_typ) env
             else if strip_typ typ2 = string_typ then
-              let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               add_val_spec prefix_id (typq, backwards_prefix_typ) env
             else
               env
@@ -946,7 +946,7 @@ end = struct
           | args -> mk_typ (Typ_app (id, args))
         in
         let fold_accessors accs (typ, fid) =
-          let acc_typ = mk_typ (Typ_fn (rectyp, typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          let acc_typ = mk_typ (Typ_fn ([rectyp], typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
           typ_print (lazy (indent 1 ^ "Adding accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
           Bindings.add (field_name id fid) (typq, acc_typ) accs
         in
@@ -962,7 +962,8 @@ end = struct
 
   let get_accessor rec_id id env =
     match get_accessor_fn rec_id id env with
-    | (typq, Typ_aux (Typ_fn (rec_typ, field_typ, effect), _)) ->
+    (* All accessors should have a single argument (the record itself) *)
+    | (typq, Typ_aux (Typ_fn ([rec_typ], field_typ, effect), _)) ->
        (typq, rec_typ, field_typ, effect)
     | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id))
 
@@ -1144,8 +1145,8 @@ end = struct
     let rec aux (Typ_aux (t,a)) =
       let rewrap t = Typ_aux (t,a) in
       match t with
-      | Typ_fn (t1, t2, eff) ->
-        rewrap (Typ_fn (aux t1, aux t2, eff))
+      | Typ_fn (arg_typs, ret_typ, eff) ->
+        rewrap (Typ_fn (List.map aux arg_typs, aux ret_typ, eff))
       | Typ_tup ts ->
         rewrap (Typ_tup (List.map aux ts))
       | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) when string_of_id r = "register" ->
@@ -1288,7 +1289,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) =
   | Typ_id _ -> true
   | Typ_tup typs -> List.for_all is_typ_monomorphic typs
   | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args
-  | Typ_fn (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
+  | Typ_fn (arg_typs, ret_typ, _) -> List.for_all is_typ_monomorphic arg_typs && is_typ_monomorphic ret_typ
   | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
   | Typ_exist _ | Typ_var _ -> false
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
@@ -1450,8 +1451,8 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.concat (List.map typ_nexps typs)
   | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
   | Typ_exist (kids, nc, typ) -> typ_nexps typ
-  | Typ_fn (typ1, typ2, _) ->
-     typ_nexps typ1 @ typ_nexps typ2
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
   | Typ_bidir (typ1, typ2) ->
      typ_nexps typ1 @ typ_nexps typ2
 and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) =
@@ -1469,7 +1470,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) -> List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
   | Typ_bidir (typ1, typ2) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -1517,8 +1518,9 @@ let typ_identical env typ1 typ2 =
     match typ1, typ2 with
     | Typ_id v1, Typ_id v2 -> Id.compare v1 v2 = 0
     | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 = 0
-    | Typ_fn (arg_typ1, ret_typ1, eff1), Typ_fn (arg_typ2, ret_typ2, eff2) ->
-       typ_identical' arg_typ1 arg_typ2
+    | Typ_fn (arg_typs1, ret_typ1, eff1), Typ_fn (arg_typs2, ret_typ2, eff2)
+         when List.length arg_typs1 = List.length arg_typs2 ->
+       List.for_all2 typ_identical' arg_typs1 arg_typs2
        && typ_identical' ret_typ1 ret_typ2
        && strip_effect eff1 = strip_effect eff2
     | Typ_bidir (typ1, typ2), Typ_bidir (typ3, typ4) ->
@@ -1850,7 +1852,7 @@ let rec alpha_equivalent env typ1 typ2 =
       match aux with
       | Typ_internal_unknown -> Typ_internal_unknown
       | Typ_id _ | Typ_var _ -> aux
-      | Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff)
+      | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map relabel arg_typs, relabel ret_typ, eff)
       | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2)
       | Typ_tup typs -> Typ_tup (List.map relabel typs)
       | Typ_exist (kids, nc, typ) ->
@@ -2236,7 +2238,8 @@ let rec filter_casts env from_typ to_typ casts =
      begin
        let (quant, cast_typ) = Env.get_val_spec cast env in
        match cast_typ with
-       | Typ_aux (Typ_fn (cast_from_typ, cast_to_typ, _), _)
+       (* A cast should be a function A -> B and have only a single argument type. *)
+       | Typ_aux (Typ_fn ([cast_from_typ], cast_to_typ, _), _)
             when match_typ env from_typ cast_from_typ && match_typ env to_typ cast_to_typ ->
           typ_print (lazy ("Considering cast " ^ string_of_typ cast_typ ^ " for " ^ string_of_typ from_typ ^ " to " ^ string_of_typ to_typ));
           cast :: filter_casts env from_typ to_typ casts
@@ -2400,11 +2403,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
         print_endline ("Solved " ^ string_of_nexp nexp ^ " = " ^ Big_int.to_string n);
         annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
      end
-  (* All constructors are treated as having one argument so Ctor(x, y)
-     is checked as Ctor((x, y)) *)
-  | E_app (ctor, x :: y :: zs), _ when Env.is_union_constructor ctor env ->
-     typ_print (lazy ("Checking multiple argument constructor: " ^ string_of_id ctor));
-     crule check_exp env (mk_exp ~loc:l (E_app (ctor, [mk_exp ~loc:l (E_tuple (x :: y :: zs))]))) typ
+  (* All constructors and mappings are treated as having one argument
+     so Ctor(x, y) is checked as Ctor((x, y)) *)
+  | E_app (f, x :: y :: zs), _ when Env.is_union_constructor f env || Env.is_mapping f env ->
+     typ_print (lazy ("Checking multiple argument constructor or mapping: " ^ string_of_id f));
+     crule check_exp env (mk_exp ~loc:l (E_app (f, [mk_exp ~loc:l (E_tuple (x :: y :: zs))]))) typ
   | E_app (mapping, xs), _ when Env.is_mapping mapping env ->
      let forwards_id = mk_id (string_of_id mapping ^ "_forwards") in
      let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in
@@ -2725,7 +2728,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
             | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length"
           in
           annot_pat (P_tup (List.rev tpats)) typ, env, guards
-       | _ -> typ_error l "Cannot bind tuple pattern against non tuple type"
+       | _ ->
+          typ_error l (Printf.sprintf "Cannot bind tuple pattern %s against non tuple type %s"
+                         (string_of_pat pat) (string_of_typ typ))
      end
   | P_app (f, pats) when Env.is_union_constructor f env ->
      begin
@@ -2734,14 +2739,10 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
          | Typ_tup typs -> typs
          | _ -> [typ]
-       in
+       in       
        match Env.expand_synonyms env ctor_typ with
-       | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+       | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
-            let arg_typ = match arg_typ with
-              | Typ_aux (Typ_tup [arg_typ], _) -> arg_typ
-              | _ -> arg_typ
-            in
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ));
               let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
@@ -3473,10 +3474,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   in
   let quants, typ_args, typ_ret, eff =
     match Env.expand_synonyms env f_typ with
-    | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) ->
-       quant_items typq, typ_args, typ_ret, eff
-    | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
-       quant_items typq, [typ_arg], typ_ret, eff
+    | Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> quant_items typq, typ_args, typ_ret, eff
     | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
   in
   let unifiers = instantiate_simple_equations quants in
@@ -3610,12 +3608,8 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
          | _ -> [typ]
        in
        match Env.expand_synonyms env ctor_typ with
-       | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+       | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
-            let arg_typ = match arg_typ with
-              | Typ_aux (Typ_tup [arg_typ], _) -> arg_typ
-              | _ -> arg_typ
-            in
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
               let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
@@ -4185,7 +4179,7 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
 
 let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
   match typ with
-  | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
+  | Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) ->
      begin
        let env = Env.add_ret_typ typ_ret env in
        (* We want to forbid polymorphic undefined values in all cases,
@@ -4199,7 +4193,16 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
          then Env.allow_polymorphic_undefineds env
          else env
        in
-       let typed_pexp, prop_eff = propagate_pexp_effect (check_case env typ_arg (strip_pexp pexp) typ_ret) in
+       (* This is one of the cases where we are allowed to treat
+          function arguments as like a tuple, and maybe we
+          shouldn't. *)
+       let typed_pexp, prop_eff =
+         match typ_args with
+         | [typ_arg] ->
+            propagate_pexp_effect (check_case env typ_arg (strip_pexp pexp) typ_ret)
+         | _ ->
+            propagate_pexp_effect (check_case env (Typ_aux (Typ_tup typ_args, l)) (strip_pexp pexp) typ_ret)
+       in
        FCL_aux (FCL_Funcl (id, typed_pexp), (l, Some ((env, typ, prop_eff), Some typ)))
      end
   | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
@@ -4251,7 +4254,6 @@ let mapcl_effect (MCL_aux (_, (l, annot))) =
   | Some ((_, _, eff), _) -> eff
   | None -> no_effect (* Maybe could be assert false. This should never happen *)
 
-
 let infer_funtyp l env tannotopt funcls =
   match tannotopt with
   | Typ_annot_opt_aux (Typ_annot_opt_some (quant, ret_typ), _) ->
@@ -4266,8 +4268,15 @@ let infer_funtyp l env tannotopt funcls =
        match funcls with
        | [FCL_aux (FCL_Funcl (_, Pat_aux (pexp,_)), _)] ->
           let pat = match pexp with Pat_exp (pat,_) | Pat_when (pat,_,_) -> pat in
-          let arg_typ = typ_from_pat pat in
-          let fn_typ = mk_typ (Typ_fn (arg_typ, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          (* The function syntax lets us bind multiple function
+             arguments with a single pattern, hence why we need to do
+             this. But perhaps we don't want to allow this? *)
+          let arg_typs =
+            match typ_from_pat pat with
+            | Typ_aux (Typ_tup arg_typs, _) -> arg_typs
+            | arg_typ -> [arg_typ]
+          in
+          let fn_typ = mk_typ (Typ_fn (arg_typs, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
           (quant, fn_typ)
        | _ -> typ_error l "Cannot infer function type for function with multiple clauses"
      end
@@ -4308,8 +4317,8 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
        let (quant, typ) = infer_funtyp l env tannotopt funcls in
        false, (quant, typ), env
   in
-  let vtyp_arg, vtyp_ret, declared_eff, vl = match typ with
-    | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) -> vtyp_arg, vtyp_ret, declared_eff, vl
+  let vtyp_args, vtyp_ret, declared_eff, vl = match typ with
+    | Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) -> vtyp_args, vtyp_ret, declared_eff, vl
     | _ -> typ_error l "Function val spec was not a function type"
   in
   check_tannotopt env quant vtyp_ret tannotopt;
@@ -4320,7 +4329,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
   let vs_def, env, declared_eff =
     if not have_val_spec
     then
-      let typ = Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, eff), vl) in
+      let typ = Typ_aux (Typ_fn (vtyp_args, vtyp_ret, eff), vl) in
       [mk_val_spec env quant typ id], Env.add_val_spec id (quant, typ) env, eff
     else [], env, declared_eff
   in
@@ -4429,15 +4438,8 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
-  | Tu_ty_id (typ, v) ->
-     (* If a constructor type is a tuple we need to wrap it again in a
-        dummy tuple constructor so that it actually gets treated as a
-        tuple and not a multiple argument function! *)
-     let tuple = match typ with
-       | Typ_aux (Typ_tup _, _) -> mk_typ (Typ_tup [typ])
-       | _ -> typ
-     in
-     let typ' = mk_typ (Typ_fn (tuple, ret_typ, no_effect)) in
+  | Tu_ty_id (arg_typ, v) ->
+     let typ' = mk_typ (Typ_fn ([arg_typ], ret_typ, no_effect)) in
      env
      |> Env.add_union_id v (typq, typ')
      |> Env.add_val_spec v (typq, typ')
@@ -4564,11 +4566,11 @@ let initial_env =
   |> Env.add_val_spec (mk_id "size_itself_int")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
-       function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
+       function_typ [app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]]
          (atom_typ (nvar (mk_kid "n"))) no_effect)
   |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
   |> Env.add_val_spec (mk_id "make_the_value")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
-       function_typ (atom_typ (nvar (mk_kid "n")))
+       function_typ [atom_typ (nvar (mk_kid "n"))]
          (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect)