Disable cross-effect subtyping of arrows

src/typechecker/FStarC.TypeChecker.Rel.fst

@@ -2150,6 +2150,44 @@ let has_typeclass_constraint (u:ctx_uvar) (wl:worklist)
   : bool
   = wl.typeclass_variables |> for_any (fun v -> UF.equiv v.ctx_uvar_head u.ctx_uvar_head)
 
+let maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term =
+  let norm = N.normalize [Env.Primops; Env.HNF; Env.Beta; Env.Eager_unfolding; Env.Unascribe; Env.Unrefine] env in
+  let t_e = norm t_e in
+  let t_expected = norm t_expected in
+  if !dbg_Rel then BU.print2 "t_e=%s   t_exp=%s\n" (show t_e) (show t_expected);
+  let rec aux e t_e t_expected =
+    match (SS.compress t_e).n, (SS.compress t_expected).n with
+    | Tm_arrow {bs=bs_e; comp=c_e}, Tm_arrow {bs=bs_exp; comp=c_exp} ->
+      let mk_c c = function
+        | [] -> c
+        | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in
+      let (bs_e, c_e), (bs_exp, c_exp) =
+        match_num_binders (bs_e, mk_c c_e) (bs_exp, mk_c c_exp) in
+      let bs_e, c_e = SS.open_comp bs_e c_e in
+      let bs_exp, c_exp = SS.open_comp bs_exp c_exp in
+      let bs_exp, as_exp = U.args_of_binders bs_exp in
+      let e' = U.mk_app e as_exp in
+      let return e' = Some (U.abs bs_exp e' (Some (U.residual_comp_of_comp c_exp))) in
+      begin match aux e' (U.comp_result c_e) (U.comp_result c_exp) with
+      | Some e' -> return e'
+      | None ->
+        let eff_e, eff_exp =
+          c_e |> U.comp_effect_name |> Env.norm_eff_name env,
+          c_exp |> U.comp_effect_name |> Env.norm_eff_name env in
+        if lid_equals eff_e eff_exp then
+          None
+        else
+          return e'
+      end
+    | _, _ -> None
+  in
+  aux e t_e t_expected
+
+let eta_expand_fun env (e t_e t_expected: term) : term =
+  match maybe_eta_expand_fun env e t_e t_expected with
+  | None -> e
+  | Some e -> e
+
 (* This function returns true for those lazykinds that
 are "complete" in the sense that unfolding them does not
 lose any information. For instance, embedded universes
@@ -2915,7 +2953,6 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term)
     *)
     let mk_solution env (lhs:flex_t) (bs:binders) (rhs:term) =
         let bs_orig = bs in
-        let rhs_orig = rhs in
         let (Flex (_, ctx_u, args)) = lhs in
         let bs, rhs =
           let bv_not_free_in_arg x arg =
@@ -2959,6 +2996,18 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term)
           bs,
           S.mk_Tm_app rhs_hd rhs_args rhs.pos
         in
+        let rhs =
+          // eta-expand functions for effect promotion, unless we're in --MLish
+          if Options.ml_ish () then rhs else
+          let env = { env with admit=true; expected_typ=None } in
+          let t_u, _ =
+            let Flex (lhs, _, _) = lhs in
+            let lhs_hd, _ = U.head_and_args lhs in
+            env.typeof_well_typed_tot_or_gtot_term env (U.mk_app lhs_hd (U.args_of_non_null_binders bs)) false in
+          let t_rhs, _ = env.typeof_well_typed_tot_or_gtot_term env rhs false in
+          if !dbg_Rel then BU.print2 "t_rhs=%s   t_u=%s\n" (show t_rhs) (show t_u);
+          eta_expand_fun env rhs t_rhs t_u in
+        if !dbg_Rel then BU.print1 "rhs_eta=%s\n" (show rhs);
         let sol =
           match bs with
           | [] -> rhs
@@ -4033,8 +4082,16 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
         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  ->
+        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
+          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

src/typechecker/FStarC.TypeChecker.Rel.fsti

