Compare effect names after partial application.

src/typechecker/FStarC.TypeChecker.Rel.fst

@@ -4026,25 +4026,23 @@ 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,
           c2 |> U.comp_effect_name |> Env.norm_eff_name env in
 
         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

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 *)

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))