Accidentally recursive definitions

[gebner]

Synport:

namespace Bool

theorem coe_sort_tt : coeSort.{1, 1} true = True :=
  coe_sort_tt

In Lean 3 coe_sort_tt would resolve to _root_.coe_sort_tt resulting in a non-recursive alias definition. But in Lean 4, coe_sort_tt now resolves to Bool.coe_sort_tt and we get a (nonterminating) recursive definition.