@@ -52,6 +52,9 @@ val head_matches_delta (env:env) (logical:bool) (smt_ok:bool) (t1 t2:typ) : (mat
 val may_relate_with_logical_guard (env:env) (is_equality:bool) (head:typ) : bool
 val guard_to_string           : env -> guard_t -> string
 val simplify_guard            : env -> guard_t -> guard_t
+
+val maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term
+
 val solve_deferred_constraints: env -> guard_t -> guard_t
 val solve_non_tactic_deferred_constraints: maybe_defer_flex_flex:bool -> env -> guard_t -> guard_t
 

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -2051,7 +2051,7 @@ and tc_abs_expected_function_typ env (bs:binders) (t0:option (typ & bool)) (body
       (* CK: add this case since the type may be f:(a -> M b wp){φ}, in which case I drop the refinement *)
       (* NS: 07/21 dropping the refinement is not sound; we need to check that f validates phi. See Bug #284 *)
       | Tm_refine {b} ->
-        let _, bs, bs', copt, env_body, body, g_env = as_function_typ norm b.sort in
+        let _, bs, bs', copt, env_body, body, g_env = as_function_typ false b.sort in
         //we pass type `t` out to check afterwards the full refinement type is respected
         Some t, bs, bs', copt, env_body, body, g_env
 
@@ -2284,8 +2284,8 @@ and tc_abs env (top:term) (bs:binders) (body:term) : term & lcomp & guard_t =
       tc_abs_expected_function_typ env bs topt body in
 
     if Debug.extreme () then
-      BU.print3 "After expected_function_typ, tfun_opt: %s, c_opt: %s, and expected type in envbody: %s\n"
-           (show tfun_opt) (show c_opt) (show (Env.expected_typ envbody));
+      BU.print4 "After expected_function_typ, tfun_opt: %s, bs: %s, c_opt: %s, and expected type in envbody: %s\n"
+           (show tfun_opt) (show bs) (show c_opt) (show (Env.expected_typ envbody));
 
     if !dbg_NYC
     then BU.print2 "!!!!!!!!!!!!!!!Guard for function with binders %s is %s\n"

src/typechecker/FStarC.TypeChecker.Util.fst

@@ -2572,6 +2572,16 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_
               BU.print1 "(%s) No user coercion found\n"
                       (Range.string_of_range e.pos)
       in
+
+      // eta-expand functions for effect promotion, unless we're in --MLish
+      match if Options.ml_ish () then None else maybe_eta_expand_fun env e lc.res_typ exp_t with
+      | Some e' ->
+        if !dbg_Coercions then
+          BU.print3 "(%s) Eta-expansion coercion from %s to %s" (Range.string_of_range e.pos) (show e) (show e');
+        // FIXME: do we need to type-check this again?
+        e', { lc with res_typ = exp_t }, Env.trivial_guard
+
+      | None ->
 
       (* TODO: hide/reveal also user coercions? it's trickier for sure *)
 

ulib/FStar.All.fsti

@@ -28,7 +28,7 @@ unfold let lift_state_all (a : Type) (wp : st_wp a) (p : all_post a) = wp (fun a
 sub_effect STATE ~> ALL { lift_wp = lift_state_all }
 
 unfold
-let lift_exn_all (a : Type) (wp : ex_wp a) (p : all_post a) (h : heap) = wp (fun ra -> p ra h)
+let lift_exn_all (a : Type) (wp : ex_wp a) : all_wp_h heap a = fun (p : all_post a) (h : heap) -> wp (fun ra -> p ra h)
 sub_effect EXN ~> ALL { lift_wp = lift_exn_all }
 
 effect All (a:Type) (pre:all_pre) (post:(h:heap -> Tot (all_post' a (pre h)))) =

ulib/FStar.BigOps.fst

@@ -108,7 +108,7 @@ let pairwise_or'_nil (#a:Type) (f:a -> a -> Type0)
   = assert (pairwise_or' f [] == False) by (T.compute())
 
 let pairwise_or'_cons (#a:Type) (f:a -> a -> Type) (hd:a) (tl:list a)
-  = assert (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl))
+  = assert_norm (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl))
 
 let pairwise_or'_prop (#a:Type) (f:a -> a -> Type) (l:list a)
   = match l with

ulib/FStar.BigOps.fsti

@@ -85,7 +85,7 @@ val map_op'_cons
 
 (** [big_and' f l] = [/\_{x in l} f x] *)
 [@@ __reduce__]
-let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_and f l True
+let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p /\ q) (fun x -> f x) l True
 
 (** Equations for [big_and'] showing it to be trivial over the empty list *)
 val big_and'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_and' f [] == True)
@@ -125,7 +125,7 @@ let big_and #a (f: (a -> Type)) (l: list a) : prop =
 
 (** [big_or f l] = [\/_{x in l} f x] *)
 [@@ __reduce__]
-let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_or f l False
+let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p \/ q) (fun x -> f x) l False
 
 (** Equations for [big_or] showing it to be [False] on the empty list *)
 val big_or'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_or' f [] == False)
@@ -174,7 +174,7 @@ let big_or #a (f: (a -> Type)) (l: list a) : prop =
 (** Mapping pairs of elements of [l] using [f] and combining them with
     [op]. *)
 [@@ __reduce__]
-let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> b)) (l: list a) (z: b) : GTot b =
+let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> GTot b)) (l: list a) (z: b) : GTot b =
   match l with
   | [] -> z
   | hd :: tl -> (map_op' op (f hd) tl z) `op` (pairwise_op' op f tl z)
@@ -195,7 +195,7 @@ let anti_reflexive (#a: Type) (f: (a -> a -> Type)) = forall x. ~(f x x)
 
       {[ pairwise_and f [a; b; c] = f a b /\ f a c /\ f b c ]} *)
 [@@ __reduce__]
-let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_and f l True
+let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p /\ q) (fun x y -> f x y) l True
 
 (** Equations for [pairwise_and] showing it to be a fold with [big_and] *)
 val pairwise_and'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_and' f [] == True)
@@ -235,7 +235,7 @@ let pairwise_and #a (f: (a -> a -> Type)) (l: list a) : prop =
 (** [pairwise_or f l] disjoins [f] on all pairs excluding the diagonal
     i.e., [pairwise_or f [a; b; c] = f a b \/ f a c \/ f b c] *)
 [@@ __reduce__]
-let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_or f l False
+let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p \/ q) (fun x y -> f x y) l False
 
 (** Equations for [pairwise_or'] showing it to be a fold with [big_or'] *)
 val pairwise_or'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_or' f [] == False)

