Disable cross-effect subtyping of arrows

doc/book/code/Pure.fst

@@ -15,7 +15,7 @@ let fact (x:nat) : pos = factorial x
 
 //SNIPPET_START: wp$
 let pre = Type0
-let post (a:Type) = a -> Type0
+let post (a:Type) = a -> GTot Type0
 let wp (a:Type) = post a -> pre
 //SNIPPET_END: wp$
 

doc/old/tutorial/code/exercises/Ex04e.fst

@@ -20,6 +20,7 @@ type option 'a =
    | None : option 'a
    | Some : v:'a -> option 'a
 
+val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
 let rec find f l = match l with
   | [] -> None
   | hd::tl -> if f hd then Some hd else find f tl

examples/algorithms/GC.fst

@@ -83,7 +83,7 @@ type mutator_inv gc_state =
   inv gc_state (fun i -> gc_state.color i = Unalloc \/ gc_state.color i = White)
 
 new_effect GC_STATE = STATE_h gc_state
-let gc_post (a:Type) = a -> gc_state -> Type0
+let gc_post (a:Type) = a -> gc_state -> GTot Type0
 sub_effect
   DIV   ~> GC_STATE = fun (a:Type) (wp:pure_wp a) (p:gc_post a) (gc:gc_state) -> wp (fun a -> p a gc)
 

examples/algorithms/IntervalIntersect.fst

@@ -589,7 +589,7 @@ let rec ppIntervals' (is:intervals): ML unit =
 
 let toI f t = I (int_to_t f) (int_to_t t)
 
-let ppIntervals is : ML string = FStar.List.Tot.fold_left (sprintf "%s %s") "" (FStar.List.map ppInterval is)
+let ppIntervals is : ML string = FStar.List.Tot.fold_left (sprintf "%s %s") "" (FStar.List.map (fun i -> ppInterval i) is)
 let main =
   print_string
     (ppIntervals (intersect [toI 3 10; toI 10 15] [toI 1 4; toI 10 14]));

examples/doublylinkedlist/DoublyLinkedList.fst

@@ -1101,8 +1101,8 @@ let tot_dll_to_fragment_split (#t:Type) (h0:heap) (d:dll t{dll_valid h0 d})
           reveal d.nodes == reveal p1.pnodes `append` reveal p2.pnodes))) =
   let split_nodes = elift2_p split_using d.nodes (hide n2) in
   lemma_split_using d.nodes n2;
-  let l1 = elift1 fst split_nodes in
-  let l2 = elift1 snd split_nodes in
+  let l1 = hide (fst split_nodes) in
+  let l2 = hide (snd split_nodes) in
   let p1 = { phead = d.lhead ; ptail = n1 ; pnodes = l1 } in
   let p2 = { phead = n2 ; ptail = d.ltail ; pnodes = l2 } in
   let f = Frag2 p1 p2 in

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.UnfoldUntil delta_constant; Env.HNF; Env.Beta; 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 *)
 

tests/bug-reports/closed/Bug3644.fst

@@ -0,0 +1,11 @@
+module Bug3644
+
+let t = nat -> nat
+let s = nat -> GTot nat
+
+let f : t = (fun n -> n)
+let g : s = f
+
+// `g` must not have the type `nat -> GTot nat`
+[@@expect_failure [19]]
+let _ = assert (has_type g t)

tests/bug-reports/closed/Bug3659.fst

@@ -0,0 +1,37 @@
+module Bug3659
+
+let point t = unit -> t
+let dv_point t = unit -> Dv t
+
+let cast (#t: Type u#a) (f: point t) : dv_point t = f
+
+let is_inj #t #s (f: t->s) : prop =
+  forall x y. f x == f y ==> x == y
+
+// The `cast` function must not be injective.
+[@@expect_failure [19]]
+let cast_inj_fails (t: Type u#a) : squash (is_inj (cast #t)) = ()
+
+// Otherwise we would get an unsoundness:
+let cast_inj (t: Type u#a) : squash (is_inj (cast #t)) = admit ()
+
+let to_type (#t: Type0) (x: t) : Type0 = y:t { y == x }
+let to_type_inj t : squash (is_inj (to_type #t)) =
+  introduce forall (x y: t). to_type x == to_type y ==> x == y with
+  introduce _ ==> _ with _.
+  let x: to_type x = x in
+  let x: to_type y = coerce_eq () x in
+  ()
+
+let const #t (x: t) : point t = fun _ -> x
+let const_inj t : squash (is_inj (const #t)) =
+  assert forall x. const #t x () == x
+
+let f (t: Type u#a) : GTot Type0 = to_type (cast (const t))
+let f_inj : squash (Functions.is_inj (f u#a)) =
+  to_type_inj (dv_point (Type u#a));
+  cast_inj (Type u#a);
+  const_inj (Type u#a)
+
+let contradiction : squash False =
+  Cardinality.Universes.no_inj_universes_suc f

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)
@@ -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.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)))) =