Typeclass synthesis constructs exponentially large proof terms for diamond-shaped instance graphs

The following diamond-shaped class hierarchy has a valid solution at every depth, and synthesis finds the search path quickly (sub-millisecond via tabling). However, the constructed proof term grows as 2^n because both branches of each diamond independently embed the full proof of the shared ancestor. This causes synthesis to silently fail once the proof term exceeds synthInstance.maxSize.

set_option synthInstance.maxHeartbeats 80000000

class T0 where u : Unit := ()
instance : T0 := {}

class L0 where u : Unit := ()
class R0 where u : Unit := ()
instance [T0] : L0 := {}
instance [T0] : R0 := {}

class T1 where u : Unit := ()
instance [L0] [R0] : T1 := {}

class L1 where u : Unit := ()
class R1 where u : Unit := ()
instance [T1] : L1 := {}
instance [T1] : R1 := {}

class T2 where u : Unit := ()
instance [L1] [R1] : T2 := {}

-- ... continuing this pattern to depth 19 ...

At each level, both Li and Ri require Ti, and T{i+1} requires both Li and Ri. The tabled resolution algorithm correctly avoids redundant search, but the proof term duplicates the Ti solution into both branches.

Observed behavior:

With synthInstance.maxSize 128 (default), synthesis fails around depth 7.
With synthInstance.maxSize 2000000, synthesis fails at depth 19.
With synthInstance.maxSize 200000000, depth 19 succeeds instantly.

The failure is always a bare failed to synthesize with no diagnostic about the size limit being hit — the oversized solution is silently rejected in addAnswer.

Expected behavior: Since the search succeeds in O(n) time via tabling, the proof term should also be O(n) — e.g., by sharing the Ti subterm between the Li and Ri branches using let bindings.

🤖 Prepared with Claude Code

Reproduce the diamond hierarchy with the reported synthInstance.maxSize values and observe where synthesis fails. Read the synthesis addAnswer path, where oversized solutions are silently rejected, and trace how tabled answers become proof terms. Done means valid depth-19 synthesis no longer creates exponentially large terms or fails silently due to the size limit.