Syntax highlighting of record fields in a parametrised module

[gallais]

I've noticed that if I have a parametrised module with a record type then the record fields are only properly highlighted if it comes last in the telescope of parameters.

record SET : Set₁ where
  field `set : Set

-- extra parameter *after*  the SET one
module Aset (a : SET) (b : Set) where

  module a = SET a

  mySet : Set
  mySet = a.`set -- shows up blue

-- the SET parameter comes last
module Bset (b : Set) (a : SET) where

  module a = SET a

  mySet : Set
  mySet = a.`set -- shows up pink

[andreasabel]

Doesn't come as a suprise to me. In the second case, you can eta-contract the function a.set to a projection, but not in the first case.

Possibly related: #1581 and #3010.

[UlfNorell]

This is exactly #1581 and unrelated to #3010.

[andreasabel]

2025-11-17 still open.