splitter does not thunk argument-less alternatives #11211
Description
(This is a non-issue; I thought we have an issue and I investigated, but could not produce an actual problem. But I still want to record this investigation as a P-low issues, or maybe someone else sees how to exploit this.)
A match statement with an alternative that does no bind any variables thunks that alternative, so that that arm is not evaluated when it isn't actually taken:
def f (xs : List Nat) : Nat :=
match xs with
| [] => dbg_trace "f []"; 1
| _ => dbg_trace "f _"; 2
/--
info: f.match_1.{u_1} (motive : List Nat → Sort u_1) (xs✝ : List Nat) (h_1 : Unit → motive [])
(h_2 : (x : List Nat) → motive x) : motive xs✝
-/
#guard_msgs in
#check f.match_1
Surprisingly this isn't done for the splitter, despite the use of splitters in program (it wouldn't matter for proofs) is explicitly supported; see h_1 in
/--
info: f.match_1.splitter.{u_1} (motive : List Nat → Sort u_1) (xs✝ : List Nat) (h_1 : motive [])
(h_2 : (x : List Nat) → (x = [] → False) → motive x) : motive xs✝
-/
#guard_msgs in
#check f.match_1.splitter
I tried to write a program that uses split and has unexpected evaluation behavior, e.g. something like
def g (xs : List Nat) : Nat := by
have this : f xs = f xs := rfl
unfold f at this
split at this
· exact (dbgTrace "g []" (fun _ => 1))
· exact (dbgTrace "g _" (fun _ => 2))
/--
info: def g : List Nat → Nat :=
fun xs =>
have this := ⋯;
f.match_1.splitter
(fun xs_1 =>
xs = xs_1 →
((match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) =
match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) →
Nat)
xs
(fun h =>
Eq.ndrec (motive := fun xs =>
((match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) =
match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) →
Nat)
(id fun this => dbgTrace "g []" fun x => 1) ⋯)
(fun x x_1 h =>
Eq.ndrec (motive := fun x =>
(x = [] → False) →
((match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) =
match xs with
| [] => dbgTrace (toString "f []") fun x => 1
| x => dbgTrace (toString "f _") fun x => 2) →
Nat)
(fun x => ⋯.mpr fun this => dbgTrace "g _" fun x => 2) h x_1)
⋯ this
-/
#guard_msgs in
#print g
/--
info: f []
---
info: 1
-/
#guard_msgs in
#eval f []
/--
info: f _
---
info: 2
-/
#guard_msgs in
#eval f [1]
/--
info: g []
---
info: 1
-/
#guard_msgs in
#eval g []
/--
info: g _
---
info: 2
-/
#guard_msgs in
#eval g [1]
But alas we don't have a problem here: The use of split (which is the main user-facing entry point to using the splitter) will invariably always refine the scrutinee and maybe some hypotheses from the context (here: this), so there is a lambda in the alternative and no eager evaluations happens.
So all well for now (unless someone finds a way to expose this issue). Maybe I’ll “fix” it during some refactoring anyways, just to be safe and for more similarity between matchers and splitters.
(In fact, now that I think about it, this may be a reason why #10184 did not have the impact I expected 🤔 ).
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.