Skip to content

Commit

Permalink
Use explicit namespace specifiers when promoting/singling fixity decl…
Browse files Browse the repository at this point in the history
…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.
  • Loading branch information
RyanGlScott committed May 31, 2024
1 parent 7e5c92d commit b5ab6dc
Show file tree
Hide file tree
Showing 10 changed files with 276 additions and 73 deletions.
15 changes: 1 addition & 14 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -812,6 +812,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)
Expand Down Expand Up @@ -1506,7 +1507,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.
Expand Down Expand Up @@ -1694,19 +1694,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
Expand Down
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,7 @@ tests =
, compileAndDumpStdTest "T563"
, compileAndDumpStdTest "T567"
, compileAndDumpStdTest "T571"
, compileAndDumpStdTest "T582"
, compileAndDumpStdTest "T585"
, compileAndDumpStdTest "TypeAbstractions"
],
Expand Down
151 changes: 151 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T582.golden
Original file line number Diff line number Diff line change
@@ -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)
21 changes: 21 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T582.hs
Original file line number Diff line number Diff line change
@@ -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
|])
4 changes: 2 additions & 2 deletions singletons-th/src/Data/Singletons/TH/Partition.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
47 changes: 35 additions & 12 deletions singletons-th/src/Data/Singletons/TH/Promote.hs
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name
<- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs) defaults_list
defunAssociatedTypeFamilies 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

Expand Down Expand Up @@ -591,14 +591,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
Expand All @@ -615,8 +615,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
Expand All @@ -635,9 +642,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:
Expand All @@ -653,16 +661,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

Expand All @@ -679,7 +694,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
Expand Down
16 changes: 8 additions & 8 deletions singletons-th/src/Data/Singletons/TH/Promote/Defun.hs
Original file line number Diff line number Diff line change
Expand Up @@ -443,7 +443,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
Expand Down Expand Up @@ -520,10 +520,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
Expand Down Expand Up @@ -834,7 +834,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
Expand All @@ -843,6 +843,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.
-}
4 changes: 2 additions & 2 deletions singletons-th/src/Data/Singletons/TH/Single.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -544,7 +544,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)
Expand Down
Loading

0 comments on commit b5ab6dc

Please sign in to comment.