Forever inferring the same instance

Stream: general

[Anne Baanen]

I'm having trouble understanding a timeout in #8761: I modified some typeclass instances on intermediate_field so they are as general as the subalgebra instances they are defined in terms of. In combination with docs#polynomial.gal.is_scalar_tower, this caused a timeout here, but the weird thing is: there is no actual loop in the instances, yet it keeps trying to infer the fact parameter to docs#polynomial.gal.is_scalar_tower, receiving a cached failure, and trying again. How is this happening, and how can we stop this from happening?

Here's a slightly minimized test case. I didn't manage to minimize this any further - apparently it's a subtle issue.

[Eric Wieser]

Is it actually a loop, or does bumping the heartbeat limit let it succeed?

[Anne Baanen]

I have left it compiling that file on the command line for like 15 minutes, without any indication of finishing. So if it's not forever, it's at least for way too long.

[Anne Baanen]

Although that was with a lot of set_option trace.whatever enabled. Perhaps it will be a "bit" faster without so much I/O...

[Anne Baanen]

Indeed, now the instance correctly fails within "only" 5 minutes.

[Anne Baanen]

From some more testing with is_def_eq_detail later, and it looks like the real issue is that it's trying to unify docs#polynomial.gal.algebra p p.splitting_field : algebra p.splitting_field p.splitting_field with docs#algebra.id p.splitting_field, which causes a huge mass of unfolds, and the repeated fact inference is a side-effect of this unification. Since we don't really care about the definition of gal.algebra, I'll just mark it as irreducible so the attempted unification doesn't take so long. Or is there a better way?

[Frédéric Dupuis]

This sounds like it might be another manifestation of this issue.

[Anne Baanen]

Good point, that looks like it's exactly the same issue.

[Anne Baanen]

For now, it seems I successfully worked around the issue by putting back the old is_scalar_tower instance as a specialization of the others, so it will get applied quickly in the common cases.

[Eric Wieser]

That's what I ended up doing for many of the generalized module instances