diff --git a/client/Infer.ml b/client/Infer.ml
index 0e57b3d314cbeb14e7619eae9f29155f75d08de1..50791d517aaf88c61d9276a02244c9e47c79c8c4 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -355,14 +355,18 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(* Generalization. *)
| ML.Let (loc, rec_, x, t, u) ->
-
- begin match rec_ with
- | ML.Non_recursive -> ()
- | ML.Recursive -> raise (Error (loc, Unsupported "let rec"))
- end;
-
+ 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, ty), 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
@@ -372,7 +376,43 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
produced. *)
let sch tyvars =
List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) tyvars ty in
- F.Let (loc, F.Non_recursive, x, sch a, F.ftyabs ~loc a t',
+ 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'))
diff --git a/client/test/RandomML.ml b/client/test/RandomML.ml
index c1f4f0040bae230be610997e5c7ad29e8ebf7d93..90a666326a53a7a827ec8c68cb5607e2128546d7 100644
--- a/client/test/RandomML.ml
+++ b/client/test/RandomML.ml
@@ -37,9 +37,7 @@ let let_ self k n =
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; *)
+ 1, pure ML.Recursive;
] in
let+ x, t1, t2 =
let inner_k = match rec_ with
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/run.t b/client/test/suite.t/run.t
index 653f6586ad3c78bd75ccf19e4418009deb8a5e5f..6894a99669f3b28c74eda77441b4c4b9145317cb 100644
--- a/client/test/suite.t/run.t
+++ b/client/test/suite.t/run.t
@@ -311,7 +311,36 @@ Mutual recursion is not yet supported.
Polymorphic recursion is not yet supported.
-A simple let-rec function: List.length
+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
@@ -329,8 +358,20 @@ A simple let-rec function: List.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".
+ 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)
@@ -342,8 +383,15 @@ Using recursion to define (loop : 'a -> 'b)
$ 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".
+ 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.