"Multiple fixity declarations" errors

[RyanGlScott]

I discovered this when investigating #160. This is reproducble with singletons-2.3 or HEAD:

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

import Data.Singletons.TH

$(singletons [d|
  infixl 5 $$:
  ($$:) :: Bool -> Bool -> Bool
  _ $$: _ = False
 |])

$ /opt/ghc/8.2.1/bin/runghc -ddump-splices Bug.hs
Bug.hs:(12,3)-(16,3): Splicing declarations
    singletons
      [d| infixl 5 $$:_a3AU

          ($$:_a3AU) :: Bool -> Bool -> Bool
          _ $$:_a3AU _ = False |]
  ======>
    infixl 5 $$:_a6jG
    ($$:_a6jG) :: Bool -> Bool -> Bool
    ($$:_a6jG) _ _ = False
    type ($$:$$$) (t_a6jH :: Bool) (t_a6jI :: Bool) =
        ($$:) t_a6jH t_a6jI
    instance SuppressUnusedWarnings ($$:$$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:$$:$$###)) GHC.Tuple.())
    data ($$:$$) (l_a6jK :: Bool) (l_a6jJ :: TyFun Bool Bool)
      = forall arg_a6jL. SameKind (Apply (($$:$$) l_a6jK) arg_a6jL) (($$:$$$) l_a6jK arg_a6jL) =>
        (:$$:$$###)
    type instance Apply (($$:$$) l_a6jK) l_a6jJ = ($$:) l_a6jK l_a6jJ
    instance SuppressUnusedWarnings ($$:$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:$$:$###)) GHC.Tuple.())
    data ($$:$) (l_a6jM :: TyFun Bool (TyFun Bool Bool
                                       -> GHC.Types.Type))
      = forall arg_a6jN. SameKind (Apply ($$:$) arg_a6jN) (($$:$$) arg_a6jN) =>
        (:$$:$###)
    type instance Apply ($$:$) l_a6jM = ($$:$$) l_a6jM
    type family ($$:) (a_a6jO :: Bool) (a_a6jP :: Bool) :: Bool where
      ($$:) _z_6989586621679034086_a6jS _z_6989586621679034089_a6jV = FalseSym0
    infixl 5 $$:
    infixl 5 %$$:
    (%$$:) ::
      forall (t_a6jW :: Bool) (t_a6jX :: Bool).
      Sing t_a6jW
      -> Sing t_a6jX -> Sing (Apply (Apply ($$:$) t_a6jW) t_a6jX :: Bool)
    (%$$:) _ _ = SFalse

Bug.hs:12:3: error:
    Multiple fixity declarations for ‘$$:_a6jG’
    also at  Bug.hs:(12,3)-(16,3)
   |
12 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

[RyanGlScott]

Another way you can trigger this error is through this program:

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

import Data.Kind
import Data.Singletons.TH

$(singletons [d|
    infixr 6 :*:
    data (a :: Type) :*: (b :: Type) = a :*: b
  |])

$ /opt/ghc/8.2.1/bin/runghc -ddump-splices Bug.hs
Bug.hs:(13,3)-(16,4): Splicing declarations
    singletons
      [d| infixr 6 :*:_a3B5, :*:_a3B4

          data (a_a3B6 :: Type) :*:_a3B4 (b_a3B7 :: Type)
            = a_a3B6 :*:_a3B5 b_a3B7 |]
  ======>
    infixr 6 :*:_a6l8
    infixr 6 :*:_a6l7
    data (:*:_a6l7) (a_a6l9 :: Type) (b_a6la :: Type)
      = a_a6l9 :*:_a6l8 b_a6la
    type (:*:$$$) (t_a6ld :: a6989586621679034167) (t_a6le :: b6989586621679034168) =
        (:*:_a6l8) t_a6ld t_a6le
    instance SuppressUnusedWarnings (:*:$$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:*:$$###)) GHC.Tuple.())
    data (:*:$$) (l_a6lg :: a6989586621679034167) (l_a6lf :: TyFun b6989586621679034168 ((:*:_a6l7) a6989586621679034167 b6989586621679034168))
      = forall arg_a6lh. SameKind (Apply ((:*:$$) l_a6lg) arg_a6lh) ((:*:$$$) l_a6lg arg_a6lh) =>
        (:*:$$###)
    type instance Apply ((:*:$$) l_a6lg) l_a6lf = (:*:_a6l8) l_a6lg l_a6lf
    instance SuppressUnusedWarnings (:*:$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:*:$###)) GHC.Tuple.())
    data (:*:$) (l_a6li :: TyFun a6989586621679034167 (TyFun b6989586621679034168 ((:*:_a6l7) a6989586621679034167 b6989586621679034168)
                                                       -> Type))
      = forall arg_a6lj. SameKind (Apply (:*:$) arg_a6lj) ((:*:$$) arg_a6lj) =>
        (:*:$###)
    type instance Apply (:*:$) l_a6li = (:*:$$) l_a6li
    infixr 6 :%*:
    infixr 6 :%*:
    data instance Sing (z_a6lk :: (:*:_a6l7) a_a6l9 b_a6la)
      = forall (n_a6ll :: a_a6l9)
               (n_a6lm :: b_a6la). z_a6lk ~ (:*:_a6l8) n_a6ll n_a6lm =>
        (:%*:) (Sing (n_a6ll :: a_a6l9)) (Sing (n_a6lm :: b_a6la))
    type :%*: = (Sing :: (:*:_a6l7) a_a6l9 b_a6la -> Type)
    instance (SingKind a_a6l9, SingKind b_a6la) =>
             SingKind ((:*:_a6l7) a_a6l9 b_a6la) where
      type Demote ((:*:_a6l7) a_a6l9 b_a6la) = (:*:_a6l7) (Demote a_a6l9) (Demote b_a6la)
      fromSing ((:%*:) b_a6ln b_a6lo)
        = ((:*:_a6l8) (fromSing b_a6ln)) (fromSing b_a6lo)
      toSing ((:*:_a6l8) b_a6lp b_a6lq)
        = case
              (GHC.Tuple.(,) (toSing b_a6lp :: SomeSing a_a6l9))
                (toSing b_a6lq :: SomeSing b_a6la)
          of {
            GHC.Tuple.(,) (SomeSing c_a6lr) (SomeSing c_a6ls)
              -> SomeSing (((:%*:) c_a6lr) c_a6ls) }
    instance (SingI n_a6ll, SingI n_a6lm) =>
             SingI ((:*:_a6l8) (n_a6ll :: a_a6l9) (n_a6lm :: b_a6la)) where
      sing = ((:%*:) sing) sing

Bug.hs:13:3: error:
    Multiple fixity declarations for ‘:%*:’
    also at  Bug.hs:(13,3)-(16,4)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

Bug.hs:13:3: error:
    Multiple fixity declarations for ‘:*:_a6l8’
    also at  Bug.hs:(13,3)-(16,4)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

[RyanGlScott]

Note that the bug in https://github.com/goldfirere/singletons/issues/197#issue-235752688 does not happen for other infix functions. For example, these work:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Works where

import Data.Kind
import Data.Singletons.TH

$(singletons [d|
    infixl 5 <>:, `infixFun`
    (<>:), infixFun :: Bool -> Bool -> Bool
    _ <>: _ = False
    _ `infixFun` _ = True
  |])

However, for the example in https://github.com/goldfirere/singletons/issues/197#issuecomment-308475645, that sort of thing appears to fail for all datatypes with identically named constructors that have fixity declarations, since this fails as well:

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

import Data.Kind
import Data.Singletons.TH

$(singletons [d|
    infixr 6 `Prefix`
    data Prefix (a :: Type) (b :: Type) = Prefix a b
  |])

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170523: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:13:3: error:
    Multiple fixity declarations for ‘SPrefix’
    also at  Bug.hs:(13,3)-(16,4)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

Bug.hs:13:3: error:
    Multiple fixity declarations for ‘Prefix_a6o9’
    also at  Bug.hs:(13,3)-(16,4)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

[RyanGlScott]

After some digging, here's what I've uncovered.

The former bug appears to be related to #29 (see also my comment in https://github.com/goldfirere/singletons/issues/160#issuecomment-308519043). Because we don't prepend function names that begin with a $ with a colon when promoting them, we accidentally create a promoted fixity declaration for ($$:) that clashes with the value-level fixity declaration for ($$:). I suppose a serviceable workaround for this issue would be to avoid creating promoted fixity declarations for things that begin with $.

The latter bug is nastier, and I think there might be one or two GHC bugs making it worse. First, observe what happens when you try to quasiquote a fixity declaration for something that's used in both the type and constructor namespace (example from Trac #13799):

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where

$([d| infixr 5 :*:
      data a :*: b = a :*: b
    |])

$ /opt/ghc/8.2.1/bin/runghc Bug.hs
Bug.hs:(6,3)-(8,6): Splicing declarations
    [d| infixr 5 :*:_a1pB, :*:_a1pA

        data a_a1pC :*:_a1pA b_a1pD = a_a1pC :*:_a1pB b_a1pD |]
  ======>
    infixr 5 :*:_a4aj
    infixr 5 :*:_a4ai
    data (:*:_a4ai) a_a4ak b_a4al = a_a4ak :*:_a4aj b_a4al

Bug.hs:6:3: error:
    Multiple fixity declarations for ‘:*:_a4aj’
    also at  Bug.hs:(6,3)-(8,6)
  |
6 | $([d| infixr 5 :*:
  |   ^^^^^^^^^^^^^^^^...

Internally, it seems that GHC is creating two newName-d copies of :*:. The Multiple fixity declarations for ‘:*:_xxxx’ error is thus a consequence of Trac #13054, and the Multiple fixity declarations for ‘:%*:’ error happens because we naïvely single both fixity declarations for :*: to :%*:. Yuck.

[goldfirere]

Yes, the special-case for $ is atrocious. Instead, perhaps all defunctionalization symbols of symbolic identifiers should have something like @#$%^%$#@ placed before the $$$... suffix to avoid name clashes and the special case for $.

I'm not convinced that GHC's mishandling of infix declarations is to blame here, though. Note that the output in your last comment is not due to newName but just the fact that the term-level and type-level namespaces are distinct.

[RyanGlScott]

Yes, the special-case for $ is atrocious. Instead, perhaps all defunctionalization symbols of symbolic identifiers should have something like @#$%^%$#@ placed before the $$$... suffix to avoid name clashes and the special case for $.

That does sound like it would have much lower rate of collisions, yes.

I'm not convinced that GHC's mishandling of infix declarations is to blame here, though. Note that the output in your last comment is not due to newName but just the fact that the term-level and type-level namespaces are distinct.

Right, in theory having two different :*: identifiers (one term-level one, and one type-level one) shouldn't be a problem. But in practice it is, which is the nub of Trac #13054. So in order to promote that program, we're going to have to cleverly work around that bug somehow.

[RyanGlScott]

The former bug (the one in https://github.com/goldfirere/singletons/issues/197#issue-235752688) was fixed in #199 (and later obsoleted by #203). So all that's left here is to address the bug in https://github.com/goldfirere/singletons/issues/197#issuecomment-308475645. We can't fix the problem that GHC Trac #13799 induces yet, but we can at least avoid generating duplicate fixity declarations for promoted/singled infix names.

[RyanGlScott]

Actually, I'm going to claim that #200 fixes the issue in https://github.com/goldfirere/singletons/issues/197#issuecomment-308475645 too. Why? Because with the changes in #200, we'll generate two singled names for data a :*: b = a :*: b:

• %:*: (for the datatype name)
• :%*: (for the constructor name)

So we needn't worry ourselves with generating duplicate fixity declarations.

There's still the issue that you can't actually give a fixity declaration for :*: due to GHC Trac #13799, but that's solely GHC's fault.

[RyanGlScott]

Bah, I spoke too soon. There's exactly one scenario where singletons will still generate duplicate fixity declarations, even after #200: when you have a datatype and constructor with the same, prefix name:

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

import Data.Singletons.TH

$(singletons [d|
    infixr 6 `Pair`
    data a `Pair` b = a `Pair` b
  |])

This generates duplicate fixity declarations:

    infixr 6 `SPair`
    infixr 6 `SPair`

So this is something that needs to be fixed on singletons' side.

[RyanGlScott]

Oops, my comment in https://github.com/goldfirere/singletons/issues/197#issuecomment-315395657 was misleading. The reason that two SPair fixity declarations are being generated is not the fault of singletons, but rather GHC Trac #14032, which causes duplicate fixity declarations to be produced during renaming (and then singletons then singles both of them, leading to shenanigans).

If that ticket were fixed, then this whole issue would go away. In light of this, I'll close this ticket, as this is squarely a GHC issue, and fixing that issue will make this one go away as well.