Another interal error in Substitute:72 when filling a hole

[caryoscelus]

Using Agda version 2.5.4.2 (similar #3312 is reported to be fixed in it).

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:72

The simplest code i've found that triggers it:

kk : ∀ {ℓ} → Set ℓ
kk = {!∀ B → B!}

Both C-c C-r and C-c C-space trigger this. C-c C-. shows Have: piSort (univSort _8) (λ B → _8)

Removing ℓ or specifying B type is enough to avoid issue.

[gallais]

Same as #3312: it looks like it has been fixed in master.