From 07e2158b6728b3689c55b30baeaee3afb97e6b5c Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 7 Jan 2025 21:42:13 -0800
Subject: [PATCH] Compare effect names after partial application.

---
 src/typechecker/FStarC.TypeChecker.Rel.fst | 20 +++++++++-----------
 ulib/FStar.Pervasives.fsti                 |  2 +-
 ulib/FStar.SquashProperties.fst            |  2 +-
 3 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst
index d7b728e71b6..9602cb7c680 100644
--- a/src/typechecker/FStarC.TypeChecker.Rel.fst
+++ b/src/typechecker/FStarC.TypeChecker.Rel.fst
@@ -4026,6 +4026,13 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
         solve_one_universe_eq orig u1 u2 wl
 
       | Tm_arrow {bs=bs1; comp=c1}, Tm_arrow {bs=bs2; comp=c2} ->
+        let mk_c c = function
+            | [] -> c
+            | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in
+
+        let (bs1, c1), (bs2, c2) =
+            match_num_binders (bs1, mk_c c1) (bs2, mk_c c2) in
+
         let eff1, eff2 =
           let env = p_env wl orig in
           c1 |> U.comp_effect_name |> Env.norm_eff_name env,
@@ -4033,18 +4040,9 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
 
         if not (Options.ml_ish () || Ident.lid_equals eff1 eff2) then
           giveup wl (Thunk.mk fun _ -> "computation type mismatch in arrow: " ^ string_of_lid eff1 ^ " vs " ^ string_of_lid eff2) orig
-
         else
-
-        let mk_c c = function
-            | [] -> c
-            | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in
-
-        let (bs1, c1), (bs2, c2) =
-            match_num_binders (bs1, mk_c c1) (bs2, mk_c c2) in
-
-        solve_binders bs1 bs2 orig wl
-        (fun wl scope subst  ->
+          solve_binders bs1 bs2 orig wl
+          (fun wl scope subst  ->
             let c1 = Subst.subst_comp subst c1 in
             let c2 = Subst.subst_comp subst c2 in //open both comps
             let rel = if (Options.use_eq_at_higher_order()) then EQ else problem.relation in
diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti
index 0c3a4f6a550..2c4c2d2072a 100644
--- a/ulib/FStar.Pervasives.fsti
+++ b/ulib/FStar.Pervasives.fsti
@@ -538,7 +538,7 @@ let ex_wp (a: Type) = ex_post a -> GTot ex_pre
 
 (** Returning a value [x] normally promotes it to the [V x] result *)
 unfold
-let ex_return (a: Type) (x: a) (p: ex_post a) : GTot Type0 = p (V x)
+let ex_return (a: Type) (x: a) : GTot (ex_wp a) = fun p -> p (V x)
 
 (** Sequential composition of exception-raising code requires case analysing
     the result of the first computation before "running" the second one *)
diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst
index fb9a54a5daf..c081a4de7a2 100644
--- a/ulib/FStar.SquashProperties.fst
+++ b/ulib/FStar.SquashProperties.fst
@@ -108,7 +108,7 @@ let l1 (a:Type) (b:Type) =
 		   let f0 (x:pow a) (y:b) : GTot bool = false in
 		   let g0 (x:pow b) (y:a) : GTot bool = false in
 		   map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> 
-				  MkC f0 g0 (fun r x -> false_elim (f r))))
+				  MkC (fun x y -> f0 x y) (fun x y -> g0 x y) (fun r x -> false_elim (f r))))
 
 (* The paradoxical set *)
 type u = p:Type -> Tot (squash (pow p))