isDefEq causes maximum recursion depth has been reached when given type argument mismatched

[Qiu233]

Description

This bug only occurs when using big operator.

If S is given by axiom S : Finset ℕ rather than in the context, the bug disappears.
If P is defined not using ∏, the bug disappears.

Steps to Reproduce

import Mathlib

lemma card {a b : Finset α} : a = b → a.card = b.card := congrArg _

example := by
  let S := Finset.range 10000
  let P : ℕ := ∏ a ∈ S, a
  have t : P = (∏ a ∈ S, a) := by rfl
  have := card t

Expected behavior: No error or should have been caught.

Actual behavior: Error on card t.

Versions

• 4.9.0
• 4.11.0-rc2
• 4.16.0-rc1

Context

Code like card t above is generated (by meta-programming) to test whether lemmas like card can be applied to some term so we get new facts.
What we want is to recover if test fails, but unfortunately it crashes our meta-program.

This bug occurs only once in millions of such tests. No other similar case found yet, so it might be not vital.

[Kha]

Could you provide any context for this bug, is it something people stumble over naturally?

[Qiu233]

Could you provide any context for this bug, is it something people stumble over naturally?

Of course. Context has been updated.