From d8c48c57c87c61b1869eef843e4a3f0160b1d675 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 28 May 2024 19:13:49 -0400 Subject: [PATCH] Introduce ForAllTyFlag, use it in matchUpSigWithDecl For now, this is simply a refactoring. We will make use of this more in a subsequent commit in which we use `matchUpSigWithDecl` to determine the binders of a promoted class declaration, in which case we will need to be able to tell invisible binders from visible ones. --- .../src/Data/Singletons/TH/Single/Data.hs | 21 ++++++++++- singletons-th/src/Data/Singletons/TH/Util.hs | 37 +++++++++++++------ 2 files changed, 46 insertions(+), 12 deletions(-) diff --git a/singletons-th/src/Data/Singletons/TH/Single/Data.hs b/singletons-th/src/Data/Singletons/TH/Single/Data.hs index 8df30cbb..27932aa5 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Data.hs +++ b/singletons-th/src/Data/Singletons/TH/Single/Data.hs @@ -329,10 +329,29 @@ singDataSAK data_sak data_bndrs data_k = do Map.fromList $ zip invis_data_sak_arg_nms invis_data_bndr_nms (_, swizzled_sing_sak_tvbs) = mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs + swizzled_sing_sak_tvbs' = + map (fmap mk_data_sak_spec) swizzled_sing_sak_tvbs -- (4) Finally, construct the kind of the singled data type. - pure $ DForallT (DForallInvis swizzled_sing_sak_tvbs) + pure $ DForallT (DForallInvis swizzled_sing_sak_tvbs') $ DArrowT `DAppT` data_k `DAppT` DConT typeKindName + where + -- Convert a ForAllTyFlag value to a Specificity value, i.e., a binder + -- suitable for use in an invisible `forall`. We convert Required values + -- to SpecifiedSpec values because all of the binders in the `forall` are + -- invisible. For instance, we would single this data type: + -- + -- type T :: forall k -> k -> Type + -- data T k (a :: k) where ... + -- + -- Like so: + -- + -- -- Note: the `k` is invisible, not visible + -- type ST :: forall k (a :: k). T k a -> Type + -- data ST z where ... + mk_data_sak_spec :: ForAllTyFlag -> Specificity + mk_data_sak_spec (Invisible spec) = spec + mk_data_sak_spec Required = SpecifiedSpec {- Note [singletons-th and record selectors] diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index a0398151..6bbf8504 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -744,7 +744,7 @@ matchUpSigWithDecl :: -- ^ The quantifiers in the declaration's standalone kind signature -> [DTyVarBndrVis] -- ^ The user-written binders in the declaration - -> q [DTyVarBndrSpec] + -> q [DTyVarBndr ForAllTyFlag] matchUpSigWithDecl = go_fun_args Map.empty where go_fun_args :: @@ -764,7 +764,7 @@ matchUpSigWithDecl = go_fun_args Map.empty -- extended with @[a :-> x, b :-> y]@. This ensures that we will -- produce @Maybe (x, y)@ instead of @Maybe (a, b)@ in -- the kind for @z@. - -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec] + -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] go_fun_args _ DFANil [] = pure [] -- This should not happen, per the function's precondition @@ -790,12 +790,12 @@ matchUpSigWithDecl = go_fun_args Map.empty let mb_match_subst = matchTy NoIgnore decl_bndr_kind anon' in maybe decl_bndr_kind (`substType` decl_bndr_kind) mb_match_subst sig_args' <- go_fun_args subst sig_args decl_bndrs - pure $ DKindedTV decl_bndr_name SpecifiedSpec anon'' : sig_args' + pure $ DKindedTV decl_bndr_name Required anon'' : sig_args' -- This should not happen, per precondition (1). go_fun_args _ _ [] = fail "matchUpSigWithDecl.go_fun_args: Too few binders" - go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec] + go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] go_invis_tvbs subst [] sig_args decl_bndrs = go_fun_args subst sig_args decl_bndrs -- This should not happen, per precondition (2). @@ -809,15 +809,15 @@ matchUpSigWithDecl = go_fun_args Map.empty BndrReq -> do let (subst', invis_tvb') = substTvb subst invis_tvb sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss - pure $ invis_tvb' : sig_args' + pure $ fmap Invisible invis_tvb' : sig_args' -- If the next decl_bndr is an invisible @-binder, then we must match it -- against the invisible forall–bound variable in the kind. BndrInvis -> do let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs - pure (sig_tvb : sig_args') + pure (fmap Invisible sig_tvb : sig_args') - go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec] + go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] go_vis_tvbs subst [] sig_args decl_bndrs = go_fun_args subst sig_args decl_bndrs -- This should not happen, per precondition (1). @@ -830,7 +830,7 @@ matchUpSigWithDecl = go_fun_args Map.empty BndrReq -> do let (subst', sig_tvb) = match_tvbs subst vis_tvb decl_bndr sig_args' <- go_vis_tvbs subst' vis_tvbs sig_args decl_bndrs - pure (sig_tvb : sig_args') + pure ((Required <$ sig_tvb) : sig_args') -- We have a visible forall in the kind, but an invisible @-binder as -- the next decl_bndr. This is ill kinded, so throw an error. BndrInvis -> @@ -847,12 +847,13 @@ matchUpSigWithDecl = go_fun_args Map.empty -- -- 2. A 'DTyVarBndrSpec' that has the name of @decl_bndr@, but with the new -- kind resulting from matching. - match_tvbs :: DSubst -> DTyVarBndr flag -> DTyVarBndrVis -> (DSubst, DTyVarBndrSpec) + match_tvbs :: DSubst -> DTyVarBndr flag -> DTyVarBndrVis -> (DSubst, DTyVarBndr flag) match_tvbs subst sig_tvb decl_bndr = let decl_bndr_name = extractTvbName decl_bndr mb_decl_bndr_kind = extractTvbKind decl_bndr sig_tvb_name = extractTvbName sig_tvb + sig_tvb_flag = extractTvbFlag sig_tvb mb_sig_tvb_kind = substType subst <$> extractTvbKind sig_tvb mb_kind :: Maybe DKind @@ -867,8 +868,8 @@ matchUpSigWithDecl = go_fun_args Map.empty subst' = Map.insert sig_tvb_name (DVarT decl_bndr_name) subst sig_tvb' = case mb_kind of - Nothing -> DPlainTV decl_bndr_name SpecifiedSpec - Just kind -> DKindedTV decl_bndr_name SpecifiedSpec kind in + Nothing -> DPlainTV decl_bndr_name sig_tvb_flag + Just kind -> DKindedTV decl_bndr_name sig_tvb_flag kind in (subst', sig_tvb') @@ -885,3 +886,17 @@ swizzleTvb swizzle_env subst tvb = case Map.lookup tvb_name swizzle_env of Just user_name -> mapDTVName (const user_name) tvb1 Nothing -> tvb1 + +-- The visibility of a binder in a type-level declaration. This generalizes +-- 'Specificity' (which lacks an equivalent to 'Required') and 'BndrVis' (which +-- lacks an equivalent to @'Invisible' 'Inferred'@). +-- +-- This is heavily inspired by a data type of the same name in GHC: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/98597ad5fca81544d74f721fb508295fd2650232/compiler/GHC/Types/Var.hs#L458-465 +data ForAllTyFlag + = Invisible !Specificity + -- ^ If the 'Specificity' value is 'SpecifiedSpec', then the binder is + -- permitted by request. If the 'Specificity' value is 'InferredSpec', then + -- the binder is prohibited from appearing in source Haskell. + | Required + -- ^ The binder is required to appear in source Haskell