Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use explicit namespace specifiers when promoting/singling fixity declarations #598

Merged
merged 1 commit into from
Jun 6, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 1 addition & 14 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
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 @@ -153,6 +153,7 @@ tests =
, compileAndDumpStdTest "T567"
, compileAndDumpStdTest "T571"
, compileAndDumpStdTest "T581"
, compileAndDumpStdTest "T582"
, compileAndDumpStdTest "T585"
, compileAndDumpStdTest "TypeAbstractions"
, compileAndDumpStdTest "T589"
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`
Comment on lines +125 to +128
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was surprised to see that these generated fixity declarations seemingly lacked namespace specifiers. Some investigation reveals that the declarations actually do have namespace specifiers, but due to a GHC pretty-printing bug, the namespaces don't get printed in the -ddump-splices output. Thankfully, the generated code still behaves as expected, but we'll have to live with some counterintuitive golden output until that GHC bug gets fixed upstream.

(%%%%) ::
(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 @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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:
Expand All @@ -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

Expand All @@ -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
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 @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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.
-}
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 @@ -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)
Expand Down
Loading