Merge pull request #3028 from mtzguido/fix-hashcons-env

Hashconsed arrows/abstractions in the SMT encoding must be abstracted over their free variables

examples/layeredeffects/GTWP.fst

@@ -56,16 +56,23 @@ let bind (a b : Type) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a
   | D -> coerce (d_bind #_ #_ #wc #wf (coerce c) f)
 // GM: would be nice to skip the annotations.
 
-let subcomp (a:Type) (i:idx) (wp1 : wp a)
-                             (wp2 : wp a)
-                             (f : m a i wp1)
+let subcomp (a:Type u#aa) (i:idx)
+            (wp1 : wp a)
+            (wp2 : wp a)
+            (f : m a i wp1)
    : Pure (m a i wp2)
           (requires (forall p. wp2 p ==> wp1 p))
           (ensures (fun _ -> True))
    = match i with
      | T -> f
      | G -> f
-     | D -> coerce f
+     | D ->
+       (* This case needs some handholding. *)
+       let f : raise_t (unit -> DIV a wp1) = f in
+       let f : unit -> DIV a wp1 = downgrade_val f in
+       let f : unit -> DIV a wp2 = f in
+       assert_norm (m a i wp2 == raise_t (unit -> DIV a wp2));
+       coerce (raise_val f)
 
 unfold
 let ite_wp #a (w1 w2 : wp a) (b:bool) : wp a =

src/fstar/FStar.CheckedFiles.fst

@@ -40,7 +40,7 @@ module Dep     = FStar.Parser.Dep
  * detect when loading the cache that the version number is same
  * It needs to be kept in sync with prims.fst
  *)
-let cache_version_number = 58
+let cache_version_number = 59
 
 (*
  * Abbreviation for what we store in the checked files (stages as described below)