val ref ([@@@ strictly_positive] a:Type u#1)
  : Type0
let ref a = ref' a
val ref ([@@@ strictly_positive] a:Type u#1)
  : Type0
let ref a =
ref' a
Steel.ST.GhostHigherReference.fst.checked
Steel.ST.HigherReference.fst.checked Steel.ST.Coercions.fsti.checked Steel.HigherReference.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GhostHigherReference.fst
Steel.ST.GhostHigherReference.ref'
module Steel.ST.GhostHigherReference

// needed because I need to know that `Steel.ST.HigherReference.ref a`
// can be turned into `Steel.HigherReference.ref a`
friend Steel.ST.HigherReference

module RST = Steel.ST.HigherReference
module R = Steel.HigherReference

module STC = Steel.ST.Coercions

// FIXME: WHY WHY WHY in `Ghost.reveal (ref a)` is `a` not strictly positive?

[@@erasable]
noeq
type ref' ([@@@strictly_positive] a : Type u#1) : Type0
= | Hide: (reveal: R.ref a) -> ref' a
val ref ([@@@ strictly_positive] a:Type u#1)
  : Type0
a: Type -> Type0