Agda: Internal error for local modules with refined parameters

[UlfNorell]

module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

module M (n : Nat) (m : Nat) where

  foo : n ≡ 0 → Nat
  foo refl = 0
    module M' where
      bar : Nat
      bar = m

  bad : Nat
  bad = M'.bar -- internal error Monad.Signature:882

The local module M' just has the m parameter since n has been refined. This causes problems when we exit the scope of M'.

[UlfNorell]

You can also prove false:

module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data ⊥ : Set where

T : Nat → Set
T zero    = ⊥
T (suc n) = Nat

module M (n : Nat) where

  foo : n ≡ 0 → T n → Nat
  foo refl t = 0
    module M' where
      bar : ⊥
      bar = t

  bad : ⊥
  bad = M'.bar

loop : ⊥
loop = M.bad 0

[UlfNorell]

There might be a story on inverting the module parameter substitution that makes sense of this example, but I think the best fix for now is to disallow named where modules if the module parameters have been refined.

[nad]

Are you sure that anonymous where modules are unaffected by this kind of problem?

[UlfNorell]

Reasonably sure. The module parameter substitution is only used to insert the module parameter arguments when the user explicitly references a name. Since you can't reference definitions from anonymous where modules it wouldn't be a problem.