From cb683e778a1c876147b8610d7271252412232e52 Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Thu, 9 Mar 2023 16:07:33 +0530 Subject: [PATCH 1/2] when checking equatable check for the leftmost head --- src/typechecker/FStar.TypeChecker.Core.fst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index c2a1244795d..1cc5700d309 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -514,8 +514,7 @@ let no_guard (g:result 'a) | err -> err let equatable g t = - let head, _ = U.head_and_args t in - Rel.may_relate_with_logical_guard g.tcenv true head + t |> U.leftmost_head |> Rel.may_relate_with_logical_guard g.tcenv true let apply_predicate x p = fun e -> Subst.subst [NT(x.binder_bv, e)] p From afaaa116702358a46953622421a21bbf138a5054 Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Thu, 9 Mar 2023 16:07:37 +0530 Subject: [PATCH 2/2] snap --- ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index 9c42bb28c8a..58d06f74759 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -1005,11 +1005,11 @@ let no_guard : 'a . 'a result -> 'a result = let (equatable : env -> FStar_Syntax_Syntax.term -> Prims.bool) = fun g -> fun t -> - let uu___ = FStar_Syntax_Util.head_and_args t in - match uu___ with - | (head, uu___1) -> - FStar_TypeChecker_Rel.may_relate_with_logical_guard g.tcenv true - head + let uu___ = + FStar_Compiler_Effect.op_Bar_Greater t + FStar_Syntax_Util.leftmost_head in + FStar_Compiler_Effect.op_Bar_Greater uu___ + (FStar_TypeChecker_Rel.may_relate_with_logical_guard g.tcenv true) let (apply_predicate : FStar_Syntax_Syntax.binder -> FStar_Syntax_Syntax.term ->