Merge pull request #3683 from mtzguido/dbg_nit

Core: debug nits
FStarLang · Jan 17, 2025 · bdc586e · bdc586e
2 parents 7cd7efc + 6bffb26
commit bdc586e
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/syntax/print/FStarC.Syntax.Print.fst b/src/syntax/print/FStarC.Syntax.Print.fst
@@ -351,6 +351,7 @@ instance showable_ctx_uvar_meta = {
           | Ctx_uvar_meta_attr attr -> "Ctx_uvar_meta_attr " ^ show attr
           | Ctx_uvar_meta_tac r -> "Ctx_uvar_meta_tac " ^ show r);
 }
+instance showable_bqual   = { show = (fun b -> bqual_to_string (Some b)); } // really silly but OK
 instance showable_aqual   = { show = aqual_to_string; }
 
 let tscheme_to_string ts =

diff --git a/src/syntax/print/FStarC.Syntax.Print.fsti b/src/syntax/print/FStarC.Syntax.Print.fsti
@@ -38,6 +38,7 @@ instance val showable_ctxu      : showable ctx_uvar
 instance val showable_binding   : showable binding
 instance val showable_subst_elt : showable subst_elt
 instance val showable_branch    : showable branch
+instance val showable_bqual     : showable binder_qualifier
 instance val showable_aqual     : showable aqual
 instance val showable_qualifier : showable qualifier
 instance val showable_pat       : showable pat

diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst
@@ -431,12 +431,10 @@ let check_bqual (b0 b1:bqual)
       return ()
     | Some Equality, Some Equality ->
       return ()
-    | Some (Meta t1), Some (Meta t2) ->
-      if equal_term t1 t2
-      then return ()
-      else fail "Binder qualifier mismatch"
+    | Some (Meta t1), Some (Meta t2) when equal_term t1 t2 ->
+      return ()
     | _ ->
-      fail "Binder qualifier mismatch"
+      fail (BU.format2 "Binder qualifier mismatch, %s vs %s" (show b0) (show b1))
 
 let check_aqual (a0 a1:aqual)
   : result unit