AST: More robust recursion check for opaque types with infinite underlying types
Tracking seen declarations and substitution maps only detects the
situation where the opaque type's underlying type contains itself
with the same substitution map. However, it is also possible to
recurse with a different substitution map.
In general termination is undecidable with a problem like this,
so instead of trying to catch cycles, just impose a termination
limit.
This converts a stack overflow into an assertion, which is still
not ideal; we should really diagnose something instead. But this
is a first step.