From 8aa6ca5122b806b92a404ef94e742c7207e51d3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 22 Oct 2024 17:21:36 -0700 Subject: [PATCH] Tc: improve some errors --- src/typechecker/FStarC.TypeChecker.TcTerm.fst | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst index a2bbd9f07c8..28e7720dec6 100644 --- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst @@ -4195,11 +4195,14 @@ and build_let_rec_env _top_level env lbs : list letbinding & env_t & guard_t = // TODO: There's a similar error in check_let_recs, would be nice // to remove this one. if List.isEmpty formals || List.isEmpty actuals then - raise_error lbtyp Errors.Fatal_RecursiveFunctionLiteral // TODO: GM: maybe point to the one that's actually empty? - (BU.format3 "Only function literals with arrow types can be defined recursively; got (%s) %s : %s" + // TODO: GM: maybe point to the one that's actually empty? + raise_error lbtyp Errors.Fatal_RecursiveFunctionLiteral [ + text "Only function literals with arrow types can be defined recursively."; + text <| (BU.format3 "Got (%s) %s : %s" (tag_of lbdef) (show lbdef) (show lbtyp)); + ]; let nformals = List.length formals in @@ -4266,12 +4269,13 @@ and check_let_recs env lbts = let bs, t, lcomp = abs_formals lb.lbdef in //see issue #1017 match bs with - | [] -> raise_error (S.range_of_lbname lb.lbname) - Errors.Fatal_RecursiveFunctionLiteral - (BU.format2 - "Only function literals may be defined recursively; %s is defined to be %s" + | [] -> + raise_error (S.range_of_lbname lb.lbname) Errors.Fatal_RecursiveFunctionLiteral [ + text "Only function literals may be defined recursively."; + text <| (BU.format2 "%s is defined to be %s" (show lb.lbname) - (show lb.lbdef)) + (show lb.lbdef)); + ] | _ -> (); (* HACK ALERT: arity