Zulip Chat Archive

Stream: general

Topic: Forever inferring the same instance

Anne Baanen (Aug 23 2021 at 08:56):

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 (Aug 23 2021 at 09:15):

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

Anne Baanen (Aug 23 2021 at 09:18):

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 (Aug 23 2021 at 09:20):

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 (Aug 23 2021 at 09:24):

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

Anne Baanen (Aug 24 2021 at 13:14):

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 (Aug 24 2021 at 14:30):

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

Anne Baanen (Aug 24 2021 at 14:38):

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

Anne Baanen (Aug 24 2021 at 14:41):

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 (Aug 24 2021 at 14:51):

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

Last updated: Dec 20 2023 at 11:08 UTC