pp.analyze doesn't add type annotations to ofNat

Stream: lean4

[Jakub Nowak]

import Mathlib

set_option pp.analyze true

variable {V K : Type} [Field K] [AddCommGroup V] [Module K V] (w : V)

#check 0 • w

#check (0 : K) • w

The type of 0 in the first case is ℕ, and K in the second. Yet, pretty printer prints the same expressions.

[Kyle Miller]

pp.analyze hasn't seen active development for a few years. I've done some occasional maintenance to keep it from breaking as the pretty printer has changed.

In this case, it might have something to do with the fact that it's got a hard-coded list of heterogenous binary operations: docs#Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHBinOp

However, with a quick skim of the code, that list seems to be for avoiding unnecessary type ascriptions, so I'm not sure if that's the explanation.

[Kyle Miller]

Are you able to verify that pp.analyze ever adds type ascriptions to ofNat numerals? I'm assuming you have, given your Mathlib-specific smul example, rather than a Lean-only example.

[Jakub Nowak]

I was too lazy to make the example Lean-only, I'll check, but I suspect that it never produces type hint for ofNat. The pretty printer often does bad job and makes things unreadable, and I'm sometimes use pp.analyze true to make things more readable. Like in the example above, I would expect the default pretty printer to print 0 with type hint in the second case. Unfortunately it doesn't, and pp.analyze doesn't either.

[Jakub Nowak]

Here's Lean-only mwe.

structure Foo where
  n : Nat

structure Bar where
  n : Nat

instance : OfNat Foo n where
  ofNat := .mk n

instance : OfNat Bar n where
  ofNat := .mk n

instance : HMul Foo Nat Nat where
  hMul | { n }, m => n * m

instance : HMul Bar Nat Nat where
  hMul | { n }, m => n * m

set_option pp.analyze true

#check (3 : Foo) * 42

#check (3 : Bar) * 42

[Kyle Miller]

Is my understanding correct that this MWE is meant to demonstrate that pp.analyze doesn't print type ascriptions for ofNat? This is something that can be observed already built-in types, like

set_option pp.analyze true
#check (1 : Nat) * 1
#check (1 : Int) * 1

Given your mwe is still complicated, can I ask for further clarification: are these meant to illustrate only that pp.analyze does not add ascriptions for ofNat, or are you reporting a a bug in an interaction between pp.analyze, ofNat, and heterogeneous operators?

[Kyle Miller]

This is a strong mwe to demonstrate that pp.analyze isn't able to add type ascriptions:

set_option pp.analyze true

def f {α : Type} (_ : α) : Nat := 0

#check f (1 : Nat)
#check f (1 : Int)

[Jakub Nowak]

I'm only reporting this as a bug with ofNat and pp.analyze. I was trying to produce an example, where the type cannot be deduced from the type of the resulting expression. Which I think your first example fails to show.

[Jakub Nowak]

Ah yes, I think your second example captures the problem, and is much simpler than mine.

[Kyle Miller]

There are additional pp.analyze options. Try set_option pp.analyze.trustOfNat false

[Jakub Nowak]

Ah, yes, though, it exists for a reason, without it, it's too verbose where it doesn't have to be:

set_option pp.analyze true
set_option pp.analyze.trustOfNat false

/-- info: HMul.hMul (α := Nat) 0 0 : Nat -/
#guard_msgs in
#check 0 * 0

That's probably something that could be improved. Instead of "trusting" OfNat, we could try to analyze where the type annotation is necessary .

[Robin Arnez]

I'll just mention set_option pp.numericTypes true which simply always prints the type of ofNats. That at least works for this case but it might be too extreme.