dbg_trace in match discriminants breaks generalization

Stream: lean4

[Eric Wieser]

If I use dbg_trace in a match discriminant, then it blocks generalization:

example (x : Nat) (hx : x ≠ 0) : Fin x :=
  match x, hx with
  | (_ + 1), _ => 0

example (x : Nat) (hx : x ≠ 0) : Fin x :=
  match dbg_trace "oh no"; x, hx with
  | (_ + 1), _ => 0  -- type error, because the goal is still `Fin x` and not `Fin (_ + 1)`

is this a reasonable thing to want? Is it remotely possible to fix?

[Mario Carneiro]

I lean toward "it's not a reasonable thing to want"

[Mario Carneiro]

this is kind of part of the challenge of working in dependent type theory, you can inspect the code that was written just prior and if you add additional code then the types can break

[Eric Wieser]

The context here is trying to confirm how many timesf is evaluated in

example (x : Nat) (f : Nat → Nat) (hx : f x ≠ 0) : Fin (f x) :=
  match f x, hx with
  | 2, _ => 0
  | (_ + 1), _ => 0

[Mario Carneiro]

you can use the motive := argument of match to explicitly generalize

[Eric Wieser]

(and the context for that is to try and work out if quote4#31 introduces any double-evaluation bugs)

[Mario Carneiro]

I would expect it to only evaluate f once there

[Mario Carneiro]

looking at the generated IR for the example confirms it is only evaluated once

[Eric Wieser]

How hard would it be to implement match? that tells me the motive that was found automatically?

[Mario Carneiro]

possible?

[Mario Carneiro]

there is a lot of stuff going on in match though, you might have to do a lot of copy paste

[Eric Wieser]

Presumably it would be much easier to implement in core, which already has all the info?

[Mario Carneiro]

you could also do it as a code action

[Mario Carneiro]

might be nice to have "insert type" code actions in more places generally

[Mario Carneiro]

in fact "insert value of underscore" would cover a pretty wide variety of insertion tasks

[Mario Carneiro]

unfortunately using match (motive := _) doesn't work