typechecker: unfold expected type in checking of let recs

Use N.get_n_binders () to obtain the needed amount of binders without
over flattening.

Fixes FStarLang#2895

src/typechecker/FStar.TypeChecker.Util.fst

@@ -186,35 +186,27 @@ let extract_let_rec_annotation env {lbname=lbname; lbunivs=univ_vars; lbtyp=t; l
                  (Print.term_to_string e)
                  (Print.term_to_string t);
   let env = Env.push_univ_vars env univ_vars in
-  let un_arrow t =
-    //Rather than use U.arrow_formals_comp, we use un_arrow here
-    //since the former collapses adjacent Tot annotations, e.g.,
-    //    x:t -> Tot (y:t -> M)
-    // is collapsed, breaking arities
-      match (SS.compress t).n with
-      | Tm_arrow (bs, c) ->
-        Subst.open_comp bs c
-      | _ ->
-        Errors.raise_error (Errors.Fatal_LetRecArgumentMismatch, "Recursive functions must be introduced at arrow types")
-                           rng
-  in
   let reconcile_let_rec_ascription_and_body_type tarr lbtyp_opt =
       let get_decreases c =
           U.comp_flags c |> BU.prefix_until (function DECREASES _ -> true | _ -> false)
       in
-      match lbtyp_opt with
-      | None ->
-        let bs, c = un_arrow tarr in
-        (match get_decreases c with
-         | Some (pfx, DECREASES d, sfx) ->
+      let fallback () =
+        let bs, c = U.arrow_formals_comp tarr in
+        match get_decreases c with
+        | Some (pfx, DECREASES d, sfx) ->
            let c = Env.comp_set_flags env c (pfx @ sfx) in
            U.arrow bs c, tarr, true
-         | _ -> tarr, tarr, true)
+        | _ -> tarr, tarr, true
+      in
+      match lbtyp_opt with
+      | None ->
+        fallback()
 
       | Some annot ->
-        let bs, c = un_arrow tarr in
-        let bs', c' = un_arrow annot in
-        if List.length bs <> List.length bs'
+        let bs, c = U.arrow_formals_comp tarr in
+        let n_bs = List.length bs in
+        let bs', c' = N.get_n_binders env n_bs annot in
+        if List.length bs' <> n_bs
         then Errors.raise_error (Errors.Fatal_LetRecArgumentMismatch, "Arity mismatch on let rec annotation")
                                 rng;
         let move_decreases d flags flags' =
@@ -307,8 +299,9 @@ let extract_let_rec_annotation env {lbname=lbname; lbunivs=univ_vars; lbtyp=t; l
               | Tm_ascribed (body', (Inr c, tac_opt, use_eq), lopt) ->
                 let tarr = mk_arrow c in
                 let tarr, lbtyp, recheck = reconcile_let_rec_ascription_and_body_type tarr lbtyp_opt in
-                let bs', c = un_arrow tarr in
-                if List.length bs' <> List.length bs
+                let n_bs = List.length bs in
+                let bs', c = N.get_n_binders env n_bs tarr in
+                if List.length bs' <> n_bs
                 then failwith "Impossible"
                 else let subst = U.rename_binders bs' bs in
                      let c = SS.subst_comp subst c in

tests/bug-reports/Bug2895.fst

@@ -0,0 +1,41 @@
+module Bug2895
+
+// let rec not used
+#set-options "--warn_error -328"
+
+(* Recursive functions must be literals, but the annotated type
+can be an _abbreviation_ of an arrow type, as in the examples that
+follow. See issue #2895. *)
+
+type foo (t:Type) = t -> bool
+val f : foo string
+let rec f (u : string) : bool = false
+let test = f "123"
+
+(* From the issue *)
+type comparator_for (t:Type) = t -> t -> bool
+val univ_eq : comparator_for int
+let rec univ_eq (u1 u2 : int) : bool = false
+
+(* A more involved variant, that could fail to extract due to coercions.
+*)
+
+type cmpres #t (x y : t) = bool
+type comparator_for' (t:Type) = x:t -> y:t -> cmpres x y
+
+let string_eq : comparator_for' string = fun x y -> x = y
+let bool_eq : comparator_for' bool = fun x y -> x = y
+
+type sb = | S of string | B of bool
+val sb_eq : comparator_for' sb
+
+(* The body of this function gets a coercion, as the branches
+are of seemingly different types (due to the refinement). Extraction
+must make sure to push that coercion in, or we otherwise define
+an ocaml let rec where the body is an Obj.magic call (and not
+a literal fun), which fails to compile. *)
+let rec sb_eq (sb1 sb2 : sb) : cmpres sb1 sb2 =
+  match sb1, sb2 with
+  | S s1, S s2 -> string_eq s1 s2
+  | B b1, B b2 -> bool_eq b1 b2
+  | _ -> false

tests/bug-reports/Bug2895.ml.expected

@@ -0,0 +1,29 @@
+open Prims
+type 't foo = 't -> Prims.bool
+let rec (f : Prims.string foo) = fun u -> false
+let (test : Prims.bool) = f "123"
+type 't comparator_for = 't -> 't -> Prims.bool
+let rec (univ_eq : Prims.int comparator_for) = fun u1 -> fun u2 -> false
+type ('t, 'x, 'y) cmpres = Prims.bool
+type 't comparator_for' = 't -> 't -> ('t, unit, unit) cmpres
+let (string_eq : Prims.string comparator_for') = fun x -> fun y -> x = y
+let (bool_eq : Prims.bool comparator_for') = fun x -> fun y -> x = y
+type sb =
+  | S of Prims.string 
+  | B of Prims.bool 
+let (uu___is_S : sb -> Prims.bool) =
+  fun projectee -> match projectee with | S _0 -> true | uu___ -> false
+let (__proj__S__item___0 : sb -> Prims.string) =
+  fun projectee -> match projectee with | S _0 -> _0
+let (uu___is_B : sb -> Prims.bool) =
+  fun projectee -> match projectee with | B _0 -> true | uu___ -> false
+let (__proj__B__item___0 : sb -> Prims.bool) =
+  fun projectee -> match projectee with | B _0 -> _0
+let rec (sb_eq : sb comparator_for') =
+  Obj.magic
+    (fun sb1 ->
+       fun sb2 ->
+         match (sb1, sb2) with
+         | (S s1, S s2) -> Obj.repr (string_eq s1 s2)
+         | (B b1, B b2) -> Obj.repr (bool_eq b1 b2)
+         | uu___ -> Obj.repr false)

tests/bug-reports/Makefile

@@ -50,7 +50,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2635.fst Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst \
   Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\
   Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
-  Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst
+  Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst
@@ -112,7 +112,7 @@ SHOULD_NOT_VERIFY_NOT_WORKING=Bug186.fst Bug397b.fst
 SHOULD_EXTRACT_CLOSED=Bug086.fst Bug314.fst Bug540.fst Bug541.fst Bug589.fst \
 	ExtractionBug2.fst Bug1101.fst Bug1485.fst Bug734.fst Bug310.fst \
 	Bug2058.fst RemoveUnusedTypars.B.fst RemoveUnusedTyparsIFace.B.fst \
-	PushPopProjectors.fst Bug2412.fst Bug2595.fst Bug2699.fst
+	PushPopProjectors.fst Bug2412.fst Bug2595.fst Bug2699.fst Bug2895.fst
 #ExtractionBug03.fst
 
 # Bug1479.fst Crashes when in CI with "Error: Unbound module FStar_Tactics_Effect"
@@ -192,6 +192,12 @@ Bug2699.ml:
 Bug2699.extract: Bug2699.ml
 	diff -u --strip-trailing-cr Bug2699.ml Bug2699.ml.expected
 
+Bug2895.ml:
+	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --extract Bug2895 --codegen OCaml Bug2895.fst
+
+Bug2895.extract: Bug2895.ml
+	diff -u --strip-trailing-cr Bug2895.ml Bug2895.ml.expected
+
 
 RemoveUnusedTypars.B.extract: RemoveUnusedTypars.A.fst RemoveUnusedTypars.B.fst
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --cache_checked_modules RemoveUnusedTypars.A.fst
@@ -213,20 +219,22 @@ RemoveUnusedTyparsIFace.B.extract: RemoveUnusedTyparsIFace.A.fst RemoveUnusedTyp
 PushPopProjectors.extract: PushPopProjectors.fst
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out_$* --codegen FSharp $^
 
-output-accept: Bug310.ml Bug2058.ml Bug2595.ml
+output-accept: Bug310.ml Bug2058.ml Bug2595.ml Bug2699.ml Bug2895.ml
 	cp Bug310.ml Bug310.ml.expected
 	cp Bug2058.ml Bug2058.ml.expected
 	cp Bug2595.ml Bug2595.ml.expected
+	cp Bug2699.ml Bug2699.ml.expected
+	cp Bug2895.ml Bug2895.ml.expected
 
 %.extract: %.fst
-	@mkdir -p out_$*
-	@echo '[EXTRACT   $<]'
+	$(Q)mkdir -p out_$*
+	$(Q)echo '[EXTRACT   $<]'
 	$(Q)$(FSTAR) $(SIL) $(FSTAR_DEFAULT_ARGS) --odir out_$* --codegen OCaml $^
-	@echo '[OCAMLOPT  $<]'
-	@$(OCAMLOPT) out_$*/$(CAPPED).ml -o $(CAPPED).exe
-	@echo '[RUN       $(CAPPED).exe]'
-	@./$(CAPPED).exe
-	@touch $@
+	$(Q)echo '[OCAMLOPT  $<]'
+	$(Q)$(OCAMLOPT) out_$*/$(CAPPED).ml -o $(CAPPED).exe
+	$(Q)echo '[RUN       $(CAPPED).exe]'
+	$(Q)./$(CAPPED).exe
+	$(Q)touch $@
 
 extract: $(subst .fst,.extract,$(SHOULD_EXTRACT_CLOSED))