Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?

Question

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running #print on the internal definition that the compiler produces. It produces the following error:

16:12: type mismatch at application
  ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
term
  λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0
has type
  nat.below (λ (ᾰ : ℕ), ℕ) 0 → ℕ : Type
but is expected to have type
  ?m_1 0 : Sort ?

Why is there an error when I'm just pasting code from the output of the Lean compiler? Is there some special context needed for internal definitions to be interpreted correctly? What is the best way to take an internal definition and convert it into something that will type check properly?

I'm using Lean 3.46 with lean-mode in Emacs.

The example code:

def leanfib : ℕ → ℕ
| nat.zero := nat.zero
| (nat.succ nat.zero) := (nat.succ nat.zero)
| (nat.succ (nat.succ n)) := (leanfib (nat.succ n)) + (leanfib n)

#eval list.map leanfib (list.range 12)
#print leanfib
#print leanfib._main

def «print of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  ᾰ.brec_on
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ.succ),
               ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ.succ.succ),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F)
         ᾰ
         _F)

EDIT: Jason Rute's answer and followup comments helped me find the right conversation on the Lean zulip chat forum to resolve my issue. Basically, if you are having trouble with "round trip" errors from the pretty printer, the first step is to activate an option: set_option pp.all true. After setting this option, the output of #print on that function becomes much much more verbose and complicated, but does typecheck correctly. I had a feeling that activating this option is in some sense applying "excessive force". After doing some digging in the source, it turns out that this is indeed that case: setting the "pp.all" option to true (as of version 3.46) is equivalent to setting the following:

set_option pp.implicit true
set_option pp.proofs true
set_option pp.coercions true
set_option pp.notation false
set_option pp.universes true
set_option pp.full_names true
set_option pp.beta false
set_option pp.numerals false
set_option pp.strings false
set_option pp.binder_types true
set_option pp.generalized_field_notation false

I was able to repair the "type-check-ability" of this example by combining the full force of "pp.all" with the lighter touch of setting "pp.generalized_field_notation" to false, which produces the following output:

def «print (with pp.generalized_field_notation=false) of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  nat.brec_on ᾰ
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ ᾰ)),
               nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ (nat.succ ᾰ))),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F)
         ᾰ
         _F)

This is much simpler than what is produced by printing with "pp.all", but still has the error: invalid 'nat.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known. However, by looking at the big ugly term that gets printed with "pp.all" (which I haven't reproduced here because it is so big and ugly), I was able to determine the type of the lambda that encloses the term that produces the error. Then this version can be fixed by annotating that type, as follows:

def «repaired print (with pp.generalized_field_notation=false) of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  nat.brec_on ᾰ
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       let t₁ : Π (ᾰ : ℕ), nat.below.{1} (λ (ᾰ : ℕ), ℕ) ᾰ → ℕ :=
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ ᾰ)),
               nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ (nat.succ ᾰ))),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F) in t₁ ᾰ _F)

In summary, the original term that got printed by the pretty printer was indeed close to the right thing. The version printed by using option "pp.generalized_field_notation" is even closer to the right thing, but still needs some type information. This type information can be obtained by looking at the version that gets printed by using "pp.all".

Answer 1

This is a known problem in Lean 3. Output from the pretty printer will sometimes not parse back into Lean. You can find a lot about this on the Lean Zulip discussed as the round-trip issue with the pretty printer. I heard it will be better in Lean 4 and at least there used to be notes about it in the delaborator code for Lean 4.

Edit: Applying set_option pp.all true can often lead to output which is parsable, although incredibly verbose.

However, if you find a specific thing which is broken in Lean 3, I would file a GitHub issue at https://github.com/leanprover-community/lean. I’ve heard some issues are hard to fix, but others might be a one line change if you file an issue with a MWE.)