ghost_in_runtime: a ghost value used by the running program

A ghost parameter (ghost s : T), a ghost let and a ghost fn exist only for proofs: the compiler removes them before the program runs. So the program itself may not use one. A ghost value may appear only where nothing runs:

• in a refinement, such as a parameter’s or the result’s;
• in another ghost let, or as the argument of a ghost parameter;
• as a lemma’s argument, or in a proof hint (assert … by, calc);
• in a ghost fn’s body.

Returning it, branching or matching on it, capturing it in a closure, passing it to an ordinary parameter, or calling a ghost fn from ordinary code is this error.

A program that triggers it

mod Main do
  fn clamp(x : Int, ghost limit : Int) : Int do
    if x > limit do limit else x end
  end
end

The fix

If the program needs the value, it is not ghost: make it an ordinary parameter.

mod Main do
  fn clamp(x : Int, limit : Int) : Int do
    if x > limit do limit else x end
  end
end

If only the proof needs it, keep it ghost and use it in the contract instead:

mod Main do
  fn below(ghost limit : Int, x : {Int | _ < limit}) : {Int | _ < limit} do
    x
  end
end

Why the rule exists

Erasing ghost code must not change what the program does. If a branch, a result or a closure could depend on a ghost value, removing it would leave the program reading something that no longer exists, or would change its behaviour. Keeping ghost values out of every runtime position makes erasure safe by construction.

See also: the lemmas guide, ghost_misuse.