diff --git a/client/F.ml b/client/F.ml
index 88c0c8af569aababc4c421e5f25903025c4f9a13..5fc2eb884762e14677334bca2f20ed8a548a0a15 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -87,7 +87,7 @@ type ('a, 'b) term =
   | Annot of loc * ('a, 'b) term * ('a, 'b) typ
   | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
   | App of loc * ('a, 'b) term * ('a, 'b) term
-  | Let of loc * tevar * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
   | TyAbs of loc * 'b * ('a, 'b) term
   | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
   | Tuple of loc * ('a, 'b) term list
@@ -99,6 +99,8 @@ type ('a, 'b) term =
   | Refl of loc * ('a,'b) typ
   | Use of loc * ('a,'b) term * ('a,'b) term
 
+and rec_status = Recursive | Non_recursive
+
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
@@ -201,36 +203,39 @@ module TypeInTerm : DeBruijn.TRAVERSE
 
   let rec traverse lookup extend env t =
     let trav env = traverse lookup extend env in
+    let trav_ty env ty =
+      TypeInType.traverse lookup extend env ty in
     match t with
     | Var (pos, x) ->
         Var (pos, x)
     | Hole (pos, ty, ts) ->
-      let ty' = TypeInType.traverse lookup extend env ty in
+      let ty' = trav_ty env ty in
       let ts' = List.map (trav env) ts in
       Hole (pos, ty', ts')
     | Annot (pos, t, ty) ->
         let t' = trav env t
-        and ty' = TypeInType.traverse lookup extend env ty in
+        and ty' = trav_ty env ty in
         Annot (pos, t', ty')
     | Abs (pos, x, ty, t) ->
-        let ty' = TypeInType.traverse lookup extend env ty
+        let ty' = trav_ty env ty
         and t' = trav env t in
         Abs (pos, x, ty', t')
     | App (pos, t1, t2) ->
         let t1' = trav env t1
         and t2' = trav env t2 in
         App (pos, t1', t2')
-    | Let (pos, x, t1, t2) ->
+    | Let (pos, rec_, x, ty, t1, t2) ->
+        let ty' = trav_ty env ty in
         let t1' = trav env t1
         and t2' = trav env t2 in
