deriving Hashable on recursive inductive

Stream: lean4

[Yuri de Wit]

The builtin deriving handler can deal with this simple recursive inductive:

inductive T
| a
| b (t : T)
deriving Hashable

However, it does not seem to be able to handle the following:

inductive T2
| a
| b (ts : List T2)
deriving Hashable -- ERROR: failed to synthesize instance Hashable (List T2)

Even though there is a Hashable instance for (List α), Lean can't synthesize the instance.

The generated mutual and instance looks good:

mutual
       private partial def hashT2✝ (x✝ : @T2) : UInt64✝ :=
         match x✝ with
         | @T2.a => 0
         | @T2.b a✝ => mixHash✝ 1 (hash✝ a✝)
end
instance : Hashable (@T2) := ⟨hashT2✝⟩

But it can't resolve (hash✝ a✝) for the List argument.

What am I missing here?

[Henrik Böving]

the type is not declared as Hashable during the definition of the function so there is no instance to be found. Instead of recursively calling hash here it should do something with hashT2 on the list, probably a sort of fold operation.

[Yuri de Wit]

I see. I missed the fact that the generated hashT is calling hashT directly and not going through typeclass resolution.

Thanks.

[Tom]

What option did you specify/what did you write to see that mutual code? I tried a variety of the pp flags but can't get the infoview to show it.
Thanks.

[Yuri de Wit]

Hi @Tom , I used set_option trace.Elab.Deriving.hashable true. It will dump the mutual block and the instance.

[Yuri de Wit]

Henrik Böving said:

Instead of recursively calling hash here it should do something with hashT2 on the list, probably a sort of fold operation.

The fact that the Hashable (List α) instance is already the needed fold, makes inlining of this fold operation solution unsatisfactory, though. It seems that there needs to be a better solution for these mutual references.

[Yuri de Wit]

Yuri de Wit said:

Hi Tom , I used set_option trace.Elab.Deriving.hashable true. It will dump the mutual block and the instance.

FYI, here is the deriving handler for Hashable src/Lean/Elab/Deriving/Hashable.lean (was enlightening to look at):

def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
  if (← declNames.allM isInductive) && declNames.size > 0 then
    let cmds ← liftTermElabM <| mkHashableInstanceCmds declNames
    cmds.forM elabCommand
    return true
  else
    return false