When does Repr not work?

Stream: lean4

[Chris Lovett]

I know Leo explained this to me before but I'm still confused why Repr doesn't work on Option:

inductive Option (α : Type) : Type where
  | none : Option α
  | some (val : α) : Option α
  deriving Repr

/-
expression
  Option.none
has type
  Option ?m.704
but instance
  Lean.Eval (Option ?m.704)
failed to be synthesized, this instance instructs Lean on how to display
the resulting value, recall that any type implementing the `Repr` class
also implements the `Lean.Eval` class
-/
#eval Option.none

#eval Option 10  -- this works fine and prints "some 10" so why can't Option.none print "none" ?

So when can I expect Repr to fail like this? Any time there is an unresolved metavariable? Could Repr be specialized in this case so that it prints "none" since the metavariable does not need to be resolved in that case?

[Mario Carneiro]

You would need that unresolved metavariable to have a Repr instance to be able to print "none"

[Mario Carneiro]

I don't think we should try to evaluate terms containing free variables in #eval

[Mario Carneiro]

I would suggest just writing (none : Option Nat) or whatever

[Mario Carneiro]

or @none Nat if you prefer

[Mario Carneiro]

Even if the type did have a repr instance unconditionally you will get a different error:

inductive Foo (α : Type)
| foo : Foo α

instance : Repr (Foo α) := ⟨λ _ _ => "Foo"⟩

#eval Foo.foo
-- don't know how to synthesize implicit argument
--   @Foo.foo ?m.168
-- context:
-- ⊢ Type

[Mac]

A more Rust-like way for this to work, would be to instead export none from a singleton None type that is coercible to Option. For example:

namespace Alt

inductive None
| none
deriving Repr

export None (none)

instance : Coe None (Option α) := ⟨fun _ => Option.none⟩

#eval none --- Alt.None.none
#eval (none : Option Nat) -- none

[Mac]

Such a flexible None type could also coerce to other types with null constructors (e.g. List):

instance : Coe None (List α) := ⟨fun _ => List.nil⟩

Alternatively, Unit/PUnit could be use for this purpose instead rather than creating a new type.