Test "bugs/eta-ctor-alias"
Expected: ✋ reject · Size: 7.2 KB · Lines: 122 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Bogus proof that f = Box.mk for every f : BoxFn, where BoxFn is a
reducible alias for Bool → Box.
A checker that eta-expands a partially applied constructor (see
corner-cases/eta-ctor) has to take the missing arguments from the type of
the constructor application. Taking them from the type of the other side
without unfolding it, here BoxFn, finds no arguments to add, then compares
the (zero) given fields only, and accepts.
This bug was found by phiferd in a draft of https://github.com/leanprover/lean4/pull/15373 to the official kernel, and fixed before it was merged.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | ✋ | 1 ms | 40.2 MB | |||
| mathgraph | ✋ | 1 ms | 36.1 MB | |||
| nanoclo | ✋ | 1 ms | 45.9 MB | |||
| con-ron | ✋ | 23 ms | 58.8 MB | |||
| nanobruijn | ✋ | 1 ms | 9.0 MB | |||
| nanoda | ✋ | 1 ms | 3.5 MB | |||
| lazylean | ✋ | 1 ms | 21.7 MB | |||
| con-leche | ✋ | 4 ms | 22.2 MB | |||
| eink0rn | ✋ | 2 ms | 12.4 MB | |||
| official | ✋ | 28 ms | 67.4 MB | |||
| ind-models | ✋ | 100 ms | 103.8 MB | |||
| lean4lean | ✋ | 72 ms | 105.1 MB | |||
| tenet | ✋ | 136 ms | 45.2 MB | |||
| tenet-hs | ✋ | 1 ms | 9.5 MB | |||
| lean4cobol | ✋ | 5 ms | 13.6 MB | |||
| evmlean | ✋ | 1.6 s | 276.9 MB | |||
| mini | ✋ | 34 ms | 73.8 MB | |||
| overfull | ✋ | 15.5 s | 46.7 MB | |||
| metalean-slow | ✋ | 31 ms | 72.1 MB | |||
| tenet-jvm | ✋ | 117 ms | 65.5 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.6 MB | |||
| kiota | ✋ | 1 ms | 7.4 MB | |||
| metalean-fast | ✋ | 30 ms | 72.2 MB | |||
| canonical-min | 🚫 | 387 ms | 1.1 GB | |||
| rpylean | ✋ | 1 ms | 4.4 MB | |||
| vow-lean-kernel | ✋ | 88 ms | 8.6 MB | |||
| parse-only | 👍 | 28 ms | 65.7 MB |