diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index c48ede5d6606d58ebcaec1235f7bcd8a5f95f3ea..630a7862dc3f8e88fa83d3ef60628f5761bed2cf 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -61,7 +61,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
   | F.App (_, t1, t2) ->
       P.App (self env t1, self env t2)
   | F.Let (_, x, t, u) ->
-      P.Let (P.PVar x, self env t, self env u)
+      P.Let (P.Non_recursive, P.PVar x, self env t, self env u)
   | F.TyAbs (_, x, t) ->
       let alpha = new_tyvar () in
       P.TyAbs (alpha, self ((x, alpha) :: env) t)
@@ -73,7 +73,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
       P.Proj (i, self env t)
   | F.LetProd (_, xs, t, u) ->
       let pat = P.PTuple (List.map (fun x -> P.PVar x) xs) in
-      P.Let (pat , self env t, self env u)
+      P.Let (P.Non_recursive, pat, self env t, self env u)
   | F.Variant (_, lbl, (tid, tys) , t) ->
       P.Variant (
           lbl,
diff --git a/client/Infer.ml b/client/Infer.ml
index 6851e1de6603cf8699a70fb7e3901b19e325dff7..e632ca7dad96b3d20f475f223b40b386830f6e30 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -104,6 +104,7 @@ type error =
   | Cycle of F.nominal_type
   | VariableConflict of ML.tevar
   | VariableScopeEscape
+  | Unsupported of string
 
 exception Error of Utils.loc * error
 
@@ -278,7 +279,7 @@ let convert env params ty =
 let get_loc t =
   match t with
   | ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
-  | ML.App (pos, _, _) | ML.Let (pos, _, _, _) | ML.Annot (pos, _, _)
+  | ML.App (pos, _, _) | ML.Let (pos, _, _, _, _) | ML.Annot (pos, _, _)
   | ML.Tuple (pos, _) | ML.LetProd (pos, _, _, _)
   | ML.Variant (pos, _, _) | ML.Match (pos, _, _)
     -> pos
@@ -352,8 +353,13 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
       and+ t2' = hastype t2 v
       in F.App (loc, t1', t2')
 
-    (* Generalization. *)
-    | ML.Let (loc, x, t, u) ->
+      (* Generalization. *)
+    | ML.Let (loc, rec_, x, t, u) ->
+
+        begin match rec_ with
+        | ML.Non_recursive -> ()
+        | ML.Recursive -> raise (Error (loc, Unsupported "let rec"))
+        end;
 
       (* Construct a ``let'' constraint. *)
       let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
@@ -700,5 +706,9 @@ let emit_error loc (error : error) =
       Printf.printf
         "Scope error: variable %s is already bound in this pattern."
         x
+  | Unsupported (feature) ->
+      Printf.printf
+        "Type inference does not yet support %S."
+        feature
   end;
   flush stdout
diff --git a/client/Infer.mli b/client/Infer.mli
index 7cb977e760a0e4025010e4cd6a1837512ea6f006..064ace3a3c4889b3c7ba979710e9b7dd906328b9 100644
--- a/client/Infer.mli
+++ b/client/Infer.mli
@@ -4,6 +4,7 @@ type error =
   | Cycle of F.nominal_type
   | VariableConflict of ML.tevar
   | VariableScopeEscape
+  | Unsupported of string
 
 exception Error of Utils.loc * error
 
diff --git a/client/ML.ml b/client/ML.ml
index f91cf3c90a87d7d7559828df864239b0d07cf62d..54511198f83b263d99c7fdbe962033c36a5da96e 100644
--- a/client/ML.ml
+++ b/client/ML.ml
@@ -24,18 +24,20 @@ type typ =
  [@@deriving compare]
 
 type rigidity = Flexible | Rigid
-
-let compare_rigidity r1 r2 = compare r1 r2
+  [@@deriving compare]
 
 type type_annotation = rigidity * tyvar list * typ [@@deriving compare]
   (* some <flexible vars> . <ty> *)
 
+type recursive_status = Recursive | Non_recursive
+  [@@deriving compare]
+
 type term =
   | Var of loc * tevar
   | Hole of loc * term list
   | Abs of loc * tevar * term
   | App of loc * term * term
-  | Let of loc * tevar * term * term
+  | Let of loc * recursive_status * tevar * term * term
   | Annot of loc * term * type_annotation
   | Tuple of loc * term list
   | LetProd of loc * tevar list * term * term
diff --git a/client/MLLexer.mll b/client/MLLexer.mll
index 1dd9f6bbc94c7e3885d7ec5afd8ed173ee1e4878..03f711d50b9183ed58aa92dc55e6f5eeb883ceff 100644
--- a/client/MLLexer.mll
+++ b/client/MLLexer.mll
@@ -6,6 +6,7 @@
 
   let keywords = [
       "let", LET;
+      "rec", REC;
       "in", IN;
       "fun", FUN;
       "let", LET;
diff --git a/client/MLParser.mly b/client/MLParser.mly
index 13cda8c43cdcdd4062435dec1d992412a02a520d..b87017d410754f0d066b92dedc9da3ff41a4bc65 100644
--- a/client/MLParser.mly
+++ b/client/MLParser.mly
@@ -9,6 +9,7 @@
 %token FUN
 %token ARROW "->"
 %token LET IN
+%token REC "rec"
 %token EQ "="
 
 %token LPAR "("
@@ -72,7 +73,9 @@ let term_abs :=
       List.fold_right (fun x t -> Abs (Some $loc, x, t)) xs t
     }
 
-  | (x, t1, t2) = letin(tevar) ;          { Let (Some $loc, x, t1, t2) }
+  | (x, t1, t2) = letin(tevar) ;          { Let (Some $loc, Non_recursive, x, t1, t2) }
+
+  | (x, t1, t2) = letrecin(tevar) ;       { Let (Some $loc, Recursive, x, t1, t2) }
 
   | (xs, t1, t2) = letin(tuple(tevar)) ;  { LetProd (Some $loc, xs, t1, t2) }
 
@@ -228,5 +231,10 @@ let letin (X) :=
       t1 = term ; IN ;
       t2 = term_abs ;                     { (x, t1, t2) }
 
+let letrecin (X) :=
+  | LET ; REC; x = X ; EQ ;
+      t1 = term ; IN ;
+      t2 = term_abs ;                     { (x, t1, t2) }
+
 let pipe_separated_list (X) :=
   | option (PIPE) ; ~ = separated_list (PIPE, X) ; <>
diff --git a/client/MLPrinter.ml b/client/MLPrinter.ml
index 0cefd3c350cca7290ecad0b6e2735970ff99508c..cf3e3109339563c4cba65db6bab76af222d1d60a 100644
--- a/client/MLPrinter.ml
+++ b/client/MLPrinter.ml
@@ -37,15 +37,15 @@ let rec translate_term (t : ML.term) : P.term =
       P.Abs (P.PVar x, self t)
   | ML.App (_, t1, t2) ->
       P.App (self t1, self t2)
-  | ML.Let (_, x, t, u) ->
-      P.Let (P.PVar x, self t, self u)
+  | ML.Let (_, r, x, t, u) ->
+      P.Let (r, P.PVar x, self t, self u)
   | ML.Annot (_, t, tyannot) ->
       P.Annot (self t, translate_annot tyannot)
   | ML.Tuple (_, ts) ->
       P.Tuple (List.map translate_term ts)
   | ML.LetProd (_, xs, t, u) ->
       let pat = P.PTuple (List.map (fun x -> P.PVar x) xs) in
-      P.Let (pat, self t, self u)
+      P.Let (P.Non_recursive, pat, self t, self u)
   | ML.Variant (_, lbl, t) ->
       P.Variant (lbl, None, Option.map self t)
   | ML.Match (_, t, brs) ->
diff --git a/client/P.ml b/client/P.ml
index 495c6feb7504f50da1d34736c57a0d69ed0c6e69..fe1d506554f43d6490360c6fb7a389924f0e6d4a 100644
--- a/client/P.ml
+++ b/client/P.ml
@@ -15,6 +15,8 @@ and datatype = Datatype.tyconstr_id * typ list
 
 type rigidity = Flexible | Rigid
 
+type recursive_status = ML.recursive_status = Recursive | Non_recursive
+
 type type_annotation = rigidity * tyvar list * typ
   (* some <flexible vars> . <ty> *)
 
@@ -25,7 +27,7 @@ type term =
   | Hole of typ option * term list
   | Abs of pattern * term
   | App of term * term
-  | Let of pattern * term * term
+  | Let of recursive_status * pattern * term * term
   | Annot of term * type_annotation
   | TyAbs of tyvar * term
   | TyApp of term * typ
diff --git a/client/Printer.ml b/client/Printer.ml
index c05446ecc4048a4678fdb13c6caccb82a635f6ce..b74de8d04299442e592607f81750cef1f76c3e2e 100644
--- a/client/Printer.ml
+++ b/client/Printer.ml
@@ -106,8 +106,11 @@ let print_tuple print_elem elems =
           separate_map (comma ^^ break 1) print_elem elems in
     surround 2 0 lparen contents rparen
 
-let print_let_in lhs rhs body =
+let print_let_in rec_ lhs rhs body =
   string "let"
+  ^^ (match rec_ with
+      | Recursive -> space ^^ string "rec"
+      | Non_recursive -> empty)
   ^^ surround 2 1 empty lhs empty
   ^^ string "="
   ^^ surround 2 1 empty rhs empty
@@ -163,8 +166,8 @@ and print_term_abs t =
   | TyAbs _ ->
       let (xs, t) = flatten_tyabs t in
       print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
-  | Let (p, t1, t2) ->
-      print_let_in
+  | Let (rec_, p, t1, t2) ->
+      print_let_in rec_
         (print_pattern p)
         (print_term t1)
         (print_term_abs t2)
diff --git a/client/test/CheckML.ml b/client/test/CheckML.ml
index 33e9e98a763b3da1a96fb7091c8fcf00da18bd4b..039f76be994064db6a0fac77f06a8bf3f984112d 100644
--- a/client/test/CheckML.ml
+++ b/client/test/CheckML.ml
@@ -48,7 +48,7 @@ let letify xts =
     | [(_loc, _last_var, t)] ->
         t
     | (loc, x, t) :: xts ->
-        ML.Let (loc, x, t, aux xts)
+        ML.Let (loc, ML.Non_recursive, x, t, aux xts)
   in
   aux xts
 
diff --git a/client/test/RandomML.ml b/client/test/RandomML.ml
index e320cf819ae8332022966caae23286c991d1973c..c1f4f0040bae230be610997e5c7ad29e8ebf7d93 100644
--- a/client/test/RandomML.ml
+++ b/client/test/RandomML.ml
@@ -34,8 +34,19 @@ let app self k n =
 
 let let_ self k n =
   let* n1, n2 = split (n - 1) in
-  let+ x, t1, t2 = triple (bind k) (self (k, n1)) (self (k + 1, n2))
-  in ML.Let (None, x, t1, t2)
+  let* rec_ =
+    frequency [
+      3, pure ML.Non_recursive;
+      (* we disable 'let rec' generation for tnow,
+         as the type-checker does not suport it. *)
+      (* 1, pure ML.Recursive; *)
+    ] in
+  let+ x, t1, t2 =
+    let inner_k = match rec_ with
+      | ML.Non_recursive -> k
+      | ML.Recursive -> k + 1 in
+    triple (bind k) (self (inner_k, n1)) (self (k + 1, n2))
+  in ML.Let (None, rec_, x, t1, t2)
 
 let pair self k n =
   let* n1, n2 = split (n - 1) in
diff --git a/client/test/TestML.ml b/client/test/TestML.ml
index c55da53331e7229f8aff1a9a476d3e6fd23fd0c6..dca063b3912487bbb465f8b84396e872b00577dc 100644
--- a/client/test/TestML.ml
+++ b/client/test/TestML.ml
@@ -28,16 +28,20 @@ let k =
   ML.Abs (None, "x", ML.Abs (None, "y", x))
 
 let genid =
-  ML.Let (None, "x", id, x)
+  ML.Let (None, ML.Non_recursive,
+          "x", id, x)
 
 let genidid =
-  ML.Let (None, "x", id, ML.App (None, x, x))
+  ML.Let (None, ML.Non_recursive,
+          "x", id, ML.App (None, x, x))
 
 let genkidid =
-  ML.Let (None, "x", ML.App (None, k, id), ML.App (None, x, id))
+  ML.Let (None, ML.Non_recursive,
+          "x", ML.App (None, k, id), ML.App (None, x, id))
 
 let genkidid2 =
-  ML.Let (None, "x", ML.App (None, ML.App (None, k, id), id), x)
+  ML.Let (None, ML.Non_recursive,
+          "x", ML.App (None, ML.App (None, k, id), id), x)
 
 (* unused *)
 let _app_pair = (* ill-typed *)
@@ -48,8 +52,9 @@ let unit =
 
 (* "let x1 = (...[], ...[]) in ...[] x1" *)
 let regression1 =
-  ML.Let (None, "x1", ML.Tuple (None, [ ML.Hole (None, []) ;
-                                                  ML.Hole (None, []) ]),
+  ML.Let (None, ML.Non_recursive,
+          "x1", ML.Tuple (None, [ ML.Hole (None, []) ;
+                                       ML.Hole (None, []) ]),
           ML.App (None, ML.Hole (None, []), ML.Var (None, "x1")))
 
 (* "let f = fun x ->
@@ -59,11 +64,11 @@ let regression1 =
             fun x -> fun y -> f" *)
 let regression2 =
   ML.(
-    Let (None,
+    Let (None, Non_recursive,
       "f",
       Abs (None,
         "x",
-        Let (None,
+        Let (None, Non_recursive,
           "g",
           Abs (None,
             "y",
@@ -351,7 +356,8 @@ let test_abs_match_with () =
   test_ok "fun x -> match () with () -> () end" abs_match_with
 
 let test_let () =
-  test_ok "let y = fun x -> x in ()" (ML.Let(None, "y", id, unit))
+  test_ok "let y = fun x -> x in ()"
+    (ML.Let(None, ML.Non_recursive, "y", id, unit))
 
 let test_let_prod_singleton () =
   test_ok "let (y,) = (fun x -> x,) in ()"
diff --git a/client/test/TestMLRandom.ml b/client/test/TestMLRandom.ml
index 33081fb56b81ce0be96641c8089fa30f06afcb61..95e193a7edc92d28ccadf60452929aff063ef769 100644
--- a/client/test/TestMLRandom.ml
+++ b/client/test/TestMLRandom.ml
@@ -27,8 +27,8 @@ module Shrinker = struct
       ML.Abs (pos, y, subst_under [y] t x u)
     | ML.App (pos, t1, t2) ->
       ML.App (pos, subst t1 x u, subst t2 x u)
-    | ML.Let (pos, y, t1, t2) ->
-      ML.Let (pos, y, subst t1 x u, subst_under [y] t2 x u)
+    | ML.Let (pos, r, y, t1, t2) ->
+      ML.Let (pos, r, y, subst t1 x u, subst_under [y] t2 x u)
     | ML.Tuple (pos, ts) ->
       ML.Tuple (pos, List.map (fun t -> subst t x u) ts)
     | ML.Hole (pos, ts) ->
@@ -119,12 +119,12 @@ module Shrinker = struct
          in ML.App (pos, t1',t2')
        )
 
-      | ML.Let (pos, x, t, u) ->
+      | ML.Let (pos, r, x, t, u) ->
         subterms [t; remove_variable u x]
         <+> (
          let++ t' = t, shrink_term t
          and++ u' = u, shrink_term u
-         in ML.Let (pos, x, t', u')
+         in ML.Let (pos, r, x, t', u')
        )
 
       | ML.LetProd (pos, xs, t, u) ->
diff --git a/client/test/suite.t/letrec-list-length.midml b/client/test/suite.t/letrec-list-length.midml
new file mode 100644
index 0000000000000000000000000000000000000000..0ec64981e66db7ce88327464a28a20b8d466ce18
--- /dev/null
+++ b/client/test/suite.t/letrec-list-length.midml
@@ -0,0 +1,12 @@
+#use nat.midml
+#use list.midml
+
+(* toplevel recursion is currently not supported,
+   so we wrap a "let rec .. in .." *)
+let length =
+  let rec length = fun xs ->
+    match xs with
+    | Nil -> Zero
+    | Cons (_, rest) -> Succ (length rest)
+    end
+  in length
diff --git a/client/test/suite.t/letrec-loop.midml b/client/test/suite.t/letrec-loop.midml
new file mode 100644
index 0000000000000000000000000000000000000000..d9d62a8295470aa4889a9c76aed34040b0c277cd
--- /dev/null
+++ b/client/test/suite.t/letrec-loop.midml
@@ -0,0 +1,4 @@
+(* expected type: 'a 'b. 'a -> 'b *)
+let loop =
+  let rec loop = fun x -> loop x in
+  loop
diff --git a/client/test/suite.t/nat-annot.midml b/client/test/suite.t/nat-annot.midml
index be47836b8f35ed477aad74a7d05b90efad201735..a041cd69e60b42e2ddd2e636620bdaf96b1acd57 100644
--- a/client/test/suite.t/nat-annot.midml
+++ b/client/test/suite.t/nat-annot.midml
@@ -1,2 +1,2 @@
-type nat = | Zero | Succ of nat
+#use nat.midml
 let f = (fun x -> x : nat -> nat)
\ No newline at end of file
diff --git a/client/test/suite.t/nat.midml b/client/test/suite.t/nat.midml
new file mode 100644
index 0000000000000000000000000000000000000000..735149569f83bee8dd4ab09549612f7d1f73bc54
--- /dev/null
+++ b/client/test/suite.t/nat.midml
@@ -0,0 +1 @@
+type nat = | Zero | Succ of nat
diff --git a/client/test/suite.t/run.t b/client/test/suite.t/run.t
index 8b8ef784ba692980371fdcb6c6a0730f9bf5616d..653f6586ad3c78bd75ccf19e4418009deb8a5e5f 100644
--- a/client/test/suite.t/run.t
+++ b/client/test/suite.t/run.t
@@ -253,7 +253,7 @@ Variable scope escape
 # Annotations
 
   $ cat nat-annot.midml
-  type nat = | Zero | Succ of nat
+  #use nat.midml
   let f = (fun x -> x : nat -> nat)
 
   $ midml nat-annot.midml
@@ -302,7 +302,48 @@ Variable scope escape
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
+# Recursion
 
+For now there is only support in the parser, so the examples below
+parse correctly but fail to type-check.
+
+Mutual recursion is not yet supported.
+
+Polymorphic recursion is not yet supported.
+
+A simple let-rec function: List.length
+
+  $ cat letrec-list-length.midml
+  #use nat.midml
+  #use list.midml
+  
+  (* toplevel recursion is currently not supported,
+     so we wrap a "let rec .. in .." *)
+  let length =
+    let rec length = fun xs ->
+      match xs with
+      | Nil -> Zero
+      | Cons (_, rest) -> Succ (length rest)
+      end
+    in length
+
+  $ midml letrec-list-length.midml
+  Type inference and translation to System F...
+  File "test", line 7, characters 2-127:
+  Type inference does not yet support "let rec".
+
+Using recursion to define (loop : 'a -> 'b)
+
+  $ cat letrec-loop.midml
+  (* expected type: 'a 'b. 'a -> 'b *)
+  let loop =
+    let rec loop = fun x -> loop x in
+    loop
+
+  $ midml letrec-loop.midml
+  Type inference and translation to System F...
+  File "test", line 3, characters 2-42:
+  Type inference does not yet support "let rec".
 
 # Rigid, flexible variables.