Ignore expected type for ▸

Stream: lean4

[Parth Shastri]

Is there a nice way to prevent a ▸ b from searching the expected type to determine the substitution and instead only search b? Here's my current workaround in a minimal example:

def add (x y : Nat) := x + y

example (h₁ : z = x + y) (h₂ : w = z) : w = add x y :=
  have := h₁ ▸ h₂; by exact this

Relying on by exact not influencing the expected type of thisfeels brittle, but removing it results in an error:

invalid `▸` notation, expected result type of cast is
  w = add x y
however, the equality
  h₁
of type
  z = x + y
does not contain the expected result type on either the left or the right hand side

[Reid Barton]

Does this work?

example (h₁ : z = x + y) (h₂ : w = z) : w = add x y :=
  (h₁ ▸ h₂ : _)

[Mario Carneiro]

No, that doesn't work any more in lean 4. I made a (e :) elaborator for this use case in a post somewhere, but I don't think it's been added to mathlib yet

[Mario Carneiro]

lean4#1797

[Mario Carneiro]

/poll What should the syntax for "elaborate e without expected type" be?
(e :) (implemented in lean4#1797)
(e : _) (used in lean 3, doesn't work without a special case in lean 4)

[Mario Carneiro]

Leo wants to know how people feel about the new syntax for elaborating without an expected type. The (e :) syntax is a little unusual, but you can think of it as a "type ascription with no type" since that's the intended effect.

[Arthur Paulino]

Writing nothing after ":" looks a bit out of place within the world of Lean 4 syntax

[Mario Carneiro]

it helps signal that this is different from other type ascriptions. In the original version the :) part was actually a token

[Mario Carneiro]

What I don't like about (e : _) is that we can't just make it work, the elaborator is too smart and sees around it. This has to be a special case which means that (e : _) and (e : ?_) won't act the same

[Mario Carneiro]

There is also the unstated "something else" alternative if you have a better idea for a type-ascription-ish syntax that signposts this behavior

[James Gallicchio]

I actually like the ( ... :) syntax... if I saw it without knowing about it, I'd almost certainly look it up / ask on Zulip, which seems like a good thing IMO

• it's fun to have little smilies in our codebases :)

[Mario Carneiro]

It is mentioned in the docstring when you hover on it BTW

[Mario Carneiro]

although the docstring for parentheses is unfortunately very overloaded, having to describe all the syntaxes:

• ()
• (e)
• (e :)
• (e : ty)
• (e1, e2)
• (· + ·)

[Jannis Limperg]

I would make it a keyword, i.e. elab_without_expected_type e or something. This situation is hopefully not common enough to warrant short (and very mysterious) notation.

[Mario Carneiro]

If it's longer than have' := e; exact this then it's not really worth it

[Mario Carneiro]

It doesn't come up that often but in the places I have wanted it I also wanted a syntax that felt "built-in" for it

[James Gallicchio]

not sure it's about length but rather clarity of intent, right? if anything (e :) is more clearly "we're doing something weird" than using exact e in this weird way

[James Gallicchio]

and some keyword like elab_without_expected_type is very clear in intent

[Mario Carneiro]

yes, but it's also so obnoxiously long that I would never want to use it outside a macro

[Gabriel Ebner]

Jannis Limperg said:

This situation is hopefully not common enough to warrant short (and very mysterious) notation.

$ cd mathlib
$ rg ' : _\)' | wc -l
391

[Jannis Limperg]

Why does additional information make the elaborator fail so often? Does Lean 4 also have this sort of issue?

[Mario Carneiro]

Elaborator decisions are not always "confluent". For example it might make the difference between putting the coercions in one place or another

[Mario Carneiro]

combine this with the fact that lean tries not to backtrack during elaboration and you get occasional failures in edge cases

[Mario Carneiro]

The issues here are usually not that the elaborator has made an unambiguously wrong decision, it is just making a different decision

[Mario Carneiro]

We want the elaborator to have reasonably predictable behavior so that limits how smart we can make the heuristics, and we also don't want it to timeout or re-elaborate things many times so that limits the ability to recover. This is one way among many to nudge the elaborator in the right direction in specific situations

[Jannis Limperg]

All right, interesting.