fail to synthesize if with constant natural numbers

[lovettchris]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I can write this:

def u (x : Nat) : Nat := do
  let y := x + x
  y * (if y > 100 then 1 else y)

but if I change the final y to a constant 5 it no longer compiles:

def u (x : Nat) : Nat := do
  let y := x + x
  y * (if y > 100 then 1 else 5)

Steps to Reproduce

See above.

Expected behavior: [What you expect to happen]

should work

Actual behavior: [What actually happens]

failed to synthesize instance
  HMul Nat (Id Nat) ?m.260

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

Lean (version 4.0.0-nightly-2021-11-07, commit d5e05f3, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[leodemoura]

This is not a bug. Lean is working as expected. There is a lot going on in this example.

• Numerals in Lean are polymorphic, and Nat is the default instance when context information is not available.
• Arithmetic operations are all heterogeneous and parametrized by type classes: HAdd, HMul, etc.
• do blocks automatically lift pure code to monadic code, and between different monads.
• do blocks can be used in pure code by implicitly inserting the Id(identity) Monad.

There are also many ways to address this issue.

• Ignore. The code is not realistic to me. Novice users would not use do blocks in pure code.
• Improve the error message.
• Remove an existing feature. For example, if we disallow do blocks in pure code, the issue is gone.
• Support the scenario above by adding new instances or new features.
• ...

[dselsam]

if we disallow do blocks in pure code, the issue is gone.

FYI I use this feature all the time to get local mutation.

[leodemoura]

if we disallow do blocks in pure code, the issue is gone.

FYI I use this feature all the time to get local mutation.

It would still be doable, you would just have to explicitly use the Id monad.

BTW, I am not pushing for this solution, but I have seen users suggesting it.

[lovettchris]

I don't agree with option 1 "Novice users would not use do blocks in pure code.". I am a Novice user and I just did :-) So at a minmum we need a better error message pointing the user to these 2 possible solutions. But I still argue it is inconsistent at best that my first code block in my original bug rep[ort works, but the second does not.

So the 2 fixes I've found so far are, add a return statement:

def u (x : Nat) : Nat := do
  let y := x + x
  return y * (if y > 100 then 1 else 5)

remove the do

def u (x : Nat) : Nat := 
  let y := x + x
  y * (if y > 100 then 1 else 5)

[leodemoura]

I don't agree with option 1 "Novice users would not use do blocks in pure code.". I am a Novice user and I just did :-)

Not sure you are a novice user ;)
How did you get to this example?
Note that most new users would not even use monadic code, and just write pure definitions and theorems.

