{- Data/Singletons/Promote/Defun.hs (c) Richard Eisenberg, Jan Stolarek 2014 rae@cs.brynmawr.edu This file creates defunctionalization symbols for types during promotion. -} {-# LANGUAGE TemplateHaskell #-} module Data.Singletons.Promote.Defun where import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OSet as OSet import Data.Singletons.Promote.Monad import Data.Singletons.Promote.Type import Data.Singletons.Names import Language.Haskell.TH.Syntax import Data.Singletons.Syntax import Data.Singletons.Util import Control.Monad import Data.Foldable import qualified Data.Map.Strict as Map import Data.Map.Strict (Map) import Data.Maybe defunInfo :: DInfo -> PrM [DDec] defunInfo :: DInfo -> PrM [DDec] defunInfo (DTyConI dec :: DDec dec _instances :: Maybe [DDec] _instances) = DDec -> PrM [DDec] buildDefunSyms DDec dec defunInfo (DPrimTyConI _name :: Name _name _numArgs :: Int _numArgs _unlifted :: Bool _unlifted) = String -> PrM [DDec] forall (m :: * -> *) a. MonadFail m => String -> m a fail (String -> PrM [DDec]) -> String -> PrM [DDec] forall a b. (a -> b) -> a -> b $ "Building defunctionalization symbols of primitive " String -> String -> String forall a. [a] -> [a] -> [a] ++ "type constructors not supported" defunInfo (DVarI _name :: Name _name _ty :: DType _ty _mdec :: Maybe Name _mdec) = String -> PrM [DDec] forall (m :: * -> *) a. MonadFail m => String -> m a fail "Building defunctionalization symbols of values not supported" defunInfo (DTyVarI _name :: Name _name _ty :: DType _ty) = String -> PrM [DDec] forall (m :: * -> *) a. MonadFail m => String -> m a fail "Building defunctionalization symbols of type variables not supported" defunInfo (DPatSynI {}) = String -> PrM [DDec] forall (m :: * -> *) a. MonadFail m => String -> m a fail "Building defunctionalization symbols of pattern synonyms not supported" defunTypeDecls :: [TySynDecl] -> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM () defunTypeDecls :: [TySynDecl] -> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM () defunTypeDecls ty_syns :: [TySynDecl] ty_syns c_tyfams :: [ClosedTypeFamilyDecl] c_tyfams o_tyfams :: [OpenTypeFamilyDecl] o_tyfams = do [DDec] defun_ty_syns <- (TySynDecl -> PrM [DDec]) -> [TySynDecl] -> PrM [DDec] forall (monad :: * -> *) monoid (t :: * -> *) a. (Monad monad, Monoid monoid, Traversable t) => (a -> monad monoid) -> t a -> monad monoid concatMapM (\(TySynDecl name :: Name name tvbs :: [DTyVarBndr] tvbs rhs :: DType rhs) -> Name -> [DTyVarBndr] -> DType -> PrM [DDec] buildDefunSymsTySynD Name name [DTyVarBndr] tvbs DType rhs) [TySynDecl] ty_syns [DDec] defun_c_tyfams <- (ClosedTypeFamilyDecl -> PrM [DDec]) -> [ClosedTypeFamilyDecl] -> PrM [DDec] forall (monad :: * -> *) monoid (t :: * -> *) a. (Monad monad, Monoid monoid, Traversable t) => (a -> monad monoid) -> t a -> monad monoid concatMapM (DTypeFamilyHead -> PrM [DDec] buildDefunSymsClosedTypeFamilyD (DTypeFamilyHead -> PrM [DDec]) -> (ClosedTypeFamilyDecl -> DTypeFamilyHead) -> ClosedTypeFamilyDecl -> PrM [DDec] forall b c a. (b -> c) -> (a -> b) -> a -> c . ClosedTypeFamilyDecl -> DTypeFamilyHead forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead getTypeFamilyDecl) [ClosedTypeFamilyDecl] c_tyfams [DDec] defun_o_tyfams <- (OpenTypeFamilyDecl -> PrM [DDec]) -> [OpenTypeFamilyDecl] -> PrM [DDec] forall (monad :: * -> *) monoid (t :: * -> *) a. (Monad monad, Monoid monoid, Traversable t) => (a -> monad monoid) -> t a -> monad monoid concatMapM (DTypeFamilyHead -> PrM [DDec] buildDefunSymsOpenTypeFamilyD (DTypeFamilyHead -> PrM [DDec]) -> (OpenTypeFamilyDecl -> DTypeFamilyHead) -> OpenTypeFamilyDecl -> PrM [DDec] forall b c a. (b -> c) -> (a -> b) -> a -> c . OpenTypeFamilyDecl -> DTypeFamilyHead forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead getTypeFamilyDecl) [OpenTypeFamilyDecl] o_tyfams [DDec] -> PrM () forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m () emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM () forall a b. (a -> b) -> a -> b $ [DDec] defun_ty_syns [DDec] -> [DDec] -> [DDec] forall a. [a] -> [a] -> [a] ++ [DDec] defun_c_tyfams [DDec] -> [DDec] -> [DDec] forall a. [a] -> [a] -> [a] ++ [DDec] defun_o_tyfams buildDefunSyms :: DDec -> PrM [DDec] buildDefunSyms :: DDec -> PrM [DDec] buildDefunSyms (DDataD _new_or_data :: NewOrData _new_or_data _cxt :: DCxt _cxt _tyName :: Name _tyName _tvbs :: [DTyVarBndr] _tvbs _k :: Maybe DType _k ctors :: [DCon] ctors _derivings :: [DDerivClause] _derivings) = [DCon] -> PrM [DDec] buildDefunSymsDataD [DCon] ctors buildDefunSyms (DClosedTypeFamilyD tf_head :: DTypeFamilyHead tf_head _) = DTypeFamilyHead -> PrM [DDec] buildDefunSymsClosedTypeFamilyD DTypeFamilyHead tf_head buildDefunSyms (DOpenTypeFamilyD tf_head :: DTypeFamilyHead tf_head) = DTypeFamilyHead -> PrM [DDec] buildDefunSymsOpenTypeFamilyD DTypeFamilyHead tf_head buildDefunSyms (DTySynD name :: Name name tvbs :: [DTyVarBndr] tvbs rhs :: DType rhs) = Name -> [DTyVarBndr] -> DType -> PrM [DDec] buildDefunSymsTySynD Name name [DTyVarBndr] tvbs DType rhs buildDefunSyms (DClassD _cxt :: DCxt _cxt name :: Name name tvbs :: [DTyVarBndr] tvbs _fundeps :: [FunDep] _fundeps _members :: [DDec] _members) = do Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunReifyFixity Name name [DTyVarBndr] tvbs (DType -> Maybe DType forall a. a -> Maybe a Just (Name -> DType DConT Name constraintName)) buildDefunSyms _ = String -> PrM [DDec] forall (m :: * -> *) a. MonadFail m => String -> m a fail (String -> PrM [DDec]) -> String -> PrM [DDec] forall a b. (a -> b) -> a -> b $ "Defunctionalization symbols can only be built for " String -> String -> String forall a. [a] -> [a] -> [a] ++ "type families and data declarations" buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec] buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec] buildDefunSymsClosedTypeFamilyD = (DTyVarBndr -> DTyVarBndr) -> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec] buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr forall a. a -> a id Maybe DType -> Maybe DType forall a. a -> a id buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec] buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec] buildDefunSymsOpenTypeFamilyD = (DTyVarBndr -> DTyVarBndr) -> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec] buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr cuskify Maybe DType -> Maybe DType default_to_star where default_to_star :: Maybe DKind -> Maybe DKind default_to_star :: Maybe DType -> Maybe DType default_to_star Nothing = DType -> Maybe DType forall a. a -> Maybe a Just (DType -> Maybe DType) -> DType -> Maybe DType forall a b. (a -> b) -> a -> b $ Name -> DType DConT Name typeKindName default_to_star (Just k :: DType k) = DType -> Maybe DType forall a. a -> Maybe a Just DType k buildDefunSymsTypeFamilyHead :: (DTyVarBndr -> DTyVarBndr) -> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec] buildDefunSymsTypeFamilyHead :: (DTyVarBndr -> DTyVarBndr) -> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec] buildDefunSymsTypeFamilyHead default_tvb :: DTyVarBndr -> DTyVarBndr default_tvb default_kind :: Maybe DType -> Maybe DType default_kind (DTypeFamilyHead name :: Name name tvbs :: [DTyVarBndr] tvbs result_sig :: DFamilyResultSig result_sig _) = do let arg_tvbs :: [DTyVarBndr] arg_tvbs = (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr] forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> DTyVarBndr default_tvb [DTyVarBndr] tvbs res_kind :: Maybe DType res_kind = Maybe DType -> Maybe DType default_kind (DFamilyResultSig -> Maybe DType resultSigToMaybeKind DFamilyResultSig result_sig) Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunReifyFixity Name name [DTyVarBndr] arg_tvbs Maybe DType res_kind buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec] buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec] buildDefunSymsTySynD name :: Name name tvbs :: [DTyVarBndr] tvbs rhs :: DType rhs = Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunReifyFixity Name name [DTyVarBndr] tvbs Maybe DType mb_res_kind where -- In order to have a CUSK, a type synonym must annotate its right-hand -- side with an explicit kind signature, so we can make use of this -- property to determine the result kind when defunctionalizing the -- type synonym. mb_res_kind :: Maybe DKind mb_res_kind :: Maybe DType mb_res_kind = case DType rhs of DSigT _ k :: DType k -> DType -> Maybe DType forall a. a -> Maybe a Just DType k _ -> Maybe DType forall a. Maybe a Nothing buildDefunSymsDataD :: [DCon] -> PrM [DDec] buildDefunSymsDataD :: [DCon] -> PrM [DDec] buildDefunSymsDataD ctors :: [DCon] ctors = (DCon -> PrM [DDec]) -> [DCon] -> PrM [DDec] forall (monad :: * -> *) monoid (t :: * -> *) a. (Monad monad, Monoid monoid, Traversable t) => (a -> monad monoid) -> t a -> monad monoid concatMapM DCon -> PrM [DDec] promoteCtor [DCon] ctors where promoteCtor :: DCon -> PrM [DDec] promoteCtor :: DCon -> PrM [DDec] promoteCtor ctor :: DCon ctor@(DCon _ _ _ _ res_ty :: DType res_ty) = do let (name :: Name name, arg_tys :: DCxt arg_tys) = DCon -> (Name, DCxt) extractNameTypes DCon ctor [Name] tvb_names <- Int -> PrM Name -> PrM [Name] forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a] replicateM (DCxt -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length DCxt arg_tys) (PrM Name -> PrM [Name]) -> PrM Name -> PrM [Name] forall a b. (a -> b) -> a -> b $ String -> PrM Name forall (m :: * -> *). Quasi m => String -> m Name qNewName "t" DCxt arg_kis <- (DType -> PrM DType) -> DCxt -> PrM DCxt forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM DType -> PrM DType forall (m :: * -> *). MonadFail m => DType -> m DType promoteType DCxt arg_tys let arg_tvbs :: [DTyVarBndr] arg_tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Name -> DType -> DTyVarBndr DKindedTV [Name] tvb_names DCxt arg_kis DType res_ki <- DType -> PrM DType forall (m :: * -> *). MonadFail m => DType -> m DType promoteType DType res_ty Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunReifyFixity Name name [DTyVarBndr] arg_tvbs (DType -> Maybe DType forall a. a -> Maybe a Just DType res_ki) -- Generate defunctionalization symbols for a name, using reifyFixityWithLocals -- to determine what the fixity of each symbol should be. -- See Note [Fixity declarations for defunctionalization symbols] defunReifyFixity :: Name -> [DTyVarBndr] -> Maybe DKind -> PrM [DDec] defunReifyFixity :: Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunReifyFixity name :: Name name tvbs :: [DTyVarBndr] tvbs m_res_kind :: Maybe DType m_res_kind = do Maybe Fixity m_fixity <- Name -> PrM (Maybe Fixity) forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity) reifyFixityWithLocals Name name Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunctionalize Name name Maybe Fixity m_fixity [DTyVarBndr] tvbs Maybe DType m_res_kind -- Generate data declarations and apply instances -- required for defunctionalization. -- For a type family: -- -- type family Foo (m :: Nat) (n :: Nat) (l :: Nat) :: Nat -- -- we generate data declarations that allow us to talk about partial -- application at the type level: -- -- type FooSym3 a b c = Foo a b c -- data FooSym2 a b f where -- FooSym2KindInference :: SameKind (Apply (FooSym2 a b) arg) (FooSym3 a b arg) -- => FooSym2 a b f -- type instance Apply (FooSym2 a b) c = FooSym3 a b c -- data FooSym1 a f where -- FooSym1KindInference :: SameKind (Apply (FooSym1 a) arg) (FooSym2 a arg) -- => FooSym1 a f -- type instance Apply (FooSym1 a) b = FooSym2 a b -- data FooSym0 f where -- FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) -- => FooSym0 f -- type instance Apply FooSym0 a = FooSym1 a -- -- What's up with all the "KindInference" stuff? In some scenarios, we don't -- know the kinds that we should be using in these symbols. But, GHC can figure -- it out using the types of the "KindInference" dummy data constructors. A -- bit of a hack, but it works quite nicely. The only problem is that GHC will -- warn about an unused data constructor. So, we use the data constructor in -- an instance of a dummy class. (See Data.Singletons.SuppressUnusedWarnings -- for the class, which should never be seen by anyone, ever.) -- -- The defunctionalize function takes Maybe DKinds so that the caller can -- indicate which kinds are known and which need to be inferred. -- -- See also Note [Defunctionalization and dependent quantification] defunctionalize :: Name -> Maybe Fixity -- The name's fixity, if one was declared. -> [DTyVarBndr] -> Maybe DKind -> PrM [DDec] defunctionalize :: Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec] defunctionalize name :: Name name m_fixity :: Maybe Fixity m_fixity m_arg_tvbs' :: [DTyVarBndr] m_arg_tvbs' m_res_kind' :: Maybe DType m_res_kind' = do (m_arg_tvbs :: [DTyVarBndr] m_arg_tvbs, m_res_kind :: Maybe DType m_res_kind) <- [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType) eta_expand ([DTyVarBndr] -> [DTyVarBndr] forall a. Data a => a -> a noExactTyVars [DTyVarBndr] m_arg_tvbs') (Maybe DType -> Maybe DType forall a. Data a => a -> a noExactTyVars Maybe DType m_res_kind') let -- Implements part (2)(i) from Note [Defunctionalization and dependent quantification] tvb_to_type_map :: Map Name DType tvb_to_type_map :: Map Name DType tvb_to_type_map = [(Name, DType)] -> Map Name DType forall k a. Ord k => [(k, a)] -> Map k a Map.fromList ([(Name, DType)] -> Map Name DType) -> [(Name, DType)] -> Map Name DType forall a b. (a -> b) -> a -> b $ -- (2)(i)(c) (DTyVarBndr -> (Name, DType)) -> [DTyVarBndr] -> [(Name, DType)] forall a b. (a -> b) -> [a] -> [b] map (\tvb :: DTyVarBndr tvb -> (DTyVarBndr -> Name extractTvbName DTyVarBndr tvb, DTyVarBndr -> DType dTyVarBndrToDType DTyVarBndr tvb)) ([DTyVarBndr] -> [(Name, DType)]) -> [DTyVarBndr] -> [(Name, DType)] forall a b. (a -> b) -> a -> b $ DCxt -> [DTyVarBndr] toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ -- (2)(i)(b) (DTyVarBndr -> DType) -> [DTyVarBndr] -> DCxt forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> DType dTyVarBndrToDType [DTyVarBndr] m_arg_tvbs DCxt -> DCxt -> DCxt forall a. [a] -> [a] -> [a] ++ Maybe DType -> DCxt forall a. Maybe a -> [a] maybeToList Maybe DType m_res_kind -- (2)(i)(a) go :: Int -> [DTyVarBndr] -> Maybe DKind -> ([DTyVarBndr] -> DType) -- given the argument tyvar binders, -- produce the RHS of the Apply instance -> PrM [DDec] go :: Int -> [DTyVarBndr] -> Maybe DType -> ([DTyVarBndr] -> DType) -> PrM [DDec] go _ [] _ _ = [DDec] -> PrM [DDec] forall (m :: * -> *) a. Monad m => a -> m a return [] go n :: Int n (m_arg :: DTyVarBndr m_arg : m_args :: [DTyVarBndr] m_args) m_result :: Maybe DType m_result mk_rhs :: [DTyVarBndr] -> DType mk_rhs = do Name extra_name <- String -> PrM Name forall (m :: * -> *). Quasi m => String -> m Name qNewName "arg" let tyfun_name :: Name tyfun_name = DTyVarBndr -> Name extractTvbName DTyVarBndr m_arg data_name :: Name data_name = Name -> Int -> Name promoteTySym Name name Int n next_name :: Name next_name = Name -> Int -> Name promoteTySym Name name (Int nInt -> Int -> Int forall a. Num a => a -> a -> a +1) con_name :: Name con_name = String -> String -> Name -> Name prefixName "" ":" (Name -> Name) -> Name -> Name forall a b. (a -> b) -> a -> b $ String -> String -> Name -> Name suffixName "KindInference" "###" Name data_name m_tyfun :: Maybe DType m_tyfun = Maybe DType -> Maybe DType -> Maybe DType buildTyFunArrow_maybe (DTyVarBndr -> Maybe DType extractTvbKind DTyVarBndr m_arg) Maybe DType m_result arg_params :: [DTyVarBndr] arg_params = -- Implements part (2)(ii) from -- Note [Defunctionalization and dependent quantification] (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr] forall a b. (a -> b) -> [a] -> [b] map ((DType -> DType) -> DTyVarBndr -> DTyVarBndr map_tvb_kind (Map Name DType -> DType -> DType substType Map Name DType tvb_to_type_map)) ([DTyVarBndr] -> [DTyVarBndr]) -> [DTyVarBndr] -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] reverse [DTyVarBndr] m_args arg_names :: [Name] arg_names = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name] forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> Name extractTvbName [DTyVarBndr] arg_params params :: [DTyVarBndr] params = [DTyVarBndr] arg_params [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] -> [a] ++ [Name -> DTyVarBndr DPlainTV Name tyfun_name] con_eq_ct :: DType con_eq_ct = Name -> DType DConT Name sameKindName DType -> DType -> DType `DAppT` DType lhs DType -> DType -> DType `DAppT` DType rhs where lhs :: DType lhs = DType -> DCxt -> DType foldType (Name -> DType DConT Name data_name) ((Name -> DType) -> [Name] -> DCxt forall a b. (a -> b) -> [a] -> [b] map Name -> DType DVarT [Name] arg_names) DType -> DType -> DType `apply` (Name -> DType DVarT Name extra_name) rhs :: DType rhs = DType -> DCxt -> DType foldType (Name -> DType DConT Name next_name) ((Name -> DType) -> [Name] -> DCxt forall a b. (a -> b) -> [a] -> [b] map Name -> DType DVarT ([Name] arg_names [Name] -> [Name] -> [Name] forall a. [a] -> [a] -> [a] ++ [Name extra_name])) con_decl :: DCon con_decl = [DTyVarBndr] -> DCxt -> Name -> DConFields -> DType -> DCon DCon ((DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr] forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> DTyVarBndr dropTvbKind [DTyVarBndr] params [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] -> [a] ++ [Name -> DTyVarBndr DPlainTV Name extra_name]) [DType con_eq_ct] Name con_name (Bool -> [DBangType] -> DConFields DNormalC Bool False []) (DType -> [DTyVarBndr] -> DType foldTypeTvbs (Name -> DType DConT Name data_name) [DTyVarBndr] params) data_decl :: DDec data_decl = NewOrData -> DCxt -> Name -> [DTyVarBndr] -> Maybe DType -> [DCon] -> [DDerivClause] -> DDec DDataD NewOrData Data [] Name data_name [DTyVarBndr] args Maybe DType res_ki [DCon con_decl] [] where (args :: [DTyVarBndr] args, res_ki :: Maybe DType res_ki) = case Maybe DType m_tyfun of Nothing -> ([DTyVarBndr] params, Maybe DType forall a. Maybe a Nothing) -- If we cannot infer the return type, don't bother -- trying to construct an explicit return kind. Just tyfun :: DType tyfun -> let bound_tvs :: OSet Name bound_tvs = [Name] -> OSet Name forall a. Ord a => [a] -> OSet a OSet.fromList ((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name] forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> Name extractTvbName [DTyVarBndr] arg_params) OSet Name -> OSet Name -> OSet Name forall a. Ord a => OSet a -> OSet a -> OSet a `OSet.union` (Maybe DType -> OSet Name) -> [Maybe DType] -> OSet Name forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap ((DType -> OSet Name) -> Maybe DType -> OSet Name forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap DType -> OSet Name fvDType) ((DTyVarBndr -> Maybe DType) -> [DTyVarBndr] -> [Maybe DType] forall a b. (a -> b) -> [a] -> [b] map DTyVarBndr -> Maybe DType extractTvbKind [DTyVarBndr] arg_params) not_bound :: DTyVarBndr -> Bool not_bound tvb :: DTyVarBndr tvb = Bool -> Bool not (DTyVarBndr -> Name extractTvbName DTyVarBndr tvb Name -> OSet Name -> Bool forall a. Ord a => a -> OSet a -> Bool `OSet.member` OSet Name bound_tvs) tvb_to_type :: Name -> DType tvb_to_type tvb_name :: Name tvb_name = DType -> Maybe DType -> DType forall a. a -> Maybe a -> a fromMaybe (Name -> DType DVarT Name tvb_name) (Maybe DType -> DType) -> Maybe DType -> DType forall a b. (a -> b) -> a -> b $ Name -> Map Name DType -> Maybe DType forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup Name tvb_name Map Name DType tvb_to_type_map -- Implements part (2)(iii) from -- Note [Defunctionalization and dependent quantification] tyfun_tvbs :: [DTyVarBndr] tyfun_tvbs = (DTyVarBndr -> Bool) -> [DTyVarBndr] -> [DTyVarBndr] forall a. (a -> Bool) -> [a] -> [a] filter DTyVarBndr -> Bool not_bound ([DTyVarBndr] -> [DTyVarBndr]) -> [DTyVarBndr] -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ -- (2)(iii)(d) DCxt -> [DTyVarBndr] toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr] forall a b. (a -> b) -> a -> b $ -- (2)(iii)(c) (Name -> DType) -> [Name] -> DCxt forall a b. (a -> b) -> [a] -> [b] map Name -> DType tvb_to_type ([Name] -> DCxt) -> [Name] -> DCxt forall a b. (a -> b) -> a -> b $ -- (2)(iii)(b) OSet Name -> [Name] forall (t :: * -> *) a. Foldable t => t a -> [a] toList (OSet Name -> [Name]) -> OSet Name -> [Name] forall a b. (a -> b) -> a -> b $ DType -> OSet Name fvDType DType tyfun -- (2)(iii)(a) in ([DTyVarBndr] arg_params, DType -> Maybe DType forall a. a -> Maybe a Just ([DTyVarBndr] -> DCxt -> DType -> DType DForallT [DTyVarBndr] tyfun_tvbs [] DType tyfun)) app_data_ty :: DType app_data_ty = DType -> [DTyVarBndr] -> DType foldTypeTvbs (Name -> DType DConT Name data_name) [DTyVarBndr] m_args app_eqn :: DTySynEqn app_eqn = Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn DTySynEqn Maybe [DTyVarBndr] forall a. Maybe a Nothing (Name -> DType DConT Name applyName DType -> DType -> DType `DAppT` DType app_data_ty DType -> DType -> DType `DAppT` Name -> DType DVarT Name tyfun_name) ([DTyVarBndr] -> DType mk_rhs ([DTyVarBndr] m_args [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] -> [a] ++ [Name -> DTyVarBndr DPlainTV Name tyfun_name])) app_decl :: DDec app_decl = DTySynEqn -> DDec DTySynInstD DTySynEqn app_eqn suppress :: DDec suppress = Maybe Overlap -> Maybe [DTyVarBndr] -> DCxt -> DType -> [DDec] -> DDec DInstanceD Maybe Overlap forall a. Maybe a Nothing Maybe [DTyVarBndr] forall a. Maybe a Nothing [] (Name -> DType DConT Name suppressClassName DType -> DType -> DType `DAppT` DType app_data_ty) [DLetDec -> DDec DLetDec (DLetDec -> DDec) -> DLetDec -> DDec forall a b. (a -> b) -> a -> b $ Name -> [DClause] -> DLetDec DFunD Name suppressMethodName [[DPat] -> DExp -> DClause DClause [] ((Name -> DExp DVarE 'snd) DExp -> DExp -> DExp `DAppE` [DExp] -> DExp mkTupleDExp [Name -> DExp DConE Name con_name, [DExp] -> DExp mkTupleDExp []])]] mk_rhs' :: [DTyVarBndr] -> DType mk_rhs' = DType -> [DTyVarBndr] -> DType foldTypeTvbs (Name -> DType DConT Name data_name) -- See Note [Fixity declarations for defunctionalization symbols] mk_fix_decl :: Fixity -> DDec mk_fix_decl f :: Fixity f = DLetDec -> DDec DLetDec (DLetDec -> DDec) -> DLetDec -> DDec forall a b. (a -> b) -> a -> b $ Fixity -> Name -> DLetDec DInfixD Fixity f Name data_name fixity_decl :: [DDec] fixity_decl = Maybe DDec -> [DDec] forall a. Maybe a -> [a] maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec] forall a b. (a -> b) -> a -> b $ (Fixity -> DDec) -> Maybe Fixity -> Maybe DDec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Fixity -> DDec mk_fix_decl Maybe Fixity m_fixity [DDec] decls <- Int -> [DTyVarBndr] -> Maybe DType -> ([DTyVarBndr] -> DType) -> PrM [DDec] go (Int n Int -> Int -> Int forall a. Num a => a -> a -> a - 1) [DTyVarBndr] m_args Maybe DType m_tyfun [DTyVarBndr] -> DType mk_rhs' [DDec] -> PrM [DDec] forall (m :: * -> *) a. Monad m => a -> m a return ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec] forall a b. (a -> b) -> a -> b $ DDec suppress DDec -> [DDec] -> [DDec] forall a. a -> [a] -> [a] : DDec data_decl DDec -> [DDec] -> [DDec] forall a. a -> [a] -> [a] : DDec app_decl DDec -> [DDec] -> [DDec] forall a. a -> [a] -> [a] : [DDec] fixity_decl [DDec] -> [DDec] -> [DDec] forall a. [a] -> [a] -> [a] ++ [DDec] decls let num_args :: Int num_args = [DTyVarBndr] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [DTyVarBndr] m_arg_tvbs sat_name :: Name sat_name = Name -> Int -> Name promoteTySym Name name Int num_args mk_rhs :: [DTyVarBndr] -> DType mk_rhs = DType -> [DTyVarBndr] -> DType foldTypeTvbs (Name -> DType DConT Name name) sat_dec :: DDec sat_dec = Name -> [DTyVarBndr] -> DType -> DDec DTySynD Name sat_name [DTyVarBndr] m_arg_tvbs ([DTyVarBndr] -> DType mk_rhs [DTyVarBndr] m_arg_tvbs) [DDec] other_decs <- Int -> [DTyVarBndr] -> Maybe DType -> ([DTyVarBndr] -> DType) -> PrM [DDec] go (Int num_args Int -> Int -> Int forall a. Num a => a -> a -> a - 1) ([DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] reverse [DTyVarBndr] m_arg_tvbs) Maybe DType m_res_kind [DTyVarBndr] -> DType mk_rhs [DDec] -> PrM [DDec] forall (m :: * -> *) a. Monad m => a -> m a return ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec] forall a b. (a -> b) -> a -> b $ DDec sat_dec DDec -> [DDec] -> [DDec] forall a. a -> [a] -> [a] : [DDec] other_decs where eta_expand :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind) eta_expand :: [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType) eta_expand m_arg_tvbs :: [DTyVarBndr] m_arg_tvbs Nothing = ([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType) forall (f :: * -> *) a. Applicative f => a -> f a pure ([DTyVarBndr] m_arg_tvbs, Maybe DType forall a. Maybe a Nothing) eta_expand m_arg_tvbs :: [DTyVarBndr] m_arg_tvbs (Just res_kind :: DType res_kind) = do let (_, _, argKs :: DCxt argKs, resultK :: DType resultK) = DType -> ([DTyVarBndr], DCxt, DCxt, DType) unravel DType res_kind [Name] tvb_names <- Int -> PrM Name -> PrM [Name] forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a] replicateM (DCxt -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length DCxt argKs) (PrM Name -> PrM [Name]) -> PrM Name -> PrM [Name] forall a b. (a -> b) -> a -> b $ String -> PrM Name forall (m :: * -> *). Quasi m => String -> m Name qNewName "e" let res_kind_arg_tvbs :: [DTyVarBndr] res_kind_arg_tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Name -> DType -> DTyVarBndr DKindedTV [Name] tvb_names DCxt argKs ([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType) forall (f :: * -> *) a. Applicative f => a -> f a pure ([DTyVarBndr] m_arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr] forall a. [a] -> [a] -> [a] ++ [DTyVarBndr] res_kind_arg_tvbs, DType -> Maybe DType forall a. a -> Maybe a Just DType resultK) map_tvb_kind :: (DKind -> DKind) -> DTyVarBndr -> DTyVarBndr map_tvb_kind :: (DType -> DType) -> DTyVarBndr -> DTyVarBndr map_tvb_kind _ tvb :: DTyVarBndr tvb@DPlainTV{} = DTyVarBndr tvb map_tvb_kind f :: DType -> DType f (DKindedTV n :: Name n k :: DType k) = Name -> DType -> DTyVarBndr DKindedTV Name n (DType -> DType f DType k) {- Note [Defunctionalization and dependent quantification] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The machinery in this module supports defunctionalizing types that use dependent quantification, such as in the following example: type family Symmetry (a :: Proxy t) (y :: Proxy t) (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) :: Type where Symmetry a y _ = y :~: a Here is what is involved in making this happen: 1. When defunctionalizing, we must not only know the argument kinds, but rather the argument *kind variable binders*. This is essential since, for instance, Symmetry dependently quantifies `a` and `y` and uses them in the kind of `e`. If we did not track the original kind variable names, then instead of generating this defunctionalization symbol for Symmetry: data SymmetrySym2 (a :: Proxy t) (y :: Proxy t) :: (a :~: y) ~> Type We would generate something more general, like this: data SymmetrySym2 (abc1 :: Proxy t) (abc2 :: Proxy t) :: (a :~: y) ~> Type Alas, there are times where will have no choice but to write a slightly more general kind than we should. For instance, consider this: data SymmetrySym0 :: Proxy t ~> Proxy t ~> (a :~: y) ~> Type This defunctionalization symbol doesn't capture the dependent quantification in the first and second argument kinds. But in order to do that properly, you'd need the ability to write something like: data SymmetrySym0 :: forall (a :: Proxy t) ~> forall (y :: Proxy t) ~> (a :~: y) ~> Type It is my (RGS's) belief that it is not possible to achieve something like this in today's GHC (see #304), so we'll just have to live with SymmetrySym0 being slightly more general than it ought to be. In practice, this is unlikely to bite unless you're writing code that specifically exploits this dependency in just the right way. 2. I pulled a fast one earlier by writing: data SymmetrySym0 :: Proxy t ~> Proxy t ~> (a :~: y) ~> Type GHC will actually reject this, because it does not have a CUSK. There are two glaring problems here: (a) The kind of `t` is underdetermined. (b) `a` and `y` should have kind `Proxy t`, but this is not currently the case. Ultimately, the fix is to use explicit kind signatures. A naïve attempt would be something like this: data SymmetrySym0 :: Proxy (t :: (k :: Type)) ~> Proxy (t :: (k :: Type)) ~> ((a :: Proxy (t :: (k :: Type))) :~: (y :: Proxy (t :: (k :: Type)))) ~> Type While that works, it adds a nontrivial amount of clutter. Plus, it requires figuring out (in Template Haskell) which variables have underdetermined kinds and substituting for them. Blegh. A much cleaner approach is: data SymmetrySym0 :: forall (k :: Type) (t :: k) (a :: Proxy t) (y :: Proxy t). Proxy t ~> Proxy t ~> (a :~: y) ~> Type This time, all we have to do is put an explicit `forall` in front, and we achieve a CUSK without having to muck up the body of return kind. It also has the benefit of looking much nicer in generated code. Let's talk about how to achieve this feat, using SymmetrySym1 as the guiding example: (i) Before we begin defunctionalizing a type, we construct a mapping from variable names to their corresponding types, complete with kinds. For instance, in Symmetry, we would have the following map: { k :-> DVarT k -- k , t :-> DSigT (DVarT t) (DVarT k) -- (t :: k) , a :-> DSigT (DVarT a) (DConT ''Proxy `DAppT` DVarT t) -- (a :: Proxy t) , y :-> DSigT (DVarT y) (DConT ''Proxy `DAppT` DVarT y) -- (y :: Proxy t) , e :-> DSigT (DVarT e) (DConT ''(:~:) `DAppT` DSigT (DVarT a) (DConT ''Proxy `DAppT` DSigT (DVarT t) (DVarT k)) `DAppT` DSigT (DVarT y) (DConT ''Proxy `DAppT` DSigT (DVarT t) (DVarT k))) -- (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) } Why do this? Because when constructing the `forall` in the return kind of a defunctionalization symbol, it's convenient to be able to know the kinds of everything being bound at a glance. It's not always possible to recover the kinds of every variable (for instance, if we're just given `Proxy t ~> Proxy t ~> (a :~: y) ~> Type`), so having this information is handy. To construct this map, we: (a) Grab the list of type variable binders (this is given as an input to defunctionalize, as discussed in part (1)) and turn it into a list of types. Also include the return kind (if there is one) in this list, as it may also mention type variables with explicit kinds. (b) Construct a flat list of all type variables mentioned in this list. This may involve looking in the kinds of type variables binders. (Note that this part is crucial—the the Singletons/PolyKinds test will fail to compile without it!) (c) Take the flat list and insert each variable into the map by mapping its name to its type (as demonstrated above). To continue the Symmetry example: (a) We grab the list of type variable binders [ (a :: Proxy t) , (y :: Proxy t) , (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) ] from the Symmetry declaration. Including the return kind (Type), we get: [ (a :: Proxy t) , (y :: Proxy t) , (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) , Type ] (b) We flatten this into a list of well scoped type variables: [ k , (t :: k) , (a :: Proxy t) , (y :: Proxy t) , (e :: (a :: Proxy (t :: k)) :~: (y :~: Proxy (t :: k))) ] (c) From this, we construct the map shown at the beginning of (i). (ii) Using the map, we will annotate any kind variables in the LHS of the declaration with their respective kinds. In this example, the LHS is: data SymmetrySym1 (a :: Proxy t) :: ... Since `t` maps to simply `(t :: k)` in the map, the LHS becomes: data SymmetrySym1 (a :: Proxy (t :: k)) :: ... Why do this? Because we need to make it apparent that `k` is bound on the LHS. If we don't, we might end up trying to quantify `k` in the return kind (see #353 for an example of what goes wrong if you try to do this). Having to explicitly annotate each occurrence of every kind variable on the LHS like this is a bit tiresome, especially since we don't have to do this in the return kind. If GHC had syntax for visible dependent quantification, we could avoid this step entirely and simply write: data SymmetrySym1 :: forall k (t :: k). forall (a :: Proxy t) -> ... Until GHC gains this syntax, this is the best alternative. (iii) When constructing each defunctionalization symbol, we will end up with some remaining type variable binders and a return kind. For instance: data SymmetrySym1 (a :: Proxy (t :: k)) :: forall ???. Proxy t ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) ~> Type We must fill in the ??? part. Here is how we do so: (a) Collect all of the type variables mentioned in the return kind. (b) Look up each type variable's corresponding type in the map (from part (i)) to learn as much kind information as possible. (c) Perform a reverse topological sort on these types to put the types (and kind) variables in proper dependency order. (d) Filter out any variables that are already bound by the type variable binders that precede the return kind. After doing these steps, what remains goes in place of ???. Let's explain this with the example above: data SymmetrySym1 (a :: Proxy (t :: k)) :: forall ???. Proxy t ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) ~> Type (a) [t, a, k, y] (b) [(t :: k), (a :: Proxy t), k, (y :: Proxy t)] (c) [k, (t :: k), (a :: Proxy t), (y :: Proxy t)] (d) [(y :: Proxy t)] (`k`, `t` and `a` were already bound) Therefore, we end up with: data SymmetrySym1 (a :: Proxy (t :: k)) :: forall (y :: Proxy t). Proxy t ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) ~> Type -} -- This is a small function with large importance. When generating -- defunctionalization data types, we often need to fill in the blank in the -- sort of code exemplified below: -- -- @ -- data FooSym2 a (b :: x) (c :: TyFun y z) where -- FooSym2KindInference :: _ -- @ -- -- Where the kind of @a@ is not known. It's extremely tempting to just -- copy-and-paste the type variable binders from the data type itself to the -- constructor, like so: -- -- @ -- data FooSym2 a (b :: x) (c :: TyFun y z) where -- FooSym2KindInference :: forall a (b :: x) (c :: TyFun y z). -- SameKind (...) (...). -- FooSym2KindInference a b c -- @ -- -- But this ends up being an untenable approach. Because @a@ lacks a kind -- signature, @FooSym2@ does not have a complete, user-specified kind signature -- (or CUSK), so GHC will fail to typecheck @FooSym2KindInference@. -- -- Thankfully, there's a workaround—just don't give any of the constructor's -- type variable binders any kinds: -- -- @ -- data FooSym2 a (b :: x) (c :: TyFun y z) where -- FooSym2KindInference :: forall a b c -- SameKind (...) (...). -- FooSym2KindInference a b c -- @ -- -- GHC may be moody when it comes to CUSKs, but it's at least understanding -- enough to typecheck this without issue. The 'dropTvbKind' function is -- what removes the kinds used in the kind inference constructor. dropTvbKind :: DTyVarBndr -> DTyVarBndr dropTvbKind :: DTyVarBndr -> DTyVarBndr dropTvbKind tvb :: DTyVarBndr tvb@(DPlainTV {}) = DTyVarBndr tvb dropTvbKind (DKindedTV n :: Name n _) = Name -> DTyVarBndr DPlainTV Name n -- Shorthand for building (k1 ~> k2) buildTyFunArrow :: DKind -> DKind -> DKind buildTyFunArrow :: DType -> DType -> DType buildTyFunArrow k1 :: DType k1 k2 :: DType k2 = Name -> DType DConT Name tyFunArrowName DType -> DType -> DType `DAppT` DType k1 DType -> DType -> DType `DAppT` DType k2 buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind buildTyFunArrow_maybe :: Maybe DType -> Maybe DType -> Maybe DType buildTyFunArrow_maybe m_k1 :: Maybe DType m_k1 m_k2 :: Maybe DType m_k2 = do DType k1 <- Maybe DType m_k1 DType k2 <- Maybe DType m_k2 DType -> Maybe DType forall (m :: * -> *) a. Monad m => a -> m a return (DType -> Maybe DType) -> DType -> Maybe DType forall a b. (a -> b) -> a -> b $ Name -> DType DConT Name tyFunArrowName DType -> DType -> DType `DAppT` DType k1 DType -> DType -> DType `DAppT` DType k2 -- Build (~>) kind from the list of kinds ravelTyFun :: [DKind] -> DKind ravelTyFun :: DCxt -> DType ravelTyFun [] = String -> DType forall a. HasCallStack => String -> a error "Internal error: TyFun raveling nil" ravelTyFun [k :: DType k] = DType k ravelTyFun kinds :: DCxt kinds = DCxt -> DType -> DType go DCxt tailK (DType -> DType -> DType buildTyFunArrow DType k2 DType k1) where (k1 :: DType k1 : k2 :: DType k2 : tailK :: DCxt tailK) = DCxt -> DCxt forall a. [a] -> [a] reverse DCxt kinds go :: DCxt -> DType -> DType go [] acc :: DType acc = DType acc go (k :: DType k:ks :: DCxt ks) acc :: DType acc = DCxt -> DType -> DType go DCxt ks (DType -> DType -> DType buildTyFunArrow DType k DType acc) {- Note [Fixity declarations for defunctionalization symbols] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Just like we promote fixity declarations, we should also generate fixity declarations for defunctionaliztion symbols. A primary use case is the following scenario: (.) :: (b -> c) -> (a -> b) -> (a -> c) (f . g) x = f (g x) infixr 9 . 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 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. -}