lean4

lean4 copied to clipboard

example [Inhabited Empty] : α := (default : Empty).rec
                               --^ term goal (instance missing)

example [Inhabited α] : α := default
                           --^ term goal (instance shown)

example [Inhabited α] : β := _
                           --^ term goal (instance shown)

I would expect type-class instances to be shown always. This is all quite confusing since they show up just fine if you write by exact..

Versions

Since 484e5102216badf51e3738242c45c982895f8d6c

See also #1345

We have been trying to minimize the local context in error messages and the expected type info view. It may not be perfect, but we don't want to give it up because it is very helpful in many other cases. Note that, in tactic mode, we don't perform the aggressive local context filtering. This is why by exact ... produces a different behavior.

Are you proposing we never filter out local instances? This is a simple change.

We have been trying to minimize the local context in error messages and the expected type info view.

I know, that's why I'm trying to bring up particularly surprising or confusing cases that I run into. Also so that we have some papertrail about what we want to be hidden or not.

It may not be perfect, but we don't want to give it up because it is very helpful in many other cases.

I certainly agree that there is room for improvement. Do we have a list of things that we absolutely should hide? I tried to find out concrete motivating examples for hiding inaccessible assumptions but couldn't find any discussion on Zulip or github, so this is a recollection of issues that came up recently.

• Implementation details of macros. Like the discr in syntax matches or do_jp in do-notation. (Note that these should probably also be hidden from assumption etc.)
• Let-values in programming contexts. (See also Mario's let dep proposal in #1345)
• Auxiliary declarations. (Note that these definitely need to be hidden from tactics as well.)

Did I miss anything?

Are you proposing we never filter out local instances? This is a simple change.

That would be an easy fix for this particular issue, yes.

Let-values in programming contexts. (See also Mario's let dep proposal in https://github.com/leanprover/lean4/issues/1345)

I like the let dep proposal, but we should probably get support from users first. BTW, we can even use the nonDep flag to implement this feature :) We would also be able to remove let_fun. BTW, should we call it let dep or let_dep?

Did I miss anything?

I think you covered the main cases. I am also assuming you view the "expected type info view" as something that provides a mechanism for inspecting the whole local context, not only what is relevant to make sense of the expected type.

Let-values in programming contexts. (See also Mario's let dep proposal in #1345)

I like the let dep proposal, but we should probably get support from users first. BTW, we can even use the nonDep flag to implement this feature :) We would also be able to remove let_fun. BTW, should we call it let dep or let_dep?

I was also thinking about let!, although I think this kind of "try harder" naming convention is more common in mathlib than in core so maybe users with a different naming sense would prefer let dep.

BTW, should we call it let dep or let_dep?

I'd prefer let dep over let_dep (it fits in with let mut). I'm not sure I like the dep though (which I associate with dependent types, which this is not), but I don't have a better name.

I am also assuming you view the "expected type info view" as something that provides a mechanism for inspecting the whole local context, not only what is relevant to make sense of the expected type.

Yes indeed. Maybe it was a mistake to title it "expected type" in the editor. The motivation for the feature was to read complicated term-mode proofs in mathlib (also requested by the community). Dropping inaccessible hypotheses does not help with understanding golfed proofs like ⟨fun ⟨_, _⟩ => ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, fun ⟨_, _⟩ => ⟨_, (hq _).2 ‹_›⟩⟩. :smile:

Let-values in programming contexts. (See also Mario's let dep proposal in #1345)

I like the let dep proposal, but we should probably get support from users first. BTW, we can even use the nonDep flag to implement this feature :) We would also be able to remove let_fun. BTW, should we call it let dep or let_dep?

I was also thinking about let!, although I think this kind of "try harder" naming convention is more common in mathlib than in core so maybe users with a different naming sense would prefer let dep.

Yeah, and we have been using the ! suffix for things that may panic at runtime.

Regarding using the nonDep flag: I was actually thinking the other way around: we would rename let_fun to let and let to something else, so let syntax would normally desugar the same as have and the letE expr constructor would only be used for this let! thing.

I'm not sure I like the dep though (which I associate with dependent types, which this is not)

You could think of it as dependable let... :)

