:. and :! aren't assigned fixity declarations

[RyanGlScott]

To see what I mean, observe that the following program fails to typecheck:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Singletons.Prelude
import Data.Singletons.TH

$(singletons [d|
  (!) :: Bool -> Bool -> Bool
  (!) = (||)
  infixr 2 !
  |])

f1 :: (False && True :! True) :~: True
f1 = Refl

$ ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:20:6: error:
    • Couldn't match type ‘'True’ with ‘'False’
      Expected type: ('False && ('True :! 'True)) :~: 'True
        Actual type: 'True :~: 'True
    • In the expression: Refl
      In an equation for ‘f1’: f1 = Refl
   |
20 | f1 = Refl
   |      ^^^^

It ought to, though, since we declared the the fixity of (!) (and thus (:!)) to be infixr 2, so False && True :! True should associate as (False && True) :! True. However, it appears that in practice, (:!) isn't given a fixity declaration, so that expression actually associates as False && (True :! True).

Indeed, searching through the -ddump-splices output reveals no fixity declaration for (:!). (There is one for (%!), however.)

The same problem also affects (.), which promotes to (:.).

[RyanGlScott]

Ugh, it turns out that I'm the one who caused these shenanigans. The culprit is here:

singletons/src/Data/Singletons/Promote.hs

Lines 534 to 539 in 47a62de

	promoteInfixDecl :: Fixity -> Name -> Maybe DDec
	promoteInfixDecl fixity name
	| isDataConName name || not (isHsLetter (head (nameBase name)))
	= Nothing -- No need to promote fixity declarations for constructor names or
	-- infix names, as those fixity declarations apply to both
	-- the value and type namespaces.

Here, I boldly claim that no non-alphanumeric identifiers need to have their fixity declarations promoted, since their promoted names as the same as their unpromoted ones. However, there are exactly two exceptions to this rule: (.) and (!), as it turns out.

Fix incoming.

[RyanGlScott]

Fixed in f13482a.

Note that I didn't add a test case for (.) since it proves to be trickier than you'd expect. See #323.