Parameterised datatype as a module parameter?

Question

In Agda, how can I define a parameterised module equivalent to the following?

data Sig : Set ℓ where
  ■ : Sort → Sig
  ν : Sig → Sig

module SortedABT {ℓ} (Sort : Set ℓ) (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List Sig) where

Of course the above doesn't work because ℓ and Sort appear in the definition of Sig, but are parameters of the module, so not yet defined where they appear. I've looked at the Agda manual and tried various web searches, but not found a workaround. Help, please!

Answer 1

Not sure what kind of UX you're looking for, but you could try

module _ {ℓ} (Sort : Set ℓ) where

  data Sig : Set ℓ where
    ■ : Sort → Sig
    ν : Sig → Sig

  module SortedABT (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List Sig) where

That adds

Sig : ∀ {ℓ} (Sort : Set ℓ) → Set ℓ

to the current scope together with the expected SortedABT.

Alternatively you may want to give the outer module a name like this:

module SigAndStuff {ℓ} (Sort : Set ℓ) where

so that it always needs to be opened explicitly at a specific Sort, e.g.

open SigAndStuff ⊤

which adds

Sig : Set

to the current scope as well as your original SortedABT instantiated like this:

SortedABT {zero} {⊤}

Answer 2

Another answer was provided by Naïm Camille Favier on the Agda Zulip.

data Sig {ℓ} (Sort : Set ℓ) : Set ℓ where
  ■ : Sort → Sig Sort
  ν : Sig Sort → Sig Sort

module SortedABT {ℓ} (Sort : Set ℓ) (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List (Sig Sort)) where
...