From ba63ad9b3bc4991a42a05b21dcc78534c273aa35 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Wed, 4 Jan 2023 17:01:35 -0500 Subject: [PATCH] Make subst restore the level even on error --- typing/ctype.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index 306980c802..77c5c721cc 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -152,7 +152,8 @@ let global_level = s_ref 1 let saved_level = s_ref [] type levels = - { current_level: int; nongen_level: int; global_level: int; + { current_level: int; nongen_level: int; + global_level: int; (* level assigned to a fresh 'a in user code *) saved_level: (int * int) list; } let save_levels () = { current_level = !current_level; @@ -1592,7 +1593,7 @@ let subst env level priv abbrev oty params args body = current_level := old_level; umode := old_umode; body' - with Unify _ -> + with Unify _ | Cannot_subst | Escape _ -> current_level := old_level; umode := old_umode; undo_abbrev ();