From ce248c76cc1d3a503d48f556c74122e14bdfc40a Mon Sep 17 00:00:00 2001
From: Xavier Denis <xldenis@gmail.com>
Date: Wed, 1 Nov 2023 14:48:44 +0100
Subject: [PATCH] Improve inference of Ghost when erased

---
 creusot-contracts-dummy/src/lib.rs | 2 +-
 creusot-contracts/src/lib.rs       | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/creusot-contracts-dummy/src/lib.rs b/creusot-contracts-dummy/src/lib.rs
index fb0a0d8d18..c0614b720a 100644
--- 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
index a09bf20432..248f8b2990 100644
--- 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)
         }
     }