Different elab results

Stream: lean4

[Marcus Rossel]

In the following examples, the third case elaborates different from the first two:

import Lean
open Lean Meta Elab Tactic

elab "type_of" t:term : tactic => do
  withMainContext do
    let ex ← Tactic.elabTerm t none
    let ty ← inferType ex
    IO.println ty

example (h : ∀ x : Nat, 1 + x = x + 1) : True := by
  type_of h
  -- forall (x : Nat), Eq.{1} Nat (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) x) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) x (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))

example : True := by
  type_of (sorry : ∀ x : Nat, 1 + x = x + 1)
  -- forall (x : Nat), Eq.{1} Nat (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) x) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) x (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))

example : True := by
  have h : ∀ x : Nat, 1 + x = x + 1 := sorry
  type_of h
  -- forall (x : Nat), Eq.{?_uniq.1161} Nat (HAdd.hAdd.{?_uniq.1164, ?_uniq.1163, ?_uniq.1162} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{?_uniq.1167} Nat 1 (instOfNatNat 1)) x) (HAdd.hAdd.{?_uniq.1179, ?_uniq.1178, ?_uniq.1177} Nat Nat Nat (instHAdd.{0} Nat instAddNat) x (OfNat.ofNat.{?_uniq.1182} Nat 1 (instOfNatNat 1)))

In particular, it contains lots of universe level metavariables. Why is that/ how can I have it elaborate to the same result as the other two cases?

[Kyle Miller]

When you print with IO.println, it's using toString which has no access to the MetaM state. Make sure to instantiateMVars

[Kyle Miller]

Or, maybe instead do logInfo m!"{ty}" or similar. The logInfo function captures the MetaM state and does pretty printing.

[Kyle Miller]

You don't need to instantiateMVars in that case.

[Marcus Rossel]

Using instantiateMVars on ty does indeed fix it. Why is the last case different from the other two in the first place though?

[Kyle Miller]

The last case is how I'd expect it to normally be. There's no reason to assume that expressions have every metavariable's value substituted in.

[Kyle Miller]

I briefly tried looking into the source for why (sorry : ∀ x : Nat, 1 + x = x + 1) seems to instantiate all the metavariables in the type of sorry, and nothing popped out as being the reason.