Improve inference of Ghost when erased

creusot-rs · Nov 1, 2023 · ce248c7 · ce248c7
1 parent 338c7e7
commit ce248c7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/creusot-contracts-dummy/src/lib.rs b/creusot-contracts-dummy/src/lib.rs
@@ -29,7 +29,7 @@ pub fn proof_assert(_: TS1) -> TS1 {
 
 #[proc_macro]
 pub fn gh(_: TS1) -> TS1 {
-    quote::quote! { creusot_contracts::ghost::Ghost::dummy() }.into()
+    quote::quote! { creusot_contracts::ghost::Ghost::from_fn(|| unsafe { std::hint::unreachable_unchecked() }) }.into()
 }
 
 #[proc_macro_attribute]

diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs
@@ -187,14 +187,14 @@ pub mod ghost {
         T: ?Sized;
 
     impl<T: ?Sized> Ghost<T> {
-        pub fn dummy() -> Ghost<T> {
+        pub fn from_fn(_: fn() -> T) -> Self {
             Ghost(std::marker::PhantomData)
         }
     }
 
     impl<T: ?Sized> Clone for Ghost<T> {
         fn clone(&self) -> Self {
-            Self::dummy()
+            Ghost(std::marker::PhantomData)
         }
     }