Agda 2.6.4 RC1 fails to terminate type checking

[martinescardo]

Agda 2.6.4 RC1 with TypeTopology (https://github.com/martinescardo/TypeTopology) fails to terminate in the module source/Iterative/Ordinals.lagda.

The whole module is syntax-highlighted, using agda2-highlight-level 'interactive, so it is difficult to see where in the file the problem is occurring.

[martinescardo]

By manual bisection, the function whose type checking seems to loop is Ord-to-𝕍-behaviour in line 917 of the above file.

[andreasabel]

Not sure if it is related, but I noticed an error in debug printing:

Debug printing tc.lhs.top:10 failed due to exception:
  An internal error has occurred. Please report this as a bug.
  Location of the error: impossible, called at src/full/Agda/TypeChecking/Rules/Def.hs:755:46 

agda/src/full/Agda/TypeChecking/Rules/Def.hs

Lines 752 to 755 in 8c4f28a

	reportSDoc "tc.lhs.top" 10 $ vcat
	[ "Clause before translation:"
	, nest 2 $ vcat
	[ "delta =" <+> do escapeContext impossible (size delta) $ prettyTCM delta

[andreasabel]

With -v10, Agda hangs at checking Ord-to-𝕍-behaviour, last words:

term _b_1399 := Iterative.Sets.φ-emb 𝓤 ua
                (Underlying.⟨ underlying-type-of-ordinal ⟩ α)
                (λ x → Ord-to-𝕍 (α ↓ x)) (_1389 (𝓤 = 𝓤) (ua = ua) (α = α))
                , (λ x → pr₂ (Ord-to-𝕍 (α ↓ x)))

Turning the body of Ord-to-𝕍-behaviour into a hole and then giving it succeeds.

Looks like the occurs checker is looping:

$ agda-2.6.4 Issue6759.lagda -v tc.meta.assign:20 -v tc.meta.occurs:40 
...
term _b_39 := Iterative.Sets.φ-emb 𝓤 ua
              (Underlying.⟨ underlying-type-of-ordinal ⟩ α)
              (λ x → Ord-to-𝕍 (α ↓ x)) (_29 (𝓤 = 𝓤) (ua = ua) (α = α))
              , (λ x → pr₂ (Ord-to-𝕍 (α ↓ x)))
mvar args: 2 1 0
fvars lhs (rel): 0 1 2
fvars lhs (nonstrict):
fvars lhs (irr):
initOccursCheck: we look into the following definitions:
Ord-to-𝕍-behaviour
occursCheck: meta variable _29 has relevance Relevant and quantity Quantity0 Q0Inferred
Meta occurs check found bad relevance
aborting because occurrence is flexible
initOccursCheck: we look into the following definitions:
Ord-to-𝕍-behaviour
<<BUSY>>

[andreasabel]

My bisection run says: 2af2ff1 is the first bad commit

Date: Tue Nov 29 17:39:24 2022 +0100
[ fix #6364 ] Only filter instances based on their type, not their body

But I am not sure this is right, need to verify.

Ok, this commit is bad in the sense that it exhibits the loop, but is it the first?

Another bisect from v2.6.3 to this commit confirms, yes. (Ping @jespercockx .)

[andreasabel]

What is weird about this bisection result is that TypeTopology does not use instance arguments.

[martinescardo]

It actually does use instance arguments. See source/Notation/*.lagda. If my automatic count is correct, 32 files declare instances (where some files declare lots of them, e.g. source/Various/Dedekind.lagda).

[andreasabel]

@martinescardo: I made the mistake to grep in *.agda which didn't return any hits, but not for the reasons I believed...

Instance resolution has gone through a change, which is skimpily described in the changelog as follows:

agda/CHANGELOG.md

Lines 284 to 287 in 84b6bb2

	* [**Breaking**] The algorithm for resolution of instance arguments
	has been simplified. It will now only rely on the type of instances
	to determine which candidate it should use, and no longer on their
	values.

More information can be found in the issue and the PR:

• Instance candidates filtered out by type errors #6364
• Only filter instances based on their type, not their body #6368

It seems that other libraries had to be changed to work with the simplified instance resolution, so maybe a "continues to work without changes" cannot be expected for developments that use instance arguments.
What is not nice here, though, is that the result is not a failure to resolve some instances, but a seeming non-termination in the occurs checker.

[andreasabel]

@jespercockx : Do you have time to look at this issue? It is blocking the next RC...

[jespercockx]

I could try to take a look, but could you post the file that you used for bisection? That'd be a lot easier than starting from the TypeTopology library.

[martinescardo]

This example I could try to reduce. However, it is very strange. I tested the whole of TypeTopology with Agda 2.6.4 RC1, and only two errors, in 165k lines, occur, this one, and the __IMPOSSIBLE__ one in issue #6758.

What's more, regarding the issue here, a very similar short function occurs in another file with the same shape as this one, and no errors occur.

[andreasabel]

@jespercockx Thanks! I put the files used for bisection up here:

• Issues with Agda 2.6.4 RC1 martinescardo/TypeTopology#176

[jespercockx]

Comparing the debug output between 2.6.3 and 2.6.4, here is what I can make of the situation:

• There are two metavariables _29 and _39.
• The meta _29 comes from a type signature, so it is given modality @0.
• Due to a change in the instance resolution, the order in which the metavariables _29 and _39 are solved is reversed: in 2.6.3, _29 is solved first, but in 2.6.4 Agda first tries to solve _39 instead.
• The meta _29 appears in the solution to _39 in a flexible position.
• Since _29 has modality @0, it is not allowed to be used in the solution to _39, causing a pattern violation.
• Since the position of _29 in the solution of _39 is flexible, Agda doesn't do the usual trick of promoting _29 to a stricter modality.
• Agda thinks it might be able to get rid of it by normalising the solution of _39.
• Unfortunately, in this case normalising the solution takes a very long (infinite?) time. This was not noticeable in 2.6.3 since it was never normalised.

Writing this down and noticing that you are using --lossy-unification has given me an idea of how this could be solved: when --lossy-unification is enabled, we could apply the modality promotion of metavariables more eagerly as well. This might lose solutions, but with --lossy-unification you already don't have the guarantee of unique solutions, and the fact that you are using it implies avoiding normalisation is probably more important.

[jespercockx]

Good news: my idea seems to fix the issue. After a few hours of staring at debug output, actually implementing the fix only took a minute. I've made a PR at #6796.

[jespercockx]

I wonder if a better solution that attacks the problem at its root would be to provide a flag that disables the normalization heuristic in the occurs checker. This wouldn't cause any regressions (like my fix in #6759 doesn), but would allow users who care more about performance than about powerful inference to turn off the part that makes Agda's typechecker slow.

[andreasabel]

@jespercockx wrote:

provide a flag that disables the normalization heuristic in the occurs checker.

One could experiment with this and see how larger developments are affected. I have no intuition how often normalization is needed in practice in the occurs check.

[martinescardo]

Thanks for fixing this issue!

[nad]

Without normalisation there is presumably a risk that Agda's behaviour could be more brittle: replacing one piece of code with something definitionally equivalent could make the code stop working. We use normalisation in with abstraction to avoid problems of this kind, but the normalisation also makes with very slow in certain situations. On the other hand, the reflection machinery does not enforce normalisation, even though this could lead to brittleness.

Perhaps we could have a broader discussion about these things. My opinion is that, given that a non-trivial definitional equality is one of the defining features of this kind of type theory, we should try to make most features respect definitional equality.