Heisenbug

Stream: general

[Scott Morrison]

I just found a Heisenbug: a proof that doesn't typecheck correctly, but if you add tactic.result >>= tactic.trace at the end, it does!

[Simon Hudon]

those are fun

[Simon Hudon]

I suspect that pretty printing either does some type checking (forcing some unification) or resolves some meta variables. You can try and see what is the smallest some term of the proof that you can print and which will fix the proof

[Scott Morrison]

I'm in the midst of further changes that will affect how my metavariables get handled, so I think I'm going to defer diagnosing this bug, hoping that if I don't look at it it will disappear permanently. :-)