lean hanging mwe

Stream: lean4

[James Gallicchio]

Weird mwe:

def Cached {α : Type _} (a : α) := { b // b = a }

structure Hashed where
  k : UInt64
  hash : Cached (k >>> 30)

Causes lean to hang on 4.0.0-nightly-2022-09-22

[Henrik Böving]

What happens if you start reducing the 30?

[James Gallicchio]

Oh that's bizarre -- 0 finishes instantly, and then by 4 it takes 20 seconds

[James Gallicchio]

For some reason for large enough values it doesn't even report the timeout, just hangs

[James Gallicchio]

You don't even need the subtype, embedding it in the struct also causes slowdown:

private def finishHash (x : UInt64) : UInt64 :=
  let x := x ^^^ (x >>> 30)
  let x := x * 0xbf58476d1ce4e5b9
  let x := x ^^^ (x >>> 27)
  let x := x * 0x94d049bb133111eb
  let x := x ^^^ (x >>> 31)
  x

structure Hashed (κ) [Hashable κ] where
  k : κ
  hashk : UInt64
  h_hash : hashk = finishHash (hash k)

but it's noticeably faster than the subtype version (thus the larger hash function, which is impossibly slow with the subtype)

[James Gallicchio]

And of course making finishHash opaque works fine

[Henrik Böving]

I'm guessing its trying to do some reduction operations on the >>> which causes it to hang for big numbers then

[James Gallicchio]

Making it irreducible doesn't prevent the hanging, but I'm not really sure what @[irreducible] controls