letD is short and reminiscent of letI from mathlib which was used in the instance use-case (no longer needed in lean 4)...?

I'd like to reserve the letI name for "inline" let, which does not produce a let-binding at all.

I completely agree with Gabriel, let dep fits perfectly with let mut (which probably will be the more common of the two)

Regarding using the nonDep flag: I was actually thinking the other way around: we would rename let_fun to let and let to something else, so let syntax would normally desugar the same as have and the letE expr constructor would only be used for this let! thing.

I prefer to use the nonDep flag. It seems more robust than using ((fun x => e) v) + Expr.mdata.

• We can distinguish between beta-reduction and let-expansion in different places (example: simp).
• let+nonDep flag is more efficient to process when using the locally nameless approach. We already have code for efficiently processing blocks of nested lets or lambdas. It seems to verbose to encode long blocks of nested (e.g., let x1 := v1; let x2 := v2; e) using the let_funs (e.g., ((fun x1 => (fun x2 => e) v2) v1).)

I completely agree with Gabriel, let dep fits perfectly with let mut (which probably will be the more common of the two)

I agree, and I would love to have a corresponding let ??? for letI :) let inline is probably too verbose :)

Is it feasible to use command keywords here: def for let dep and abbrev for let inline?

Regarding let_fun verbosity: although I think that's a good argument for why to use letE, I think that also points to the need to have a telescope operator for handling nested let_fun independent of whether it is being used in the desugaring here. That seems worthy of special case handling. (Another thing to consider is that the lambda/app encoding has a different n-ary extension, (fun x1 x2 => e) v1 v2. I guess there isn't an n-ary let_fun to go with it, but a binder traversal would probably want to deal with this too.)

I have no input on the 🚲 🏠 , but regarding the representation I agree with Leo that using letE with nonDep, as well as deleting let_fun if possible seems like the best option. To advertise my own experiments a bit, I have been trying out a custom let_opaque which does not zeta-reduce and has extra lifting rules. I found the mdata approach to be a little gnarly to handle during normalization. In the end I am using a combinator which abstracts let-bindings and reintroduces mdata, but it is finnicky to ensure it gets preserved everywhere.

Okay one input on shed:

I'm not sure I like the dep though (which I associate with dependent types, which this is not), but I don't have a better name.

But that's exactly what this is known as, a dependent let! The type of the body can depend on the value of the binding.

But that's exactly what this is known as, a dependent let! The type of the body can depend on the value of the binding.

Do you have a reference for that? I have never heard of it before. (Also note that your description does not reflect the feature we're discussing here. Here the type-checking of the body may depend on the value of the let-binding, this makes a difference even if the body has a type like Nat.)

Also note that your description does not reflect the feature we're discussing here.

Hmm? I thought this entire discussion of Mario's proposal (which did diverge from the original topic) was (morally) to hide the defeq x = v when typechecking e in let x := v; e and to introduce a let dep with the current behaviour (where the defeq is available).

was (morally) to hide the defeq x = v when typechecking e in let x := v; e and to introduce a let dep with the current behaviour

Not just morally, I'd say, but fully: the kernel should reject let n := 42; (.ofNat 0 : Fin n).1 as well.

Also note that your description does not reflect the feature we're discussing here.

Hmm?

I think this was just a misunderstanding. You meant the right thing, but wrote "the type of the body can depend on the value of the binding" which is something different. To be concrete (with current syntax):

let     n := 42; (.ofNat 0 : Fin n).1
let_fun n := 42; (.ofNat 0 : Fin n).1

Both bodies have type Nat (modulo type-checking errors), and Nat does not depend on n or that n reduces to 42. However only the first one type-checks.

David Renshaw just reminded me of another reason why hiding hypotheses is confusing: tactics can fail if you have extra hypotheses in the local context. (So you have to call clear first.) If the extra hypotheses are hidden, you don't even know what's wrong. (See https://github.com/leanprover-community/mathlib4/issues/404. If pairwise was in Type instead of Prop, then you'd need to clear an invisible hypothesis.)