But I still argue it is inconsistent at best that my first code block in my original bug rep[ort works, but the second does not.

They are not the same. In the first one, you had y a non-polymorphic symbol. Its type is Nat. In the second, you replaced y with a polymorphic symbol (a numeral).

So the 2 fixes I've found so far are, add a return statement:

In both cases, you are avoiding the Id Nat vs Nat.
There are other ways to "fix" the example.
The general guideline is to provide additional type information. Example: numerals are polymorphic, I am seeing an Id Nat. So, we would write (5 : Nat) instead.

[lovettchris]

No I really am a Novice so much so I didn't even know numerals were polymorphic. Now that you pointed that out I see there's another fix:

def u (x : Nat) : Nat := do
  let y := x + x
  y * (if y > 100 then 1 else (5 : Nat))

So how can we improve this error message so I would have realized that is what is going on ? I don't even know how to read this message:

failed to synthesize instance
  HMul Nat (Id Nat) ?m.1340

I can guess "HMul" is what the multiply elaborated to, Nat is the type that 'y' has already but (Id Nat) what is Id ?

[lovettchris]

And where do we write about the fact that numerals are polymorphic in the reference docs? I think dependent_type_theory.md brilliantly discussed polymorphism using List as an example which made all kinds of sense, but it missed the opportunity to really blow my mind and point out that numbers are polymorphic too!

And what made me try this example in the first place? I was exploring what you can do with the second part of a let statement, how much code can that second part expand to, and apparently, it can be a lot of code - with nested if-expressions I could have 10 pages of code where the bound variable y shows up someplace. Fun... could be used as a kind of templating system. where the x + x is being "plugged into the template" wherever the variable shows up...

[leodemoura]

No I really am a Novice so much so I didn't even know numerals were polymorphic.

You are not the standard novice either. The standard novice user would start using Lean in pure code, read the tutorial, and prove theorems. The do notation is usually used by advanced users that are trying to extend Lean using itself.
Yes, we want to support users that want to use Lean as a programming language and ignore all the math stuff, but this is not our priority right now.

So how can we improve this error message so I would have realized that is what is going on ?

We have to prioritize the issues and focus on the ones that are blocking the Mathlib port.
The priority is the Mathlib users.

(Id Nat) what is Id ?

It is the identity monad. If you jump to its definition, you will find

def Id (type : Type u) : Type u := type

namespace Id

instance : Monad Id where
  pure x := x
  bind x f := f x
  map f x := f x

And where do we write about the fact that numerals are polymorphic in the reference docs?

Here: https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#numerals

[Kha]

if we disallow do blocks in pure code, the issue is gone.

FYI I use this feature all the time to get local mutation.

Just to record my preferred solution here: I believe pure do should use a distinct keyword such as puredo. It is syntactically (← doesn't make any sense in it) and semantically (doesn't need to block on the expected type, shouldn't try to lift "actions" as seen here) distinct enough that it should be considered its own thing. This would also resolve the "Option monad issue".

[leodemoura]

Just to record my preferred solution here: I believe pure do should use a distinct keyword such as puredo ...

I don't like this one. It is extra complexity, a new keyword, and the benefit looks small to me.
It is also not clear whether it would fix the issue reported here or not. I am assuming puredo would still use the Do.lean code, and the Id monad would be used there since a monad is used in a few places (e.g., expanding for .. in .. do).
Are you proposing we have special support for puredo in Do.lean at every place where we use ctx.m?
BTW, as a user, I would prefer to explicitly use Id than writing puredo.

[dselsam]

In Haskell, I used to use runIdentity $ do ... all the time. Id.run do ... would be even less cumbersome. Not suggesting this but we could also call this puredo:

macro "puredo" cmds:doSeq : term => `(Id.run do $cmds)

example : Array Nat := puredo
  let mut xs := #[]
  for i in [:10] do xs := xs.push i
  return xs

[Kha]

Are you proposing we have special support for puredo in Do.lean at every place where we use ctx.m?

Only where it helps elaboration by hiding Id from the user. This should be mostly the Bind.bind $action ... quotations. In the simplest case, we could wrap action in pure beforehand.

[Kha]

(Strictly speaking, this part is independent from the "separate keyword" proposal)

[leodemoura]

In Haskell, I used to use runIdentity $ do ... all the time. Id.run do ... would be even less cumbersome. Not suggesting this but we could also call this puredo:

macro "puredo" cmds:doSeq : term => `(Id.run do $cmds)

example : Array Nat := puredo
  let mut xs := #[]
  for i in [:10] do xs := xs.push i
  return xs

Note that your suggestion does not fix the issue here.

macro "puredo" cmds:doSeq : term => `(Id.run do $cmds)

def u (x : Nat) : Nat := puredo
  let y := x + x
  y * (if y > 100 then 1 else 5)

would still produce the same error.

[leodemoura]

Only where it helps elaboration by hiding Id from the user. This should be mostly the Bind.bind $action ... quotations. In the simplest case, we could wrap action in pure beforehand.

It may work, but this kind of change can easily trigger unforeseen problems.

[dselsam]

would still produce the same error.

I was thinking that the Id.run (or the puredo) would make the Id explicit, so this would no longer be a surprising error message. Also, contra #770 (comment), on reflection I think it is not a big deal if Id.run/puredo is required to get do behavior in pure context.

[leodemoura]

Yes, Id.run would make it clear, but puredo would not unless the user looks at its definition.

[tydeu]

BTW, as a user, I would prefer to explicitly use Id than writing puredo.

I second this. Also, @dselsam your example usage of the pure do:

FYI I use this feature all the time to get local mutation.

is very questionable.

What separates pure programming and monadic programming conceptually is precisely the forbidding of things like mutations. In a functional language, If one is using mutations, they should be doing so in a monadic context. And if one doesn't want the algorithm to pollute the function signature with an Id, one can (as you mentioned) use Id.run inside the function to get a monadic context.

The magical injection of a monadic context that Lean currently supports may be a little convenient (though is typing Id.run really that bad?). However, it creates exactly the kind of issues described here. Instead of novice users (and even advanced users who forgot to add a monad) getting a error message that says something along the lines of "can't use do in a pure context" (which is the conceptual mistake here), they get some opaque error that only makes sense if one fully understands the magic going on beyond the scenes.

Thus, I really think that the idea of a pure do should just be removed.

[leodemoura]

@tydeu Yeah, the error message "can't use do in a pure context" would solve the problem.
We could include also "consider prefixing the do with Id.run <| to instruct Lean to use the Identity monad". Then, the fix is clear to new users.

[lovettchris]

Thanks @leodemoura , looks great.