Constructor instances do not work outside parameterised modules

[omelkonian]

Let's assume two files with the following definitions:

open import Agda.Builtin.Unit
module File1 (_ : ⊤) where

it : ∀ {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x

data X : Set where
  instance x : X

_ : X
_ = it

--------------------------------------------

open import Agda.Builtin.Unit
module File2 where

open import File1 tt

_ : X
_ = it

The instance is not available in File2, producing the following error:

No instance of type Y was found in scope.
when checking that the expression it has type Y

NB: If I remove the dummy parameter _ : ⊤ it works, and it was working before v2.6.2.

[omelkonian]

Also, the issue does not appear when everything is in one file:

module M₁ (_ : ⊤) where

  data X : Set where
    instance x : X

  _ : X
  _ = it

module M₂ where

  open M₁ tt

  _ : X
  _ = it

[gallais]

import File1
open File1 tt

works but not open import File1 tt 👀

[omelkonian]

Then probably related to #4166.

[jespercockx]

Isn't the problem that instance search simply does not consider instances that have explicit arguments? Normally there's a warning for that but in this case it (intentionally or unintentionally) does not fire because the argument is a module parameter.

[jespercockx]

Nevermind, I see the module is actually applied to tt in your example so it should definitely work.