Meta weirdness (was: `norm_num` question)

Stream: general

[Notification Bot]

Michael Stoll has marked this topic as unresolved.

[Michael Stoll]

Here is something weird: When I additionally import analysis.normed.field.basic in the example above, then I get an error message rec_fn_macro only allowed in meta definitions at the line meta def prove_test : ....
This does not occur when I instead import one of the files imported by analysis.normed.field.basic. What is going on here?
In a similar situation, I get an error message missing 'noncomputable' modifier, definition 'prove_foo' depends on 'rat.normed_field', which seems to be triggered by the use of norm_num.prove_ne. This is quite annoying...

[Kevin Buzzard]

Coincidentally this came up within the last day or two on the Discord. You can fix it with instance : ring ℚ := division_ring.to_ring ℚ. See #16349 which probably @Mario Carneiro should be alerted to...(and which will fix the problem if the PR is accepted, but the PR might cause other issues)

[Michael Stoll]

Thanks, Kevin!
Can you also explain how this error arises? (Just out of curiosity.)

[Kevin Buzzard]

The part I understand: the import makes the ring structure on the rationals noncomputable, because the typeclass inference system can find a new way to prove Q is a ring after the import, via normed_ring which is noncomputable, and by chance this is the preferred way after the import. The fix is to explicitly make the computable construction and explicitly add it into the system, which then prefers this choice and all of a sudden it's computable again. The part I don't understand is the rec_fn_macro error, I searched for it on this site and found several other occurrences, which all seemed to be to do with computability, but I can't say I understand the problem properly. The reason I tagged Mario in the previous post was two-fold; firstly to point out the PR to him (becuase there might be reasons against the change) but secondly to alert him to your error (which I think he understands quite well).

[Mario Carneiro]

The issue is when some auxiliary definition mistakenly gets marked computable when it shouldn't be, there is some edge case here that results in bad error messages

[Kevin Buzzard]

I was hoping that I could fix everything by adding noncomputable! all over the place but I couldn't get rid of the error.

[Mario Carneiro]

IIRC if you put noncomputable theory too you can get noncomputable on that pesky internal definition

[Michael Stoll]

It looked like analysis.normed.field.basic uses noncomputable theory, but I didn't look at it too closely.

[Yaël Dillies]

Yeah, we can make rat.normed_field computable using some trickery. I can do that if you want.

[Michael Stoll]

For now, I am happy with the workaround that Kevin mentioned. But it would be nice, of course, if the error would not show up in the first place.