[Agda] Infix in Modules with Parameters

[Philip Wadler]

Consider the following simple variant of an example in the user manual.

---

open import Data.List using (List; _∷_; [])
open import Data.Bool using (Bool; true; false)

module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where

  infix 1 _≤_
  infix 2 _⊝_

  insert : A → List A → List A
  insert x [] = x ∷ []
  insert x (y ∷ ys) with zero ≤ (y ⊝ x)
  insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
  insert x (y ∷ ys)    | false = y ∷ insert x ys

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

---

This works fine. But now say I add infix declarations in so I can omit
parentheses.

---

open import Data.List using (List; _∷_; [])
open import Data.Bool using (Bool; true; false)

module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where

  infix 1 _≤_
  infix 2 _⊝_

  insert : A → List A → List A
  insert x [] = x ∷ []
  insert x (y ∷ ys) with zero ≤ (y ⊝ x)
  insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
  insert x (y ∷ ys)    | false = y ∷ insert x ys

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

---

This yields the error message:

/Users/wadler/sf/src/extra/ModuleInfix.agda:8,11-14
> The following names are not declared in the same scope as their
> syntax or fixity declaration (i.e., either not in scope at all,
> imported from another module, or declared in a super module): _≤_
> _⊝_
> when scope checking the declaration
>   module Sort (A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)
>               (zero : A) where


Moving the infix declarations before the module yields a similar error
message.

1. What is the right way to declare fixity of infix parameters to a module?
2. Where is this documented?

Cheers, -- P




.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180418/6064dc6c/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180418/6064dc6c/attachment.ksh>