diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index 9e30f111..b3a5e37a 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -720,18 +720,19 @@ mapAndUnzip3M f (x:xs) = do isHsLetter :: Char -> Bool isHsLetter c = isLetter c || c == '_' --- Match the quantifiers in a data type's standalone kind signature with the --- binders in the data type declaration. This function assumes the following --- preconditions: +-- Match the quantifiers in a type-level declaration's standalone kind signature +-- with the user-written binders in the declaration. This function assumes the +-- following preconditions: -- --- 1. The number of required binders in the data type declaration is equal to --- the number of visible quantifiers (i.e., the number of function arrows --- plus the number of visible @forall@–bound variables) in the standalone --- kind signature. +-- 1. The number of required binders in the declaration's user-written binders +-- is equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- the standalone kind signature. -- --- 2. The number of invisible \@-binders in the data type declaration is less --- than or equal to the number of invisible quantifiers (i.e., the number of --- invisible @forall@–bound variables) in the standalone kind signature. +-- 2. The number of invisible \@-binders in the declaration's user-written +-- binders is less than or equal to the number of invisible quantifiers +-- (i.e., the number of invisible @forall@–bound variables) in the +-- standalone kind signature. -- -- The implementation of this function is heavily based on a GHC function of -- the same name: @@ -740,9 +741,9 @@ matchUpSigWithDecl :: forall q. MonadFail q => DFunArgs - -- ^ The quantifiers in the data type's standalone kind signature + -- ^ The quantifiers in the declaration's standalone kind signature -> [DTyVarBndrVis] - -- ^ The user-written binders in the data type declaration + -- ^ The user-written binders in the declaration -> q [DTyVarBndrSpec] matchUpSigWithDecl = go_fun_args Map.empty where @@ -767,107 +768,107 @@ matchUpSigWithDecl = go_fun_args Map.empty go_fun_args _ DFANil [] = pure [] -- This should not happen, per the function's precondition - go_fun_args _ DFANil data_bndrs = - fail $ "matchUpSigWithDecl.go_fun_args: Too many binders: " ++ show data_bndrs + go_fun_args _ DFANil decl_bndrs = + fail $ "matchUpSigWithDecl.go_fun_args: Too many binders: " ++ show decl_bndrs -- GHC now disallows kind-level constraints, per this GHC proposal: -- https://github.com/ghc-proposals/ghc-proposals/blob/b0687d96ce8007294173b7f628042ac4260cc738/proposals/0547-no-kind-equalities.rst go_fun_args _ (DFACxt{}) _ = fail "matchUpSigWithDecl.go_fun_args: Unexpected kind-level constraint" - go_fun_args subst (DFAForalls (DForallInvis tvbs) sig_args) data_bndrs = - go_invis_tvbs subst tvbs sig_args data_bndrs - go_fun_args subst (DFAForalls (DForallVis tvbs) sig_args) data_bndrs = - go_vis_tvbs subst tvbs sig_args data_bndrs - go_fun_args subst (DFAAnon anon sig_args) (data_bndr:data_bndrs) = do - let data_bndr_name = extractTvbName data_bndr - mb_data_bndr_kind = extractTvbKind data_bndr + go_fun_args subst (DFAForalls (DForallInvis tvbs) sig_args) decl_bndrs = + go_invis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (DFAForalls (DForallVis tvbs) sig_args) decl_bndrs = + go_vis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (DFAAnon anon sig_args) (decl_bndr:decl_bndrs) = do + let decl_bndr_name = extractTvbName decl_bndr + mb_decl_bndr_kind = extractTvbKind decl_bndr anon' = substType subst anon anon'' = - case mb_data_bndr_kind of + case mb_decl_bndr_kind of Nothing -> anon' - Just data_bndr_kind -> - let mb_match_subst = matchTy NoIgnore data_bndr_kind anon' in - maybe data_bndr_kind (`substType` data_bndr_kind) mb_match_subst - sig_args' <- go_fun_args subst sig_args data_bndrs - pure $ DKindedTV data_bndr_name SpecifiedSpec anon'' : sig_args' + Just decl_bndr_kind -> + 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' -- 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 subst [] sig_args data_bndrs = - go_fun_args subst sig_args data_bndrs + go_invis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs -- This should not happen, per precondition (2). go_invis_tvbs _ (_:_) _ [] = fail $ "matchUpSigWithDecl.go_invis_tvbs: Too few binders" - go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args data_bndrss@(data_bndr:data_bndrs) = - case extractTvbFlag data_bndr of - -- If the next data_bndr is required, then we have a invisible forall in + go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss@(decl_bndr:decl_bndrs) = + case extractTvbFlag decl_bndr of + -- If the next decl_bndr is required, then we have a invisible forall in -- the kind without a corresponding invisible @-binder, which is -- allowed. In this case, we simply apply the substitution and recurse. BndrReq -> do let (subst', invis_tvb') = substTvb subst invis_tvb - sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args data_bndrss + sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss pure $ invis_tvb' : sig_args' - -- If the next data_bndr is an invisible @-binder, then we must match it + -- 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 data_bndr - sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args data_bndrs + 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') go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec] - go_vis_tvbs subst [] sig_args data_bndrs = - go_fun_args subst sig_args data_bndrs + go_vis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs -- This should not happen, per precondition (1). go_vis_tvbs _ (_:_) _ [] = fail $ "matchUpSigWithDecl.go_vis_tvbs: Too few binders" - go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (data_bndr:data_bndrs) = do - case extractTvbFlag data_bndr of - -- If the next data_bndr is required, then we must match it against the + go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (decl_bndr:decl_bndrs) = do + case extractTvbFlag decl_bndr of + -- If the next decl_bndr is required, then we must match it against the -- visible forall–bound variable in the kind. BndrReq -> do - let (subst', sig_tvb) = match_tvbs subst vis_tvb data_bndr - sig_args' <- go_vis_tvbs subst' vis_tvbs sig_args data_bndrs + 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') -- We have a visible forall in the kind, but an invisible @-binder as - -- the next data_bndr. This is ill kinded, so throw an error. + -- the next decl_bndr. This is ill kinded, so throw an error. BndrInvis -> fail $ "matchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: " - ++ show data_bndr + ++ show decl_bndr - -- @match_tvbs subst sig_tvb data_bndr@ will match the kind of @data_bndr@ + -- @match_tvbs subst sig_tvb decl_bndr@ will match the kind of @decl_bndr@ -- against the kind of @sig_tvb@ to produce a new kind. This function -- produces two values as output: -- -- 1. A new @subst@ that has been extended such that the name of @sig_tvb@ - -- maps to the name of @data_bndr@. (See the Haddocks for the 'DSubst' + -- maps to the name of @decl_bndr@. (See the Haddocks for the 'DSubst' -- argument to @go_fun_args@ for an explanation of why we do this.) -- - -- 2. A 'DTyVarBndrSpec' that has the name of @data_bndr@, but with the new + -- 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 subst sig_tvb data_bndr = - let data_bndr_name = extractTvbName data_bndr - mb_data_bndr_kind = extractTvbKind data_bndr + 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 mb_sig_tvb_kind = substType subst <$> extractTvbKind sig_tvb mb_kind :: Maybe DKind mb_kind = - case (mb_data_bndr_kind, mb_sig_tvb_kind) of + case (mb_decl_bndr_kind, mb_sig_tvb_kind) of (Nothing, Nothing) -> Nothing - (Just data_bndr_kind, Nothing) -> Just data_bndr_kind + (Just decl_bndr_kind, Nothing) -> Just decl_bndr_kind (Nothing, Just sig_tvb_kind) -> Just sig_tvb_kind - (Just data_bndr_kind, Just sig_tvb_kind) -> do - match_subst <- matchTy NoIgnore data_bndr_kind sig_tvb_kind - Just $ substType match_subst data_bndr_kind + (Just decl_bndr_kind, Just sig_tvb_kind) -> do + match_subst <- matchTy NoIgnore decl_bndr_kind sig_tvb_kind + Just $ substType match_subst decl_bndr_kind - subst' = Map.insert sig_tvb_name (DVarT data_bndr_name) subst + subst' = Map.insert sig_tvb_name (DVarT decl_bndr_name) subst sig_tvb' = case mb_kind of - Nothing -> DPlainTV data_bndr_name SpecifiedSpec - Just kind -> DKindedTV data_bndr_name SpecifiedSpec kind in + Nothing -> DPlainTV decl_bndr_name SpecifiedSpec + Just kind -> DKindedTV decl_bndr_name SpecifiedSpec kind in (subst', sig_tvb')