-        Let (pos, x, t1', t2')
+        Let (pos, rec_, x, ty', t1', t2')
     | TyAbs (pos, x, t) ->
         let env, x = extend env x in
         let t' = trav env t in
         TyAbs (pos, x, t')
     | TyApp (pos, t, ty) ->
         let t' = trav env t
-        and ty' = TypeInType.traverse lookup extend env ty in
+        and ty' = trav_ty env ty in
         TyApp (pos, t', ty')
     | Tuple (pos, ts) ->
         let ts' = List.map (trav env) ts in
@@ -247,15 +252,15 @@ module TypeInTerm : DeBruijn.TRAVERSE
         and t' = trav env t in
         Variant (pos, lbl, dty', t')
     | Match (pos, ty, t, brs) ->
-        let ty' = TypeInType.traverse lookup extend env ty in
+        let ty' = trav_ty env ty in
         let t' = trav env t
         and brs' = List.map (traverse_branch lookup extend env) brs in
         Match (pos, ty', t', brs')
     | Absurd (pos, ty) ->
-        let ty' = TypeInType.traverse lookup extend env ty in
+        let ty' = trav_ty env ty in
         Absurd (pos, ty')
     | Refl (pos, ty) ->
-        let ty' = TypeInType.traverse lookup extend env ty in
+        let ty' = trav_ty env ty in
         Refl (pos, ty')
     | Use (pos, t, u) ->
         let t' = trav env t in
diff --git a/client/F.mli b/client/F.mli
index 82037273fd2cbb990b7b9ca51855b39d9fa8dd76..eed4d7f491fb3de82342b63aa29f9340ace6a512 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -88,7 +88,7 @@ type ('a, 'b) term =
   | Annot of loc * ('a, 'b) term * ('a, 'b) typ
   | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
   | App of loc * ('a, 'b) term * ('a, 'b) term
-  | Let of loc * tevar * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
   | TyAbs of loc * 'b * ('a, 'b) term
   | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
   | Tuple of loc * ('a, 'b) term list
@@ -100,6 +100,8 @@ type ('a, 'b) term =
   | Refl of loc * ('a,'b) typ
   | Use of loc * ('a,'b) term * ('a,'b) term
 
+and rec_status = Recursive | Non_recursive
+
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index c48ede5d6606d58ebcaec1235f7bcd8a5f95f3ea..7d5b92264a11b0657c55dc379353090ceb85b9a1 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -48,20 +48,26 @@ let print_type ty =
 
 let rec translate_term env (t : F.nominal_term) : P.term =
   let self = translate_term in
+  let annot env ty = (P.Flexible, [], translate_type env ty) in
   match t with
   | F.Var (_, x) ->
       P.Var x
   | F.Hole (_, ty, ts) ->
       P.Hole (Some (translate_type env ty), List.map (self env) ts)
   | F.Annot (_, t, ty) ->
-      P.Annot (self env t, (P.Flexible, [], translate_type env ty))
+      P.Annot (self env t, annot env ty)
   | F.Abs (_, x, ty, t) ->
-      let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
-      P.Abs (annot, self env t)
+      let x_annot = P.PAnnot (P.PVar x, annot env ty) in
+      P.Abs (x_annot, self env t)
   | 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)
+  | F.Let (_, rec_, x, ty, t, u) ->
+      let rec_ = match rec_ with
+      | F.Recursive -> P.Recursive
+      | F.Non_recursive -> P.Non_recursive
+      in
+      let x_annot = P.PAnnot (P.PVar x, annot env ty) in
+      P.Let (rec_, x_annot, 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 +79,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/FTypeChecker.ml b/client/FTypeChecker.ml
index 4d67c6160b059082e5644932ebc4ac25bbd88dd4..332d1c782e7df6daacaa1683caa45d9245594a09 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -384,9 +384,14 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
       let ty1, ty2 = as_arrow ~loc (typeof env t) in
       enforce_equal ~loc env (typeof env u) ty1;
       ty2
-  | Let (_, x, t, u) ->
-      let env = extend_with_tevar env x (typeof env t) in
-      typeof env u
+  | Let (loc, rec_, x, ty, t, u) ->
+      let env_with_x = extend_with_tevar env x ty in
+      let def_env = match rec_ with
+        | Non_recursive -> env
+        | Recursive -> env_with_x
+      in
+      enforce_equal ~loc def_env (typeof def_env t) ty;
+      typeof env_with_x u
   | TyAbs (_, (), t) ->
       TyForall ((), typeof (extend_with_tyvar env) t)
   | TyApp (loc, t, ty2) ->
diff --git a/client/Infer.ml b/client/Infer.ml
index 6851e1de6603cf8699a70fb7e3901b19e325dff7..50791d517aaf88c61d9276a02244c9e47c79c8c4 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
 
@@ -124,12 +125,12 @@ let constr c xs =
 let smart =
   true
 
-let flet ~loc (x, t, u) =
+let flet ~loc (x, ty, t, u) =
   match t with
   | F.Var (_, y) when smart && x = y ->
       u
   | t ->
-      F.Let (loc, x, t, u)
+      F.Let (loc, F.Non_recursive, x, ty, t, u)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -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,11 +353,20 @@ 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) ->
+      let hastype_def x t v =
+        match rec_ with
+        | ML.Non_recursive -> hastype t v
+        | ML.Recursive ->
+          (* For recursive definitions [let rec x = t], we bind the
+             variable [x] to the monomorphic expected type of [t] when
+             inferring the type of [t] itself. *)
+          def (X.Var x) v (hastype t v)
+      in
       (* Construct a ``let'' constraint. *)
-      let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
+      let+ (a, (b, ty), t', u') =
+        let1 (X.Var x) (hastype_def x t) (hastype u w) in
       (* [a] are the type variables that we must bind (via Lambda abstractions)
          while type-checking [t]. [(b, _)] is the type scheme that [x] must
          receive while type-checking [u]. Its quantifiers [b] are guaranteed to
@@ -364,8 +374,46 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
          application of a suitable coercion to [x]. We use smart constructors so
          that, if the lists [a] and [b] happen to be equal, no extra code is
          produced. *)
-      F.Let (loc, x, F.ftyabs ~loc a t',
-             flet ~loc (x, coerce ~loc a b (F.Var (loc, x)),
+      let sch tyvars =
+        List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) tyvars ty in
+      let rec_ = match rec_ with
+        | ML.Recursive -> F.Recursive
+        | ML.Non_recursive -> F.Non_recursive
+      in
+      let t'' = match rec_ with
+        | F.Non_recursive -> t'
+        | F.Recursive ->
+          (* For recursive definitions, the defined variable is used monomorphically
+             within the definition, so we must instantiate the type scheme.
+
+             Consider for example:
+               let rec loop x = loop x
+             Which gets inferred at type ([a] [b] a -> b).
+
+             We do not want to get
+
+               let rec (loop : [a] [b] a -> b) =
+                 Fun a b ->
+                   fun (x : a) -> loop x
+
+             which is ill-typed: the recursive occurrence of 'loop' in its body
+             is applied as a monomorphic function, but it is bound to the polymorphic
+             (loop : [a] [b] a -> b).
+
+             Instead we elaborate into the following:
+
+               let rec (loop : [a] [b] a -> b) =
+                 Fun a b ->
+                   let loop = loop [a] [b] in
+                   fun (x : a) -> loop x
+          *)
+          flet ~loc (x, ty,
+                     F.ftyapp ~loc (F.Var (loc, x)) (List.map (fun v -> F.TyVar v) a),
+                     t')
+      in
+      F.Let (loc, rec_, x, sch a,
+             F.ftyabs ~loc a t'',
+             flet ~loc (x, sch b, coerce ~loc a b (F.Var (loc, x)),
                         u'))
 
     | ML.Annot (loc, t, annot) ->
@@ -700,5 +748,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..90a666326a53a7a827ec8c68cb5607e2128546d7 100644
--- a/client/test/RandomML.ml
+++ b/client/test/RandomML.ml
@@ -34,8 +34,17 @@ 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;
+      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-add.midml b/client/test/suite.t/letrec-add.midml
new file mode 100644
index 0000000000000000000000000000000000000000..905d284579a5c3c4fb6923ee238b0f8502ceaa02
--- /dev/null
+++ b/client/test/suite.t/letrec-add.midml
@@ -0,0 +1,11 @@
+#use nat.midml
+
+(* toplevel recursion is currently not supported,
+   so we wrap a "let rec .. in .." *)
+let add =
+  let rec add = fun m n ->
+    match m with
+    | Zero -> n
+    | Succ m1 -> add m1 (Succ n)
+    end
+  in add
\ No newline at end of file
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..6894a99669f3b28c74eda77441b4c4b9145317cb 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,96 @@ 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: addition of natural numbers.
+
+  $ cat letrec-add.midml
+  #use nat.midml
+  
+  (* toplevel recursion is currently not supported,
+     so we wrap a "let rec .. in .." *)
+  let add =
+    let rec add = fun m n ->
+      match m with
+      | Zero -> n
+      | Succ m1 -> add m1 (Succ n)
+      end
+    in add
+
+  $ midml letrec-add.midml
+  Type inference and translation to System F...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  let rec (add : nat  -> nat  -> nat ) =
+    fun (m : nat ) (n : nat ) ->
+      match<nat > m with
+      | Zero<nat > () -> n
+      | Succ<nat > m1 -> add m1 (Succ<nat > n)
+      end
+  in add
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+A classic 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...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  FUN a0 ->
+    let rec (length : [a1] list a1 -> nat ) =
+      FUN a2 ->
+        let (length : list a2 -> nat ) = length [a2] in
+        fun (xs : list a2) ->
+          match<nat > xs with
+          | Nil<list a2> () -> Zero<nat > ()
+          | Cons<list a2> (_, rest) -> Succ<nat > (length rest)
+          end
+    in length [a0]
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+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...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  FUN a0 a1 ->
+    let rec (loop : [a2] [a3] a3 -> a2) =
+      FUN a4 a5 ->
+        let (loop : a5 -> a4) = loop [a4] [a5] in fun (x : a5) -> loop x
+    in loop [a1] [a0]
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
 
 # Rigid, flexible variables.