diff --git a/README.md b/README.md index dda1de55..8a73419a 100644 --- a/README.md +++ b/README.md @@ -1435,11 +1435,14 @@ The following constructs are either unsupported or almost never work: * datatypes that store arrows or `Symbol` * rank-n types +* embedded type expressions and patterns * promoting `TypeRep`s * `TypeApplications` * Irrefutable patterns * `{-# UNPACK #-}` pragmas * partial application of the `(->)` type +* namespace specifiers in fixity declarations +* invisible type patterns See the following sections for more details. @@ -1559,6 +1562,20 @@ _vanilla_ types, where a vanilla function type is a type that: 3. Contains no visible dependent quantification. +### Embedded type expressions and patterns + +As a consequence of `singletons-th` not supporting types with visible dependent +quantification (see the "Rank-n types" section above), `singletons-th` will not +support embedded types in expressions or patterns. This means that +`singletons-th` will reject the following examples: + +```hs +idv :: forall a -> a -> a +idv (type a) (x :: a) = x + +x = idv (type Bool) True +``` + ### Promoting `TypeRep`s The built-in Haskell promotion mechanism does not yet have a full story around @@ -1611,3 +1628,29 @@ quantification cannot be unpacked. See 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 +use of `@t` in this example: + +```hs +f :: a -> a +f @t x = x :: t +``` + +See [this `singletons` +issue](https://github.com/goldfirere/singletons/issues/583). diff --git a/cabal.project b/cabal.project index 15246c29..414bbbb3 100644 --- a/cabal.project +++ b/cabal.project @@ -5,4 +5,4 @@ packages: ./singletons source-repository-package type: git location: https://github.com/goldfirere/th-desugar - tag: ab301774cbe9837a9f62dceaf9ef50c76dc7c5c9 + tag: a910bb140d6f9d0c69077c32f70ff08286825dff diff --git a/singletons-base/singletons-base.cabal b/singletons-base/singletons-base.cabal index b343863f..64cdc8cf 100644 --- a/singletons-base/singletons-base.cabal +++ b/singletons-base/singletons-base.cabal @@ -78,7 +78,7 @@ library singletons-th >= 3.3 && < 3.4, template-haskell >= 2.21 && < 2.22, text >= 1.2, - th-desugar >= 1.16 && < 1.17 + th-desugar >= 1.17 && < 1.18 default-language: GHC2021 other-extensions: TemplateHaskell exposed-modules: Data.Singletons.Base.CustomStar diff --git a/singletons-th/singletons-th.cabal b/singletons-th/singletons-th.cabal index 79668429..f9e150fc 100644 --- a/singletons-th/singletons-th.cabal +++ b/singletons-th/singletons-th.cabal @@ -59,7 +59,7 @@ library singletons == 3.0.*, syb >= 0.4, template-haskell >= 2.21 && < 2.22, - th-desugar >= 1.16 && < 1.17, + th-desugar >= 1.17 && < 1.18, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2 default-language: GHC2021 diff --git a/singletons-th/src/Data/Singletons/TH/Partition.hs b/singletons-th/src/Data/Singletons/TH/Partition.hs index 5df7aaae..7dff6897 100644 --- a/singletons-th/src/Data/Singletons/TH/Partition.hs +++ b/singletons-th/src/Data/Singletons/TH/Partition.hs @@ -163,7 +163,7 @@ 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)) = +partitionClassDec (DLetDec (DInfixD fixity _ name)) = pure (infixDecl fixity name, mempty) partitionClassDec (DLetDec (DPragmaD {})) = pure (mempty, mempty) diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index c29da2a0..9b5e35f6 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -637,7 +637,7 @@ promoteInfixDecl mb_let_uniq name fixity = do where -- Produce the fixity declaration. finish :: Name -> q (Maybe DDec) - finish = pure . Just . DLetDec . DInfixD fixity + finish = pure . Just . DLetDec . DInfixD fixity NoNamespaceSpecifier -- Don't produce a fixity declaration at all. This can happen in the -- following circumstances: @@ -1045,6 +1045,8 @@ promotePat (DSigP pat ty) = do tell $ PromDPatInfos [] (fvDType ki) return (DSigT promoted ki, ADSigP promoted pat' ki) promotePat DWildP = return (DWildCardT, ADWildP) +promotePat p@(DTypeP _) = fail ("Embedded type patterns cannot be promoted: " ++ show p) +promotePat p@(DInvisP _) = fail ("Invisible type patterns cannot be promoted: " ++ show p) promoteExp :: DExp -> PrM (DType, ADExp) promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name @@ -1106,6 +1108,7 @@ promoteExp (DSigE exp ty) = do promoteExp e@(DStaticE _) = fail ("Static expressions cannot be promoted: " ++ show e) promoteExp e@(DTypedBracketE _) = fail ("Typed bracket expressions cannot be promoted: " ++ show e) promoteExp e@(DTypedSpliceE _) = fail ("Typed splice expressions cannot be promoted: " ++ show e) +promoteExp e@(DTypeE _) = fail ("Embedded type expressions cannot be promoted: " ++ show e) promoteLitExp :: OptionsMonad q => Lit -> q DType promoteLitExp (IntegerL n) = do diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs index 1ae165ab..7026c759 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs @@ -421,7 +421,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 n + mk_fix_decl n f = DLetDec $ DInfixD f NoNamespaceSpecifier n -- Indicates whether the type being defunctionalized has a standalone kind -- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs index 44272ba2..1e2f4a57 100644 --- a/singletons-th/src/Data/Singletons/TH/Single.hs +++ b/singletons-th/src/Data/Singletons/TH/Single.hs @@ -1003,6 +1003,7 @@ isException (DSigE e _) = isException e isException (DStaticE e) = isException e isException (DTypedBracketE e) = isException e isException (DTypedSpliceE e) = isException e +isException (DTypeE _) = False singMatch :: ADMatch -> SgM DMatch singMatch (ADMatch var_proms pat exp) = do diff --git a/singletons-th/src/Data/Singletons/TH/Single/Fixity.hs b/singletons-th/src/Data/Singletons/TH/Single/Fixity.hs index 048be673..9eea913a 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Fixity.hs +++ b/singletons-th/src/Data/Singletons/TH/Single/Fixity.hs @@ -34,7 +34,7 @@ singInfixDecl name fixity = do -- See [singletons-th and fixity declarations], wrinkle 1. where finish :: Name -> q (Maybe DLetDec) - finish = pure . Just . DInfixD fixity + finish = pure . Just . DInfixD fixity NoNamespaceSpecifier never_mind :: q (Maybe DLetDec) never_mind = pure Nothing diff --git a/singletons-th/src/Data/Singletons/TH/Syntax.hs b/singletons-th/src/Data/Singletons/TH/Syntax.hs index f49c09d1..7bde9213 100644 --- a/singletons-th/src/Data/Singletons/TH/Syntax.hs +++ b/singletons-th/src/Data/Singletons/TH/Syntax.hs @@ -196,7 +196,7 @@ buildLetDecEnv = go emptyLetDecEnv go acc (flattened ++ rest) go acc (DSigD name ty : rest) = go (typeBinding name ty <> acc) rest - go acc (DInfixD f n : rest) = + go acc (DInfixD f _ n : rest) = go (infixDecl f n <> acc) rest go acc (DPragmaD{} : rest) = go acc rest