Injectivity of inductive types revisited

src/smtencoding/FStar.SMTEncoding.Encode.fst

@@ -1228,8 +1228,9 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
                           params=tps;
                           t=k;
                           ds=datas} ->
+         let t_lid = t in
          let tcenv = env.tcenv in
-         let is_injective  =
+         let is_injective_on_params  =
              let usubst, uvs = SS.univ_var_opening universe_names in
              let env, tps, k =
                 Env.push_univ_vars tcenv uvs,
@@ -1267,22 +1268,48 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
                  | _ -> false
              in
              let u_leq_u_k u =
-                universe_leq (N.normalize_universe env_tps u) u_k
+                let u = N.normalize_universe env_tps u in
+                universe_leq u u_k 
              in
              let tp_ok (tp:S.binder) (u_tp:universe) =
                 let t_tp = tp.binder_bv.sort in
                 if u_leq_u_k u_tp
                 then true
-                else let formals, _ = U.arrow_formals t_tp in
-                     let _, _, _, u_formals = TcTerm.tc_binders env_tps formals in
-                     //List.iter (fun u -> BU.print1 "Universe of formal: %s\n" (Print.univ_to_string u)) u_formals;
-                     BU.for_all (fun u_formal -> u_leq_u_k u_formal) u_formals
+                else (
+                   let t_tp = 
+                      N.normalize
+                          [Unrefine; Unascribe; Unmeta;
+                          Primops; HNF; UnfoldUntil delta_constant; Beta]
+                          env_tps t_tp
+                   in
+                   let formals, t = U.arrow_formals t_tp in
+                   let _, _, _, u_formals = TcTerm.tc_binders env_tps formals in
+                   let inj = BU.for_all (fun u_formal -> u_leq_u_k u_formal) u_formals in                  
+                   if inj
+                   then (
+                     match (SS.compress t).n with
+                     | Tm_type u -> 
+                      (* retain injectivity for parameters that are type functions
+                         from small universes (i.e., all formals are smaller than the constructed type)
+                         to a universe <= the universe of the constructed type.
+                         See BugBoxInjectivity.fst *)
+                       u_leq_u_k u
+                     | Tm_name _ -> (* this is a value of another type parameter in scope *)
+                       true
+                     | _ ->
+                       false
+                   )
+                   else (
+                      false
+                   )
+
+                 )
              in
              List.forall2 tp_ok tps us
         in
         if Env.debug env.tcenv <| Options.Other "SMTEncoding"
         then BU.print2 "%s injectivity for %s\n"
-                    (if is_injective then "YES" else "NO")
+                    (if is_injective_on_params then "YES" else "NO")
                     (Ident.string_of_lid t);
         let quals = se.sigquals in
         let is_logical = quals |> BU.for_some (function Logic | Assumption -> true | _ -> false) in
@@ -1306,9 +1333,17 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
                     if List.length indices <> List.length vars
                     then failwith "Impossible";
                     let eqs =
-                        if is_injective
+                        if is_injective_on_params
+                        || Options.ext_getv "compat:injectivity" <> ""
                         then List.map2 (fun v a -> mkEq(mkFreeV v, a)) vars indices
-                        else [] in
+                        else (
+                            //only injectivity on indices
+                            let num_params = List.length tps in
+                            let _var_params, var_indices = List.splitAt num_params vars in
+                            let _i_params, indices = List.splitAt num_params indices in
+                            List.map2 (fun v a -> mkEq(mkFreeV v, a)) var_indices indices
+                        )
+                    in
                     mkOr(out, mkAnd(mk_data_tester env l xx, eqs |> mk_and_l)), decls@decls') (mkFalse, []) in
                 let ffsym, ff = fresh_fvar env.current_module_name "f" Fuel_sort in
                 let fuel_guarded_inversion =

tests/bug-reports/Bug3186.fst

@@ -3,7 +3,14 @@ module Bug3186
 let base (x:int) (_: unit {equals x 0}) =
   assert (x == 0)
 
-let base2 (x:int) (_: equals x 0) =
+let base2 (x:int) (hyp: equals x 0) =
+  let Refl = hyp in 
+  assert (x == 0)
+
+ //fails since the inversion on equals is not strong enough
+ //to be usable directly, since df6fb0d52e52289db625cbdbc7c34d975801d819
+[@@expect_failure [19]]
+let base2' (x:int) (hyp: equals x 0) =
   assert (x == 0)
 
 [@@expect_failure [19]]

tests/bug-reports/BugBoxInjectivity.fst

