Hashes for `Expr.lam` and `Expr.forallE` are the same

The hash computations for Expr.lam and Expr.forallE are the same when they have the same binders and bodies. The implementation of the computed field Expr.data does not mix in anything to differentiate these constructors.

This situation can occur in practice. Consider for example the following function, where the motive (as an Expr.lam) leads to a type whose hash collides.

open Lean Elab in
elab "#hashes " t:term : command => Command.runTermElabM fun _ => do
  let e ← Term.elabTermAndSynthesize t none
  e.forEach fun node => do
    logInfo m!"{hash node}: {node}"

set_option pp.funBinderTypes true
#hashes id <| fun b => Bool.recOn (motive := fun _ => Bool) b true false
/-
2384416661: id fun (b : Bool) ↦ Bool.recOn b true false
2927525288: id
1812194161: @id
3551570259: Bool → Bool
183048209: Bool
2428420263: fun (b : Bool) ↦ Bool.recOn b true false
2175286235: Bool.recOn #0 true false
4279372883: Bool.recOn #0 true
1771607792: Bool.recOn #0
1088603745: Bool.recOn
149233892: @Bool.recOn
3551570259: fun (x : Bool) ↦ Bool
351589370: #0
3057640288: true
1995999671: false
-/

Notice 3551570259 for both fun (x : Bool) ↦ Bool and Bool → Bool

Context

Zulip discussion

Versions

4.8.0

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4