How can I hide a name in the REPL?

Question

As stated in the answer to this question, the %hide directive allows one to make an existing name inaccessible:

import Data.String

%hide fib

%default total

fib : Nat -> Nat
fib n = loop n 0 1
  where
    loop : Nat -> Nat -> Nat -> Nat
    loop Z a _ = a
    loop (S k) a b = loop k b (a + b)

parseNat : String -> Maybe Nat
parseNat = map cast . parsePositive

response : String -> String
response s = case parseNat s of
  Just n => "fib n = " ++ show (fib n)
  Nothing => "n ∉ ℕ"

partial main : IO ()
main = repl "n = " ((++ "\n") . response)

This works fine in the code above:

*Main> :exec
n = 10
fib n = 55

However, it does not seem to carry over to the REPL:

*Main> fib 10
Can't disambiguate name: Main.fib, Prelude.Nat.fib

How can I cause the %hide directives from my code to carry over into the REPL?

Answer 1

I think you can't and the only way to invoke your function is to use its fully qualified name, e.g. Main.fib 10 would work.