{- Data/Singletons/Single/Type.hs (c) Richard Eisenberg 2013 rae@cs.brynmawr.edu Singletonizes types. -} module Data.Singletons.Single.Type where import Language.Haskell.TH.Desugar import Language.Haskell.TH.Desugar.OSet (OSet) import Language.Haskell.TH.Syntax import Data.Singletons.Names import Data.Singletons.Single.Monad import Data.Singletons.Promote.Type import Data.Singletons.TH.Options import Data.Singletons.Util import Control.Monad import Data.Foldable import Data.Function import Data.List (deleteFirstsBy) singType :: OSet Name -- the set of bound kind variables in this scope -- see Note [Explicitly binding kind variables] -- in Data.Singletons.Promote.Monad -> DType -- the promoted version of the thing classified by... -> DType -- ... this type -> SgM ( DType -- the singletonized type , Int -- the number of arguments , [Name] -- the names of the tyvars used in the sing'd type , DCxt -- the context of the singletonized type , [DKind] -- the kinds of the argument types , DKind ) -- the kind of the result type singType :: OSet Name -> DType -> DType -> SgM (DType, Int, [Name], DCxt, DCxt, DType) singType OSet Name bound_kvs DType prom DType ty = do ([DTyVarBndr] orig_tvbs, DCxt cxt, DCxt args, DType res) <- DType -> SgM ([DTyVarBndr], DCxt, DCxt, DType) forall (m :: * -> *). MonadFail m => DType -> m ([DTyVarBndr], DCxt, DCxt, DType) unravelVanillaDType DType ty let num_args :: Int num_args = DCxt -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length DCxt args DCxt cxt' <- (DType -> SgM DType) -> DCxt -> SgM DCxt forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM DType -> SgM DType singPred_NC DCxt cxt [Name] arg_names <- Int -> SgM Name -> SgM [Name] forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a] replicateM Int num_args (String -> SgM Name forall (m :: * -> *). Quasi m => String -> m Name qNewName String "t") DCxt prom_args <- (DType -> SgM DType) -> DCxt -> SgM DCxt forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM DType -> SgM DType forall (m :: * -> *). MonadFail m => DType -> m DType promoteType_NC DCxt args DType prom_res <- DType -> SgM DType forall (m :: * -> *). MonadFail m => DType -> m DType promoteType_NC DType res let args' :: DCxt args' = (Name -> DType) -> [Name] -> DCxt forall a b. (a -> b) -> [a] -> [b] map (\Name n -> DType singFamily DType -> DType -> DType `DAppT` (Name -> DType DVarT Name n)) [Name] arg_names res' :: DType res' = DType singFamily DType -> DType -> DType `DAppT` ((DType -> DType -> DType) -> DType -> DCxt -> DType forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl DType -> DType -> DType apply DType prom ((Name -> DType) -> [Name] -> DCxt forall a b. (a -> b) -> [a] -> [b] map Name -> DType DVarT [Name] arg_names) DType -> DType -> DType `DSigT` DType prom_res) -- Make sure to include an explicit `prom_res` kind annotation. -- See Note [Preserve the order of type variables during singling], -- wrinkle 3. kvbs :: [DTyVarBndr] kvbs = [DTyVarBndr] -> DCxt -> DCxt -> DType -> OSet Name -> [DTyVarBndr] singTypeKVBs [DTyVarBndr] orig_tvbs DCxt prom_args DCxt cxt' DType prom_res OSet Name bound_kvs all_tvbs :: [DTyVarBndr] all_tvbs = [DTyVarBndr] kvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] -> [a] ++ (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Name -> DType -> DTyVarBndr DKindedTV [Name] arg_names DCxt prom_args ty' :: DType ty' = [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType ravelVanillaDType [DTyVarBndr] all_tvbs DCxt cxt' DCxt args' DType res' (DType, Int, [Name], DCxt, DCxt, DType) -> SgM (DType, Int, [Name], DCxt, DCxt, DType) forall (m :: * -> *) a. Monad m => a -> m a return (DType ty', Int num_args, [Name] arg_names, DCxt cxt, DCxt prom_args, DType prom_res) -- Compute the kind variable binders to use in the singled version of a type -- signature. This has two main call sites: singType and D.S.Single.Data.singCtor. -- -- This implements the advice documented in -- Note [Preserve the order of type variables during singling], wrinkle 1. singTypeKVBs :: [DTyVarBndr] -- ^ The bound type variables from the original type signature. -> [DType] -- ^ The argument types of the signature (promoted). -> DCxt -- ^ The context of the signature (singled). -> DType -- ^ The result type of the signature (promoted). -> OSet Name -- ^ The type variables previously bound in the current scope. -> [DTyVarBndr] -- ^ The kind variables for the singled type signature. singTypeKVBs :: [DTyVarBndr] -> DCxt -> DCxt -> DType -> OSet Name -> [DTyVarBndr] singTypeKVBs [DTyVarBndr] orig_tvbs DCxt prom_args DCxt sing_ctxt DType prom_res OSet Name bound_tvbs | [DTyVarBndr] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [DTyVarBndr] orig_tvbs -- There are no explicitly `forall`ed type variable binders, so we must -- infer them ourselves. = (DTyVarBndr -> DTyVarBndr -> Bool) -> [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. (a -> a -> Bool) -> [a] -> [a] -> [a] deleteFirstsBy (Name -> Name -> Bool forall a. Eq a => a -> a -> Bool (==) (Name -> Name -> Bool) -> (DTyVarBndr -> Name) -> DTyVarBndr -> DTyVarBndr -> Bool forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` DTyVarBndr -> Name extractTvbName) (DCxt -> [DTyVarBndr] toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ DCxt prom_args DCxt -> DCxt -> DCxt forall a. [a] -> [a] -> [a] ++ DCxt sing_ctxt DCxt -> DCxt -> DCxt forall a. [a] -> [a] -> [a] ++ [DType prom_res]) ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr] forall a b. (a -> b) -> [a] -> [b] map Name -> DTyVarBndr DPlainTV ([Name] -> [DTyVarBndr]) -> [Name] -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ OSet Name -> [Name] forall (t :: * -> *) a. Foldable t => t a -> [a] toList OSet Name bound_tvbs) -- Make sure to subtract out the bound variables currently in scope, -- lest we accidentally shadow them in this type signature. -- See Note [Explicitly binding kind variables] in D.S.Promote.Monad. | Bool otherwise -- There is an explicit `forall`, so this case is easy. = [DTyVarBndr] orig_tvbs -- Single a DPred, checking that it is a vanilla type in the process. -- See [Vanilla-type validity checking during promotion] -- in Data.Singletons.Promote.Type. singPred :: DPred -> SgM DPred singPred :: DType -> SgM DType singPred DType p = do DType -> SgM () forall (m :: * -> *). MonadFail m => DType -> m () checkVanillaDType DType p DType -> SgM DType singPred_NC DType p -- Single a DPred. Does not check if the argument is a vanilla type. -- See [Vanilla-type validity checking during promotion] -- in Data.Singletons.Promote.Type. singPred_NC :: DPred -> SgM DPred singPred_NC :: DType -> SgM DType singPred_NC = [DTypeArg] -> DType -> SgM DType singPredRec [] -- The workhorse for singPred_NC. singPredRec :: [DTypeArg] -> DPred -> SgM DPred singPredRec :: [DTypeArg] -> DType -> SgM DType singPredRec [DTypeArg] _cxt (DForallT {}) = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Singling of quantified constraints not yet supported" singPredRec [DTypeArg] _cxt (DConstrainedT {}) = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Singling of quantified constraints not yet supported" singPredRec [DTypeArg] ctx (DAppT DType pr DType ty) = [DTypeArg] -> DType -> SgM DType singPredRec (DType -> DTypeArg DTANormal DType ty DTypeArg -> [DTypeArg] -> [DTypeArg] forall a. a -> [a] -> [a] : [DTypeArg] ctx) DType pr singPredRec [DTypeArg] ctx (DAppKindT DType pr DType ki) = [DTypeArg] -> DType -> SgM DType singPredRec (DType -> DTypeArg DTyArg DType ki DTypeArg -> [DTypeArg] -> [DTypeArg] forall a. a -> [a] -> [a] : [DTypeArg] ctx) DType pr singPredRec [DTypeArg] _ctx (DSigT DType _pr DType _ki) = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Singling of constraints with explicit kinds not yet supported" singPredRec [DTypeArg] _ctx (DVarT Name _n) = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Singling of contraint variables not yet supported" singPredRec [DTypeArg] ctx (DConT Name n) | Name n Name -> Name -> Bool forall a. Eq a => a -> a -> Bool == Name equalityName = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Singling of type equality constraints not yet supported" | Bool otherwise = do Options opts <- SgM Options forall (m :: * -> *). OptionsMonad m => m Options getOptions [DTypeArg] kis <- (DTypeArg -> SgM DTypeArg) -> [DTypeArg] -> SgM [DTypeArg] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM DTypeArg -> SgM DTypeArg forall (m :: * -> *). MonadFail m => DTypeArg -> m DTypeArg promoteTypeArg_NC [DTypeArg] ctx let sName :: Name sName = Options -> Name -> Name singledClassName Options opts Name n DType -> SgM DType forall (m :: * -> *) a. Monad m => a -> m a return (DType -> SgM DType) -> DType -> SgM DType forall a b. (a -> b) -> a -> b $ DType -> [DTypeArg] -> DType applyDType (Name -> DType DConT Name sName) [DTypeArg] kis singPredRec [DTypeArg] _ctx DType DWildCardT = DType -> SgM DType forall (m :: * -> *) a. Monad m => a -> m a return DType DWildCardT -- it just might work singPredRec [DTypeArg] _ctx DType DArrowT = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "(->) spotted at head of a constraint" singPredRec [DTypeArg] _ctx (DLitT {}) = String -> SgM DType forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Type-level literal spotted at head of a constraint" {- Note [Preserve the order of type variables during singling] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ singletons does its best to preseve the order in which users write type variables in type signatures for functions and data constructors. They are "preserved" in the sense that if one writes `foo @T1 @T2`, one should be able to write out `sFoo @T1 @T2` by hand and have the same order of visible type applications still work. Accomplishing this is surprisingly nontrivial, so this Note documents the various wrinkles one must iron out to get this working. ----- -- Wrinkle 1: Dealing with the presence (and absence) of `forall` ----- If we single a function that has an explicit `forall`, such as this example: const2 :: forall b a. a -> b -> a const2 x _ = x Then our job is easy, as the exact order of type variables has already been spelled out in advance. We single this to: sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y :: a) sConst2 = ... What happens if there is no explicit `forall`, as in this example? data V a absurd :: V a -> b absurd v = case v of {} This time, the order of type variables vis-à-vis TypeApplications is determined by their left-to-right order of appearance in the type signature. It's tempting to think that since there is no explicit `forall` in the original type signature, we could get away without an explicit `forall` in the singled type signature. That is, one could write: sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b) This would have the right type variable order, but unfortunately, this approach does not play well with singletons' style of code generation. Consider the code that would be generated for the body of sAbsurd: sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b) sAbsurd (sV :: Sing v) = id @(Case v v :: b) (case sV of {}) Note the use of the type `Case v v :: b` in the right-hand side of sAbsurd. However, because `b` was not bound by a top-level `forall`, it won't be in scope here, resulting in an error! (Why do we generate the code `id @(Case v v :: b)` in the first place? See Note [The id hack; or, how singletons learned to stop worrying and avoid kind generalization] in D.S.Single.) The simplest approach is to just always generate singled type signatures with explicit `forall`s. In the event that the original type signature lacks an explicit `forall`, we inferr the correct type variable ordering ourselves and synthesize a `forall` with that order. The `singTypeKVBs` function implements this logic. ----- -- Wrinkle 2: The TH reification swamp ----- There is another issue with type signatures that lack explicit `forall`s, one which the current design of Template Haskell does not make simple to fix. If we single code that is wrapped in TH quotes, such as in the following example: $(singletons [d| data Proxy (a :: k) where MkProxy :: Proxy a |]) Then our job is made much easier when singling MkProxy, since we know that the only type variable that must be quantified is `a`, as that is the only one specified in the type signature. However, this is not the only possible way to single MkProxy. One can alternatively use $(genSingletons [''Proxy]), which uses TH reification to infer the type of MkProxy. There is perilous, however, because this is how TH reifies MkProxy: ForallC [KindedTV k StarT,KindedTV a (VarT k)] [] (GadtC [MkProxy] [] (AppT (ConT Proxy) (VarT a))) In terms of actual Haskell code, that's: MkProxy :: forall k (a :: k). Proxy a This is subtly different than before, as `k` is now specified. Contrast this with `MkProxy :: Proxy a`, where `k` is invisible. In other words, if you single MkProxy using genSingletons, then `Proxy @True` will typecheck but `SMkProxy @True` will /not/ typecheck—you'd have to use `SMkProxy @_ @True` instead. Urk! At present, Template Haskell does not have a way to distinguish specified from inferred type variables—see GHC #17159—and it is unclear how one could work around this issue withouf first fixing #17159 upstream. Thankfully, it is only likely to bite in situations where the original type signature uses inferred variables, so the damage is somewhat minimal. ----- -- Wrinkle 3: Where to put explicit kind annotations ----- Type variable binders are only part of the story—we must also determine what the body of the type signature will be singled to. As a general rule, if the original type signature is of the form: f :: forall a_1 ... a_m. (C_1, ..., C_n) => T_1 -> ... -> T_p -> R Then the singled type signature will be: sF :: forall a_1 ... a_m (x_1 :: PT_1) ... (x_p :: PT_p). (SC_1, ..., SC_n) => Sing x1 -> ... -> Sing x_p -> SRes (F x1 ... x_p :: PR) Where: * x_i is a fresh type variable of kind PT_i. * PT_i is the promoted version of the type T_i, and PR is the promoted version of the type R. * SC_i is the singled version of the constraint SC_i. * SRes is either `Sing` if dealing with a function, or a singled data type if dealing with a data constructor. For instance, SRes is `SBool` in `STrue :: SBool (True :: Bool)`. One aspect of this worth pointing out is the explicit `:: PR` kind annotation in the result type `Sing (F x1 ... x_p :: PR)`. As it turns out, this kind annotation is mandatory, as omitting can result in singled type signatures with the wrong semantics. For instance, consider the `Nothing` data constructor: Nothing :: forall a. Maybe a Consider what would happen if it were singled to this type: SNothing :: forall a. SMaybe Nothing This is not what we want at all, since the `a` has no connection to the `Nothing` in the result type. It's as if we had written this: SNothing :: forall {t} a. SMaybe (Nothing :: Maybe t) If we instead generate `forall a. SMaybe (Nothing :: Maybe a)`, then this issue is handily avoided. You might wonder if it would be cleaner to use visible kind applications instead: SNothing :: forall a. SMaybe (Nothing @a) This does work for many cases, but there are also some corner cases where this approach fails. Recall the `MkProxy` example from Wrinkle 2 above: data Proxy (a :: k) where MkProxy :: Proxy a $(genSingletons [''Proxy]) Due to the design of Template Haskell (discussed in Wrinkle 2), `MkProxy` will be reified with the type of `forall k (a :: k). Proxy a`. This means that if we used visible kind applications in the result type, we would end up with this: SMkProxy :: forall k (a :: k). SProxy (MkProxy @k @a) This will not kind-check because MkProxy only accepts /one/ visible kind argument, whereas this supplies it with two. To avoid this issue, we instead use the type `forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/ technically wrong due to the fact that it explicitly quantifies `k`, but at the very least it typechecks. If GHC #17159 were fixed, we could revisit this design choice. Finally, note that we need only write `Sing x_1 -> ... -> Sing x_p`, and not `Sing (x_1 :: PT_1) -> ... Sing (x_p :: PT_p)`. This is simply because we always use explicit `forall`s in singled type signatures, and therefore always explicitly bind `(x_1 :: PT_1) ... (x_p :: PT_p)`, which fully determine the kinds of `x_1 ... x_p`. It wouldn't be wrong to add extra kind annotations to `Sing x_1 -> ... -> Sing x_p`, just redundant. -}