Optimize telescope type checking

[ice1000]

Currently, if you write (A B : Type), it is translated into (A : Type) (B : Type) right in the parser. This convenients the rest of the passes, but it makes the type term checked multiple times. If we can make it checked only once, that will save some heat produced by tycking, saving the world from global warming.

To do so, we need to change at least the concrete syntax, but not necessarily the core syntax.

This also applies to lambda terms.

[re-xyr]

I think the pain of doing that will be much larger than having to wait a bit longer in typechecking.

You are not serious about the global warming part right? It is induced by CO2, not heat from your computer.

[ice1000]

I think the pain of doing that will be much larger than having to wait a bit longer in typechecking.

Yes, I kinda agree, but if it turns out to be not that painful (both implementing it and maintaining it), it should be a good idea to do so.

This also contradicts @wsx-ucb's suggestion in another issue, which suggests that (A B : Type) and (A : Type) (B : Type) should be different semantically.

You are not serious about the global warming part right?

No.

[re-xyr]

that (A B : Type) and (A : Type) (B : Type) should be different semantically

What is Lean’s semantic?

[ice1000]

that (A B : Type) and (A : Type) (B : Type) should be different semantically

What is Lean’s semantic?

I have absolutely no idea. Maybe you can ask on Zulip or mention Seb on Twitter or look at the compiler.

[re-xyr]

I looked into Lean 3’s code and yes, it does that because it creates level meta during parsing instead. Not sure if you want to do that.

[ice1000]

I can't believe so. I don't think it's a good idea.