[Agda] Internal error at src/full/Agda/TypeChecking/Substitute.hs:144

[Helmut Grohne]

Dear Agda developers,

While refactoring some Agda code I ran into the following error message:

| Checking Error (../full/path/to/Error.agda).
| An internal error has occurred. Please report this as a bug.
| Location of the error: src/full/Agda/TypeChecking/Substitute.hs:144

This is produced using Agda 2.4.2 as obtained using cabal on a Linux
amd64 system with GHC 7.6.3.

I went ahead and tried to find a reproducer with less than 1000 lines.
After feeding Agda 30000 samples, I came up with the following 7 lines:

data A (B : Set) : Set where
module C where
  record D : Set where
module E (F : Set) (G : A F) where
  open C public using (module D)
module H (I : Set) (J : A I) where
  open E I J using ()

Is this also reproducible on the development version of Agda?

Helmut