fix recRecursive when record isn't recursive

[flupe]

A bug in agda/agda2hs#257 is caused by it relying on TypeChecking/Monad/Base:recRecursive which may fail when recMutual is set to Nothing.

[andreasabel]

Not sure what you are after here, but I can't see how this makes sense.

If you want to query recRecursive before the mutuality computation has run, maybe you want to change the type to Defn -> Maybe Bool.

Currently, the invariant is that recRecursive is never queried before it has been set to Just _.

[andreasabel]

Well, the semantics of recMutual = Nothing is that nothing is known about mutualilty yet.
If you want not mutual you have to make sure this gets set to Just [].

[flupe]

Are you saying that all record definitions should have recMutual set to Just once typechecking is done?

Because the bug from agda2hs I'm refering to comes from a record definition compiled with the backend. We call recRecursive (presumably after typechecking is completed, since it's a backend compile hook) on the given record which definitely still has recMutual set to False Nothing when it reaches the backend.

[andreasabel]

We call recRecursive (presumably after typechecking is completed, since it's a backend compile hook) on the given record which definitely still has recMutual set to False when it reaches the backend.

(I think you meant to write Nothing, not False.)
Yes, recRecursive should be set latest once all checking phases are completed (type/coverage/termination... checking).

[flupe]

Thank you for the clarification. So I guess there is still an issue with the record from agda/agda2hs#257 never getting recMutual populated by Agda before reaching the backend. I will investigate this later, closing this PR.

[andreasabel]

@flupe Maybe this PR fixes your problem in agda2hs:

• Fix mutual information not being set properly by the positivity checker #7149

[flupe]

Thank you for the heads up!