@@ -0,0 +1,72 @@
+module BugBoxInjectivity
+// #restart-solver
+// #push-options "--log_queries --query_stats --debug BugBoxInjectivity --debug_level SMTEncoding"
+module CC = FStar.Cardinality.Universes
+noeq
+type test (a:Type u#0 -> Type u#1) : Type u#1 =
+  | Mk : test a
+
+let const (f:Type u#1) : Type u#0 -> Type u#1 = fun _ -> f
+let itest (f:Type u#1) : Type u#1 = test (const f)
+let itest_inhabited (f:Type u#1) : itest f = Mk 
+let const_inversion (f0 f1:Type u#1)
+: Lemma 
+  (requires const f0 == const f1)
+  (ensures f0 == f1)
+= let _f0 = const f0 int in
+  let _f1 = const f1 int in
+  assert (_f0 == _f1);
+  ()
+let itest_injective (f0 f1:Type u#1) 
+: Lemma
+  (ensures itest f0 == itest f1 ==> const f0 == const f1)
+= let x : test (const f0) = itest_inhabited f0 in
+  let Mk #_ = x in
+  ()
+open FStar.Functions
+let itest_injective' : squash (is_inj itest) = 
+  introduce forall f0 f1.
+      itest f0 == itest f1 ==> f0 == f1
+  with introduce _ ==> _
+  with _ . (
+    itest_injective f0 f1;
+    const_inversion f0 f1
+  )
+[@@expect_failure [189]] //itest is not in the right universe to use this lemma
+let fals : squash False =
+  CC.no_inj_universes itest
+
+
+#push-options "--ext 'compat:injectivity'"
+noeq
+type test2 (a:Type u#0 -> Type u#2) : Type u#1 =
+  | Mk2 : test2 a
+#pop-options
+let const2 (f:Type u#2) : Type u#0 -> Type u#2 = fun _ -> f
+let itest2 (f:Type u#2) : Type u#1 = test2 (const2 f)
+let itest2_inhabited (f:Type u#2) : itest2 f = Mk2
+let const2_inversion (f0 f1:Type u#2)
+: Lemma 
+  (requires const2 f0 == const2 f1)
+  (ensures f0 == f1)
+= let _f0 = const2 f0 (FStar.Universe.raise_t int) in
+  let _f1 = const2 f1 (FStar.Universe.raise_t int) in
+  assert (_f0 == _f1);
+  ()
+let itest2_injective (f0 f1:Type u#2) 
+: Lemma
+  (ensures itest2 f0 == itest2 f1 ==> const2 f0 == const2 f1)
+= let x : test2 (const2 f0) = itest2_inhabited f0 in
+  let Mk2 #_ = x in
+  ()
+open FStar.Functions
+let itest2_injective' : squash (is_inj itest2) = 
+  introduce forall f0 f1.
+      itest2 f0 == itest2 f1 ==> f0 == f1
+  with introduce _ ==> _
+  with _ . (
+    itest2_injective f0 f1;
+    const2_inversion f0 f1
+  )
+let fals () : squash False =
+  CC.no_inj_universes itest2

ulib/FStar.ModifiesGen.fst

@@ -17,7 +17,7 @@ module FStar.ModifiesGen
 
 #set-options "--split_queries no"
 #set-options "--using_facts_from '*,-FStar.Tactics,-FStar.Reflection,-FStar.List'"
-
+#set-options "--z3rlimit_factor 2"
 module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 
@@ -217,7 +217,11 @@ let loc_equal_elim (#al: aloc_t) (#c: cls al) (s1 s2: loc c) : Lemma
   (ensures (s1 == s2))
   [SMTPat (s1 `loc_equal` s2)]
 = fun_set_equal_elim (Loc?.non_live_addrs s1) (Loc?.non_live_addrs s2);
-  fun_set_equal_elim (Loc?.live_addrs s1) (Loc?.live_addrs s2)
+  fun_set_equal_elim (Loc?.live_addrs s1) (Loc?.live_addrs s2);
+  let Loc regions1 region_liveness_tags1 _ _ aux1 = s1 in
+  let Loc regions2 region_liveness_tags2 _ _ aux2 = s2 in
+  assert (regions1 == regions2);
+  assert (region_liveness_tags1 == region_liveness_tags2)
 
 
 let loc_union_idem #al #c s =
@@ -1757,7 +1761,7 @@ let mem_union_aux_of_aux_left_intro
 : Lemma
   (GSet.mem x aux <==> GSet.mem (ALoc x.region x.addr (if None? x.loc then None else Some (make_cls_union_aloc b (Some?.v x.loc)))) (union_aux_of_aux_left c b aux))
   [SMTPat (GSet.mem x aux)]
-= ()
+= let ALoc _ _ _ = x in ()
 
 let mem_union_aux_of_aux_left_elim
   (#al: (bool -> HS.rid -> nat -> Tot Type))
@@ -2118,12 +2122,12 @@ let upgrade_aloc (#al: aloc_t u#a) (#c: cls al) (a: aloc c) : Tot (aloc (raise_c
 let downgrade_aloc_upgrade_aloc (#al: aloc_t u#a) (#c: cls al) (a: aloc c) : Lemma
   (downgrade_aloc (upgrade_aloc u#a u#b a) == a)
   [SMTPat (downgrade_aloc (upgrade_aloc u#a u#b a))]
-= ()
+= let ALoc _ _ _ = a in ()
 
 let upgrade_aloc_downgrade_aloc (#al: aloc_t u#a) (#c: cls al) (a: aloc (raise_cls u#a u#b c)) : Lemma
   (upgrade_aloc (downgrade_aloc a) == a)
   [SMTPat (upgrade_aloc u#a u#b (downgrade_aloc a))]
-= ()
+= let ALoc _ _ _ = a in ()
 
 let raise_loc_aux_pred
   (#al: aloc_t u#a)
@@ -2166,6 +2170,7 @@ let raise_loc_includes #al #c l1 l2 =
 #pop-options
 
 let raise_loc_disjoint #al #c l1 l2 =
+  // let ALoc _ _ _ = al in
   let l1' = raise_loc l1 in
   let l2' = raise_loc l2 in
   assert (forall (x: aloc (raise_cls c)) . GSet.mem x (Ghost.reveal (Loc?.aux l1')) <==> GSet.mem (downgrade_aloc x) (Ghost.reveal (Loc?.aux l1)));