Agda loops on simple code with a record and a hole

[guillaumebrunerie]

Agda loops when trying to type-check the simple code below (which should type-check without any issues). It also ends up using all the memory available although this is not progressive, it alternates between moments where memory usage increases quickly and calm periods.

If the field A is taken out of the record (either as a postulate or as a goal), if the argument of eq is replaced by A, or if C is replaced by a postulate, then it works.

open import Agda.Builtin.Equality

record R : Set₁ where
  field
    A : Set
    a : A
    eq : a ≡ a → a ≡ a

C : R
C = {!!}

open R C

test : a ≡ a → a ≡ a
test p = eq p

[guillaumebrunerie]

It loops with versions 2.5.4.1 and 2.5.3 as well.

[guillaumebrunerie]

Memory usage does not seem to increase at all with 2.5.3, but it does with 2.5.4.1 and with master at about the same rate (4.4 G after 30 seconds, 8.7 G after one minute, 17.3G after two minutes).

[guillaumebrunerie]

It also works if we add no-eta-equality in R.

[andreasabel]

Seems like we are building a cycle here:

C = _8
_8 = record { A = _15; a = _16; eq = _17 }
_15 = C .A

which blows up when we try to eta expand _16 or type _15.
The metaOccursCheck does not look into the definition C because it is not mutual with test.

[andreasabel]

Fixed with Ulf at AIM XXIX: The problem is that a frozen meta is eta-expanded, and the new metas are not frozen. This renders freezing of record metas inefficient in some cases, and the occurs check relies on proper freezing for detecting cycles.
Solved by eta-expanding frozen record metas to records of frozen(!) metas.