Support promoting/singling namespace specifiers in fixity declarations

[RyanGlScott]

GHC 9.10.1 adds support for namespaces in fixity declarations, e.g.,

$(singletons
  [d| infixl 4 data `f`
      f :: a -> a -> a
    |])

It would be nice if singletons-th could take these into account during promotion and singling. In particular, we could promote f to:

-- Promoted type-level declaration
infixl 4 type `F`
type F :: a -> a -> a
-- Defunctionalization symbols
infixl 4 type `FSym0`
infixl 4 type `FSym1`

And we could single f to:

infixl 4 data `sF`
sF :: forall a (x :: a) (y :: a). Sing x -> Sing y -> Sing (F x y)

Some wrinkles to this plan:

• What happens if we promote or single a quoted type-level declaration, such as this one?

  $(singletons
    [d| infixl 4 type `G`
        type G :: a -> a -> a
      |])

  In that case, we would simply return the original fixity declaration unchanged (including the type specifier).

• In the event that a fixity declaration lacks an explicit namespace specifier, I propose that we promote/single it to something that does have an explicit namespace specifier. To see why, consider this example:

  $(singletons
    [d| infixl 4 ###
        (###) :: a -> a -> a
      |])

  We must not promote this to the following:

  infixl 4 ###
  type (###) :: a -> a -> a

  If we did, there would be two clashing fixity declarations for (###): one for the name in the data namespace, and another for the name in the type namespace. We should instead promote (###) to the following to avoid the risk of name clashes:

  infixl 4 type ###
  type (###) :: a -> a -> a

  If we did this, then we can remove a hack from singletons-th that is described in Wrinkle 1: When not to promote/single fixity declarations of Note [singletons-th and fixity declarations].

[goldfirere]

What's the reason to put fixity on defunctionalization symbols? Their arity generally differs from the original construct (and so their infix usage is likely quite different-looking). And programmatically generated uses won't care about the fixity.

Otherwise, this sounds great to me.

[RyanGlScott]

See Note [Fixity declarations for defunctionalization symbols].

[goldfirere]

Ah right. Thanks!