ulib/FStar.Cardinality.Cantor.fst

@@ -2,7 +2,7 @@ module FStar.Cardinality.Cantor
 
 open FStar.Functions
 
-let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
+let no_surj_powerset (a : Type) (f : a -> GTot (powerset a)) : Lemma (~(is_surj f)) =
   let aux () : Lemma (requires is_surj f) (ensures False) =
     (* Cantor's proof: given a supposed surjective f,
     we define a set s that cannot be in the image of f. Namely,
@@ -16,9 +16,9 @@ let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
   in
   Classical.move_requires aux ()
 
-let no_inj_powerset (a : Type) (f : powerset a -> a) : Lemma (~(is_inj f)) =
+let no_inj_powerset (a : Type) (f : powerset a -> GTot a) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
-    let g : a -> GTot (powerset a) = inverse_of_inj f (fun _ -> false) in
+    let g : a -> GTot (powerset a) = inverse_of_inj (fun x -> f x) (fun _ -> false) in
     no_surj_powerset a g
   in
   Classical.move_requires aux ()

ulib/FStar.Cardinality.Cantor.fsti

@@ -6,8 +6,8 @@ set. *)
 
 open FStar.Functions
 
-val no_surj_powerset (a : Type) (f : a -> powerset a)
+val no_surj_powerset (a : Type) (f : a -> GTot (powerset a))
   : Lemma (~(is_surj f))
 
-val no_inj_powerset (a : Type) (f : powerset a -> a)
+val no_inj_powerset (a : Type) (f : powerset a -> GTot a)
   : Lemma (~(is_inj f))

ulib/FStar.Cardinality.Universes.fst

@@ -19,7 +19,7 @@ let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
   assert (xx1 === xx2);
   assert (f1 == f2)
 
-let inj_type_powerset () : Lemma (is_inj type_powerset) =
+let inj_type_powerset () : Lemma (is_inj_tot type_powerset) =
   Classical.forall_intro_2 (fun f1 -> Classical.move_requires (aux_inj_type_powerset f1))
 
 (* let u' > u be universes. (u' = max(a+1, b), u=a below)
