support for (non-polymorphic) 'let rec' in Infer.ml

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'))
 

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

client/test/suite.t/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
\ No newline at end of file

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.