Timeout when using exact

Stream: new members

[VayusElytra]

Hello, a very strange situation today.
I have the following tactic state in a proof:
image.png

Naively I thought I could just conclude from here with exact hincl. However, after a while of trying, Lean instead highlights the theorem name in red with the error message "(deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached
Use set_option maxHeartbeats <num> to set the limit.
Additional diagnostic information may be available using the set_option diagnostics true command.".

I am very confused what could be causing it to loop infinitely here when the goal and the hypothesis seem syntactically equivalent to me.
Apologies for not providing an MWE; I could not reproduce this when trying elsewhere and this would require copying 300 lines of code to work.

[Ruben Van de Velde]

Try intro B; convert hincl B and see if anything pops

[Floris van Doorn]

You can also click on both the type of hincl and the goal in the infoview and see if there are any differing implicit arguments.
Some other things to look out for:

• You introduced any data using have instead of let in your tactic proof (especially deceptive if it was a type class)
• You are working with Decidable/DecidableEq + open Classical
• You declared your own instances that are not compatible with Mathlib instances.