[Agda] Instance arguments for parametrized modules

[Guillaume Brunerie]

Hello,

Are instance arguments supposed to work as arguments of parametrized modules?
I’m asking because I just had a bug saying

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

I was trying to find a minimal example, but I got another error
instead which also looks like a bug in Agda.
The code for the second error is

> module Bug where
>
> record unit : Set where
>   constructor tt
>
> module A ⦃ t : unit ⦄ (i : unit) where
>   id : unit → unit
>   id x = x
>
> open A tt

And the error message is

> Panic: Unbound name: Bug._.id [0,8,9]@69078460
> when checking that tt are valid arguments to a function of type
> {{t : unit}} → unit → Prop



Also another problem is that it does not seem possible to specify
explicitely instance arguments of modules. In the previous example, if
I replace

> open A tt

by

> open A ⦃ tt ⦄ tt

I now get the following error message:

> {{tt}} cannot appear by itself. It needs to be the argument to a
> function expecting an instance argument.
> when scope checking {{tt}}


Thanks,

Guillaume

PS : I’m using Agda 2.3.1 compiled a few weeks ago