Use explicit namespace specifiers when promoting/singling fixity decl…

…arations

During promotion, we now give promoted fixity declarations the `type`
namespace, and during singling, we now give singled fixity declarations the
`type` namespace (if it is a singled class declaration) or the `data` namesapce
(for all other singled names). Doing so makes our intentions clearer, and it
also future-proofs the code against planned GHC changes discussed in [GHC
proposal
65](https://github.com/ghc-proposals/ghc-proposals/blob/8443acc903437cef1a7fbb56de79b6dce77b1a09/proposals/0065-type-infix.rst#migration-plan),
where specifier-less fixity declarations (e.g., `infixl 4 %%%`) will become an
error if they refer to both a term-level and type-level `%%%` name.

We now also take namespace specifiers into account when promoting fixity
declarations. This is because `Wrinkle 1: When not to promote/single fixity
declarations` in `Note [singletons-th and fixity declarations]` describes a
special case where we must avoid promoting fixity declarations for infix names,
but this workaround only needs to be used if the fixity declaration lacks an
explicit namespace specifier. If it _does_ have an explicit namespace specifier
(e.g., `infixl 4 data %%%`), then we can promote it (e.g., to `infixl 4 type
%%%`) without fear of name clashes.

Fixes #582.

README.md

@@ -811,6 +811,7 @@ The following constructs are fully supported:
 * constructors
 * if statements
 * infix expressions and types
+* fixity declarations for infix expressions and types
 * `_` patterns
 * aliased patterns
 * lists (including list comprehensions)
@@ -1540,7 +1541,6 @@ The following constructs are either unsupported or almost never work:
 * Irrefutable patterns
 * `{-# UNPACK #-}` pragmas
 * partial application of the `(->)` type
-* namespace specifiers in fixity declarations
 * invisible type patterns
 
 See the following sections for more details.
@@ -1728,19 +1728,6 @@ arguments. Attempting to promote `(->)` to zero or one argument will result in
 an error. As a consequence, it is impossible to promote instances like the
 `Functor ((->) r)` instance, so `singletons-base` does not provide them.
 
-### Namespace specifiers in fixity declarations
-
-`singletons-th` will currently ignore namespace specifiers attached to fixity
-declarations. For instance, if you attempt to promote this:
-
-```hs
-infixl 4 data `f`
-f :: a -> a -> a
-```
-
-Then it will be the same as if you had written `` infixl 4 `f` ``. See [this
-`singletons` issue](https://github.com/goldfirere/singletons/issues/582).
-
 ### Invisible type patterns
 
 `singletons-th` currently does not support invisible type patterns, such as the

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -153,6 +153,7 @@ tests =
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
     , compileAndDumpStdTest "T581"
+    , compileAndDumpStdTest "T582"
     , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
     , compileAndDumpStdTest "T589"

singletons-base/tests/compile-and-dump/Singletons/T582.golden

@@ -0,0 +1,151 @@
+Singletons/T582.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| infixl 4 !!!
+          infixl 4 %%%
+          infixl 4 `Bar`
+          infixl 4 `foo`
+
+          foo :: a -> a -> a
+          x `foo` _ = x
+          (%%%) :: a -> a -> a
+          x %%% _ = x
+
+          type Bar :: a -> a -> a
+          type (!!!) :: a -> a -> a
+
+          type x `Bar` y = x
+          type x !!! y = x |]
+  ======>
+    infixl 4 `foo`
+    foo :: a -> a -> a
+    foo x _ = x
+    infixl 4 `Bar`
+    type Bar :: a -> a -> a
+    type Bar x y = x
+    infixl 4 %%%
+    (%%%) :: a -> a -> a
+    (%%%) x _ = x
+    infixl 4 !!!
+    type (!!!) :: a -> a -> a
+    type (!!!) x y = x
+    type BarSym0 :: (~>) a ((~>) a a)
+    data BarSym0 :: (~>) a ((~>) a a)
+      where
+        BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
+                                BarSym0 a0123456789876543210
+    type instance Apply BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210
+    instance SuppressUnusedWarnings BarSym0 where
+      suppressUnusedWarnings = snd ((,) BarSym0KindInference ())
+    infixl 4 `BarSym0`
+    type BarSym1 :: a -> (~>) a a
+    data BarSym1 (a0123456789876543210 :: a) :: (~>) a a
+      where
+        BarSym1KindInference :: SameKind (Apply (BarSym1 a0123456789876543210) arg) (BarSym2 a0123456789876543210 arg) =>
+                                BarSym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (BarSym1 a0123456789876543210) a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (BarSym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) BarSym1KindInference ())
+    infixl 4 `BarSym1`
+    type BarSym2 :: a -> a -> a
+    type family BarSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+      BarSym2 a0123456789876543210 a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210
+    infixl 4 `BarSym2`
+    type (!!!@#@$) :: (~>) a ((~>) a a)
+    data (!!!@#@$) :: (~>) a ((~>) a a)
+      where
+        (:!!!@#@$###) :: SameKind (Apply (!!!@#@$) arg) ((!!!@#@$$) arg) =>
+                         (!!!@#@$) a0123456789876543210
+    type instance Apply (!!!@#@$) a0123456789876543210 = (!!!@#@$$) a0123456789876543210
+    instance SuppressUnusedWarnings (!!!@#@$) where
+      suppressUnusedWarnings = snd ((,) (:!!!@#@$###) ())
+    infixl 4 !!!@#@$
+    type (!!!@#@$$) :: a -> (~>) a a
+    data (!!!@#@$$) (a0123456789876543210 :: a) :: (~>) a a
+      where
+        (:!!!@#@$$###) :: SameKind (Apply ((!!!@#@$$) a0123456789876543210) arg) ((!!!@#@$$$) a0123456789876543210 arg) =>
+                          (!!!@#@$$) a0123456789876543210 a0123456789876543210
+    type instance Apply ((!!!@#@$$) a0123456789876543210) a0123456789876543210 = (!!!) a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings ((!!!@#@$$) a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) (:!!!@#@$$###) ())
+    infixl 4 !!!@#@$$
+    type (!!!@#@$$$) :: a -> a -> a
+    type family (!!!@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+      (!!!@#@$$$) a0123456789876543210 a0123456789876543210 = (!!!) a0123456789876543210 a0123456789876543210
+    infixl 4 !!!@#@$$$
+    type (%%%@#@$) :: (~>) a ((~>) a a)
+    data (%%%@#@$) :: (~>) a ((~>) a a)
+      where
+        (:%%%@#@$###) :: SameKind (Apply (%%%@#@$) arg) ((%%%@#@$$) arg) =>
+                         (%%%@#@$) a0123456789876543210
+    type instance Apply (%%%@#@$) a0123456789876543210 = (%%%@#@$$) a0123456789876543210
+    instance SuppressUnusedWarnings (%%%@#@$) where
+      suppressUnusedWarnings = snd ((,) (:%%%@#@$###) ())
+    infixl 4 %%%@#@$
+    type (%%%@#@$$) :: a -> (~>) a a
+    data (%%%@#@$$) (a0123456789876543210 :: a) :: (~>) a a
+      where
+        (:%%%@#@$$###) :: SameKind (Apply ((%%%@#@$$) a0123456789876543210) arg) ((%%%@#@$$$) a0123456789876543210 arg) =>
+                          (%%%@#@$$) a0123456789876543210 a0123456789876543210
+    type instance Apply ((%%%@#@$$) a0123456789876543210) a0123456789876543210 = (%%%) a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings ((%%%@#@$$) a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) (:%%%@#@$$###) ())
+    infixl 4 %%%@#@$$
+    type (%%%@#@$$$) :: a -> a -> a
+    type family (%%%@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+      (%%%@#@$$$) a0123456789876543210 a0123456789876543210 = (%%%) a0123456789876543210 a0123456789876543210
+    infixl 4 %%%@#@$$$
+    type FooSym0 :: (~>) a ((~>) a a)
+    data FooSym0 :: (~>) a ((~>) a a)
+      where
+        FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
+                                FooSym0 a0123456789876543210
+    type instance Apply FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
+    instance SuppressUnusedWarnings FooSym0 where
+      suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
+    infixl 4 `FooSym0`
+    type FooSym1 :: a -> (~>) a a
+    data FooSym1 (a0123456789876543210 :: a) :: (~>) a a
+      where
+        FooSym1KindInference :: SameKind (Apply (FooSym1 a0123456789876543210) arg) (FooSym2 a0123456789876543210 arg) =>
+                                FooSym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (FooSym1 a0123456789876543210) a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (FooSym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) FooSym1KindInference ())
+    infixl 4 `FooSym1`
+    type FooSym2 :: a -> a -> a
+    type family FooSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+      FooSym2 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210
+    infixl 4 `FooSym2`
+    type (%%%) :: a -> a -> a
+    type family (%%%) @a (a :: a) (a :: a) :: a where
+      (%%%) x _ = x
+    type Foo :: a -> a -> a
+    type family Foo @a (a :: a) (a :: a) :: a where
+      Foo x _ = x
+    infixl 4 %%%
+    infixl 4 `Foo`
+    infixl 4 %%%%
+    infixl 4 `sFoo`
+    (%%%%) ::
+      (forall (t :: a) (t :: a).
+       Sing t
+       -> Sing t -> Sing (Apply (Apply (%%%@#@$) t) t :: a) :: Type)
+    sFoo ::
+      (forall (t :: a) (t :: a).
+       Sing t -> Sing t -> Sing (Apply (Apply FooSym0 t) t :: a) :: Type)
+    (%%%%) (sX :: Sing x) _ = sX
+    sFoo (sX :: Sing x) _ = sX
+    instance SingI ((%%%@#@$) :: (~>) a ((~>) a a)) where
+      sing = singFun2 @(%%%@#@$) (%%%%)
+    instance SingI d => SingI ((%%%@#@$$) (d :: a) :: (~>) a a) where
+      sing = singFun1 @((%%%@#@$$) (d :: a)) ((%%%%) (sing @d))
+    instance SingI1 ((%%%@#@$$) :: a -> (~>) a a) where
+      liftSing (s :: Sing (d :: a))
+        = singFun1 @((%%%@#@$$) (d :: a)) ((%%%%) s)
+    instance SingI (FooSym0 :: (~>) a ((~>) a a)) where
+      sing = singFun2 @FooSym0 sFoo
+    instance SingI d => SingI (FooSym1 (d :: a) :: (~>) a a) where
+      sing = singFun1 @(FooSym1 (d :: a)) (sFoo (sing @d))
+    instance SingI1 (FooSym1 :: a -> (~>) a a) where
+      liftSing (s :: Sing (d :: a))
+        = singFun1 @(FooSym1 (d :: a)) (sFoo s)

singletons-base/tests/compile-and-dump/Singletons/T582.hs

@@ -0,0 +1,21 @@
+module T582 where
+
+import Data.Singletons.TH
+
+$(singletons [d|
+  infixl 4 data `foo`
+  foo :: a -> a -> a
+  x `foo` _ = x
+
+  infixl 4 type `Bar`
+  type Bar :: a -> a -> a
+  type x `Bar` y = x
+
+  infixl 4 data %%%
+  (%%%) :: a -> a -> a
+  x %%% _ = x
+
+  infixl 4 type !!!
+  type (!!!) :: a -> a -> a
+  type x !!! y = x
+  |])

singletons-th/src/Data/Singletons/TH/Partition.hs

@@ -163,8 +163,8 @@ partitionClassDec (DLetDec (DValD (DVarP name) exp)) =
   pure (valueBinding name (UValue exp), mempty)
 partitionClassDec (DLetDec (DFunD name clauses)) =
   pure (valueBinding name (UFunction clauses), mempty)
-partitionClassDec (DLetDec (DInfixD fixity _ name)) =
-  pure (infixDecl fixity name, mempty)
+partitionClassDec (DLetDec (DInfixD fixity ns name)) =
+  pure (infixDecl fixity ns name, mempty)
 partitionClassDec (DLetDec (DPragmaD {})) =
   pure (mempty, mempty)
 partitionClassDec (DOpenTypeFamilyD tf_head) =

singletons-th/src/Data/Singletons/TH/Promote.hs

@@ -293,7 +293,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name
     <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvb_names) defaults_list
   defunAssociatedTypeFamilies orig_cls_tvbs atfs
 
-  infix_decls' <- mapMaybeM (uncurry (promoteInfixDecl Nothing)) $
+  infix_decls' <- mapMaybeM (\(n, (f, ns)) -> promoteInfixDecl Nothing n f ns) $
                   OMap.assocs infix_decls
   cls_infix_decls <- promoteReifiedInfixDecls $ cls_name:meth_names
 
@@ -830,14 +830,14 @@ promoteLetDecEnv :: Maybe Uniq -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)
 promoteLetDecEnv mb_let_uniq (LetDecEnv { lde_defns = value_env
                                         , lde_types = type_env
                                         , lde_infix = fix_env }) = do
-  infix_decls <- mapMaybeM (uncurry (promoteInfixDecl mb_let_uniq)) $
+  infix_decls <- mapMaybeM (\(n, (f, ns)) -> promoteInfixDecl mb_let_uniq n f ns) $
                  OMap.assocs fix_env
 
     -- promote all the declarations, producing annotated declarations
   let (names, rhss) = unzip $ OMap.assocs value_env
   (pro_decs, defun_decss, ann_rhss)
     <- fmap unzip3 $
-       zipWithM (promoteLetDecRHS LetBindingRHS type_env fix_env mb_let_uniq)
+       zipWithM (promoteLetDecRHS LetBindingRHS type_env (fmap fst fix_env) mb_let_uniq)
                 names rhss
 
   emitDecs $ concat defun_decss
@@ -854,8 +854,15 @@ promoteLetDecEnv mb_let_uniq (LetDecEnv { lde_defns = value_env
 
 -- Promote a fixity declaration.
 promoteInfixDecl :: forall q. OptionsMonad q
-                 => Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
-promoteInfixDecl mb_let_uniq name fixity = do
+                 => Maybe Uniq -> Name -> Fixity
+                 -> NamespaceSpecifier
+                    -- The namespace specifier for the fixity declaration. We
+                    -- only pass this for the sake of checking if we need to
+                    -- avoid promoting a fixity declaration (see `promote_val`
+                    -- below). The actual namespace used in the promoted fixity
+                    -- declaration will always be `type`.
+                 -> q (Maybe DDec)
+promoteInfixDecl mb_let_uniq name fixity ns = do
   opts <- getOptions
   fld_sels <- qIsExtEnabled LangExt.FieldSelectors
   mb_ns <- reifyNameSpace name
@@ -874,9 +881,10 @@ promoteInfixDecl mb_let_uniq name fixity = do
           -> finish $ promotedClassName opts name
         _ -> never_mind
   where
-    -- Produce the fixity declaration.
+    -- Produce the fixity declaration. Promoted names always inhabit the `type`
+    -- namespace (i.e., `TypeNamespaceSpecifier`).
     finish :: Name -> q (Maybe DDec)
-    finish = pure . Just . DLetDec . DInfixD fixity NoNamespaceSpecifier
+    finish = pure . Just . DLetDec . DInfixD fixity TypeNamespaceSpecifier
 
     -- Don't produce a fixity declaration at all. This can happen in the
     -- following circumstances:
@@ -892,16 +900,23 @@ promoteInfixDecl mb_let_uniq name fixity = do
     never_mind = pure Nothing
 
     -- Certain value names do not change when promoted (e.g., infix names).
-    -- Therefore, don't bother promoting their fixity declarations if
-    -- 'genQuotedDecs' is set to 'True', since that will run the risk of
-    -- generating duplicate fixity declarations.
+    -- Therefore, don't bother promoting their fixity declarations if the
+    -- following hold:
+    --
+    -- - 'genQuotedDecs' is set to 'True'.
+    --
+    -- - The name lacks an explicit namespace specifier.
+    --
+    -- Doing so will run the risk of generating duplicate fixity declarations.
     -- See Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1.
     promote_val :: q (Maybe DDec)
     promote_val = do
       opts <- getOptions
       let promoted_name :: Name
           promoted_name = promotedValueName opts name mb_let_uniq
-      if nameBase name == nameBase promoted_name && genQuotedDecs opts
+      if nameBase name == nameBase promoted_name
+         && genQuotedDecs opts
+         && ns == NoNamespaceSpecifier
          then never_mind
          else finish promoted_name
 
@@ -918,7 +933,15 @@ promoteReifiedInfixDecls = mapMaybeM tryPromoteFixityDeclaration
         mFixity <- qReifyFixity name
         case mFixity of
           Nothing     -> pure Nothing
-          Just fixity -> promoteInfixDecl Nothing name fixity
+          -- NB: We don't have a NamespaceSpecifier in hand here. We could try
+          -- to look one up, but it doesn't actually matter which namespace we
+          -- pass here. If we reach this point in the code, we know we have a
+          -- non-quoted Name (as reification would failed earlier if the Name
+          -- were quoted). As such, the special case described in
+          -- [singletons-th and fixity declarations] in D.S.TH.Single.Fixity,
+          -- wrinkle 1 won't apply, and we only pass a namespace specifier for
+          -- the sake of checking this special case.
+          Just fixity -> promoteInfixDecl Nothing name fixity NoNamespaceSpecifier
 
 -- Which sort of let-bound declaration's right-hand side is being promoted?
 data LetDecRHSSort

singletons-th/src/Data/Singletons/TH/Promote/Defun.hs

@@ -445,7 +445,7 @@ defunctionalize name m_fixity defun_ki = do
                            (noExactName <$> qNewName "e")
 
     mk_fix_decl :: Name -> Fixity -> DDec
-    mk_fix_decl n f = DLetDec $ DInfixD f NoNamespaceSpecifier n
+    mk_fix_decl n f = DLetDec $ DInfixD f TypeNamespaceSpecifier n
 
 -- Indicates whether the type being defunctionalized has a standalone kind
 -- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK
@@ -529,10 +529,10 @@ Some things to note:
   to as "fully saturated" defunctionalization symbols.
   See Note [Fully saturated defunctionalization symbols].
 
-* If Foo had a fixity declaration (e.g., infixl 4 `Foo`), then we would also
-  generate fixity declarations for each defunctionalization symbol (e.g.,
-  infixl 4 `FooSym0`).
-  See Note [Fixity declarations for defunctionalization symbols].
+* If Foo had a fixity declaration (e.g., infixl 4 type `Foo`), then we would
+  also generate fixity declarations for each defunctionalization symbol (e.g.,
+  infixl 4 type `FooSym0`). See Note [Fixity declarations for
+  defunctionalization symbols].
 
 * Foo has a vanilla kind signature. (See
   Note [Vanilla-type validity checking during promotion] in D.S.TH.Promote.Type
@@ -883,7 +883,7 @@ following scenario:
 
   (.) :: (b -> c) -> (a -> b) -> (a -> c)
   (f . g) x = f (g x)
-  infixr 9 .
+  infixr 9 data .
 
 One often writes (f . g . h) at the value level, but because (.) is promoted
 to a type family with three arguments, this doesn't directly translate to the
@@ -892,6 +892,6 @@ type level. Instead, one must write this:
   f .@#@$$$ g .@#@$$$ h
 
 But in order to ensure that this associates to the right as expected, one must
-generate an `infixr 9 .@#@#$$$` declaration. This is why defunctionalize accepts
-a Maybe Fixity argument.
+generate an `infixr 9 type .@#@#$$$` declaration. This is why defunctionalize
+accepts a Maybe Fixity argument.
 -}

singletons-th/src/Data/Singletons/TH/Single.hs

@@ -401,7 +401,7 @@ singClassD (ClassDecl { cd_cxt  = cls_cxt
                                                       tyvar_names res_kis
     sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList cxts)))
                        (OMap.assocs default_defns)
-    fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs fixities
+    fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs $ fmap fst fixities
     cls_cxt' <- mapM singPred cls_cxt
     return $ DClassD cls_cxt'
                      sing_cls_name
@@ -519,7 +519,7 @@ singLetDecEnv (LetDecEnv { lde_defns = defns
   let prom_list = OMap.assocs proms
   (typeSigs, letBinds, _tyvarNames, cxts, _res_kis, singIDefunss)
     <- unzip6 <$> mapM (uncurry (singTySig defns types)) prom_list
-  infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs infix_decls
+  infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs $ fmap fst infix_decls
   bindLets letBinds $ do
     let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts)))
                      (OMap.assocs defns)