Internal error in opaque block when case splitting when just given extended lambda

[oskeri]

For the code below, the following sequence of commands produces an internal error on version 2.6.4 and on master:

1. Refine the goal with λ { x → {! x !} }
2. Case-split on x

data ⊤ : Set where
  tt : ⊤

opaque
  f : ⊤ → ⊤
  f = {! λ { x → {! x !} } !}

The error is

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\Interaction\MakeCase.hs:222:7 in Agda-2.6.5-2CGFfl0UVRq2oEiF8zwYoq:Agda.Interaction.MakeCase

Reloading between refining and case-splitting does not give an error.

[andreasabel]

The error is thrown in this function: https://github.com/agda/agda/blob/691b30a54350d047b6efd9b6d4bf61279c4761ec/src/full/Agda/Interaction/MakeCase.hs#L209-L222 It turns out that getConstInfo returns an AbstractDef Function{..} here, so, somehow the opacity logic does not allow unfolding of the extended lambda. A quick fix would be to just strip the AbstractDef wrapper here, but I guess we should understand why it is returned like this and fix the underlying problem.

[plt-amy]

Having (finally! my apologies) looked at it, the issue is that the extended lambda is added to the "declares" set of the unfolding block, but not the unfolds set. That's because we only update the unfolds set at the end of scope-checking the top-level module. Fix coming up..