@@ -29,14 +29,13 @@ let inj_type_powerset () : Lemma (is_inj type_powerset) =
    3- Therefore, there cannot be an injection from Type(u') into Type(u), otherwise we would
       compose it with the first injection and obtain the second impossible injection.
 *)
-let no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a) : Lemma (~(is_inj f)) =
+let no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a)) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
-    let comp : powerset (Type u#a) -> Type u#a = fun x -> f (type_powerset x) in
+    let comp : powerset (Type u#a) -> GTot (Type u#a) = fun x -> f (to_gtot type_powerset x) in
     inj_type_powerset ();
-    inj_comp type_powerset f;
     no_inj_powerset _ comp
   in
   Classical.move_requires aux ()
 
-let no_inj_universes_suc (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) =
+let no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a)) : Lemma (~(is_inj f)) =
   no_inj_universes f

ulib/FStar.Cardinality.Universes.fsti

@@ -6,9 +6,9 @@ open FStar.Cardinality.Cantor
 (* Prove that there can be no injection from a universe into a strictly smaller
 universe. We use `max (a+1) b` to represent an arbitrary universe strictly larger
 than `a` as we cannot write sums of universe levels. *)
-val no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a)
+val no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a))
   : Lemma (~(is_inj f))
 
 (* A simpler version for the +1 case. *)
-val no_inj_universes_suc (f : Type u#(a+1) -> Type u#a)
+val no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a))
   : Lemma (~(is_inj f))

ulib/FStar.Classical.fst

@@ -40,7 +40,7 @@ let get_equality #t a b = get_squashed #(equals a b) (a == b)
 let impl_to_arrow #a #b impl sx =
   bind_squash #(a -> GTot b) impl (fun f -> bind_squash sx (fun x -> return_squash (f x)))
 
-let arrow_to_impl #a #b f = squash_double_arrow (return_squash (fun x -> f (return_squash x)))
+let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squash b)) (fun x -> f (return_squash x)))
 
 let impl_intro_gtot #p #q f = return_squash f
 

ulib/FStar.Fin.fst

@@ -141,9 +141,9 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
       let index_of_first_pigeon = find_eq eq holes first_pigeon in //we carefully carve first_pigeon from (holes)
       let holes_except_first_pigeon = S.append (S.slice holes 0 (index_of_first_pigeon)) 
                                              (S.slice holes (index_of_first_pigeon+1) (S.length holes)) in 
-      let all_but_first_pigeon_remain_in_reduced (x: items_of eq holes { not (eq x first_pigeon) }) 
-        : Lemma (contains_eq eq holes_except_first_pigeon x) 
-        = let index_of_x_in_holes = find_eq eq holes x in 
+      introduce forall (x: items_of eq holes { not (eq x first_pigeon) }). contains_eq eq holes_except_first_pigeon x with
+        // all but first pigeon remain in reduced
+        (let index_of_x_in_holes = find_eq eq holes x in 
           reveal_opaque (`%contains_eq) (contains_eq eq);  
           if index_of_x_in_holes < index_of_first_pigeon 
           then assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon index_of_x_in_holes)
@@ -152,8 +152,7 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
             Classical.move_requires (trans_lemma eq x (S.index holes index_of_x_in_holes)) first_pigeon; 
             // append/slice smtpat hint
             assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon (index_of_x_in_holes-1))
-          end 
-      in Classical.forall_intro all_but_first_pigeon_remain_in_reduced; 
+          end);
       let i1, i2 = pigeonhole_eq (eq) (holes_except_first_pigeon)  
                                       (S.init #(items_of eq holes_except_first_pigeon)
                                               (S.length pigeons - 1) 

ulib/FStar.Functions.fsti

@@ -6,12 +6,23 @@ about functions and sets. *)
 let is_inj (#a #b : _) (f : a -> GTot b) : prop =
   forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2
 
+let to_gtot #a #b (f: a -> b) : (a -> GTot b) = fun x -> f x
+
+let is_inj_tot #a #b (f: a -> b) : prop =
+  is_inj (to_gtot f)
+
 let is_surj (#a #b : _) (f : a -> GTot b) : prop =
   forall (y:b). exists (x:a). f x == y
 
+let is_surj_tot #a #b (f: a -> b) : prop =
+  is_surj (to_gtot f)
+
 let is_bij (#a #b : _) (f : a -> GTot b) : prop =
   is_inj f /\ is_surj f
 
+let is_bij_tot #a #b (f: a -> b) : prop =
+  is_bij (to_gtot f)
+
 let in_image (#a #b : _) (f : a -> GTot b) (y : b) : prop =
   exists (x:a). f x == y
 

ulib/FStar.HyperStack.All.fst

@@ -25,7 +25,7 @@ new_effect ALL = ALL_h HyperStack.mem
 unfold let lift_state_all (a:Type) (wp:st_wp a) (p:all_post a) =  wp (fun a -> p (V a))
 sub_effect STATE ~> ALL = lift_state_all
 
-unfold let lift_exn_all (a:Type) (wp:ex_wp a)   (p:all_post a) (h:HyperStack.mem) = wp (fun ra -> p ra h)
+unfold let lift_exn_all (a:Type) (wp:ex_wp a) : all_wp_h HyperStack.mem a = fun p h -> wp (fun ra -> p ra h)
 sub_effect EXN   ~> ALL = lift_exn_all
 
 effect All (a:Type) (pre:all_pre) (post: (h0:HyperStack.mem -> Tot (all_post' a (pre h0)))) =

ulib/FStar.HyperStack.ST.fsti

@@ -47,7 +47,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' mem a pre
 let gst_post (a:Type) = st_post_h mem a
 let gst_wp (a:Type)   = st_wp_h mem a
 
-unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:mem) = wp (fun a -> p a h)
+unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h mem a = fun p h -> wp (fun a -> p a h)
 sub_effect DIV ~> GST = lift_div_gst
 
 (*
@@ -324,6 +324,7 @@ val pop_frame (_:unit)
 #push-options "--z3rlimit 40"
 let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem)
                 (s:mreference a rel{is_stack_region (frameOf s)}) (m1:mem)
+  : GTot prop
   = is_stack_region (get_tip m0)                          /\
     Map.domain (get_hmap m0) == Map.domain (get_hmap m1)  /\
     get_tip m0 == get_tip m1                              /\
@@ -378,7 +379,7 @@ val new_colored_region (r0:rid) (c:int)
                 (r1, m1) == HS.new_eternal_region m0 r0 (Some c)))
 
 let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem)
-                       (x:mreference a rel) (m1:mem) =
+                       (x:mreference a rel) (m1:mem) : GTot prop =
   let region_i = get_hmap m0 `Map.sel` i in
   as_ref x `Heap.unused_in` region_i /\
   i `is_in` get_hmap m0              /\
@@ -408,7 +409,7 @@ val rfree (#a:Type) (#rel:preorder a) (r:mreference a rel{HS.is_mm r /\ HS.is_he
   :ST unit (requires (fun m0     -> r `is_live_for_rw_in` m0))
            (ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0))
 
-unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) =
+unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop =
   m0 `contains` r /\ m1 == HyperStack.upd m0 r v
 
 (**
@@ -419,7 +420,7 @@ val op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a)
   :STL unit (requires (fun m -> r `is_live_for_rw_in` m /\ rel (HS.sel m r) v))
             (ensures  (assign_post r v))
 
-unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) =
+unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop =
   m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r
 
 (**

ulib/FStar.IndefiniteDescription.fst

@@ -64,4 +64,4 @@ let stronger_markovs_principle (p: (nat -> GTot bool))
     boolean predicate *)
 let stronger_markovs_principle_prop (p: (nat -> GTot prop))
     : Ghost nat (requires (~(forall (n: nat). ~(p n)))) (ensures (fun n -> p n)) =
-    indefinite_description_ghost _ p
+    indefinite_description_ghost _ (fun x -> p x)

ulib/FStar.Modifies.fst

@@ -237,7 +237,7 @@ let loc_includes_region_union_l = MG.loc_includes_region_union_l
 
 let loc_includes_addresses_addresses = MG.loc_includes_addresses_addresses #_ cls
 
-let loc_disjoint = MG.loc_disjoint
+let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2
 
 let loc_disjoint_sym = MG.loc_disjoint_sym