From b93062124237ae596e4dcf389816addf2dcf6ab4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 6 Jul 2024 20:51:45 -0400 Subject: [PATCH] Draft: T199 T220 improve reification w.r.t. SAKs TODO RGS: Finish me TODO RGS: Cite T199 and T220 --- CHANGES.md | 2 + Language/Haskell/TH/Desugar/Core.hs | 32 +++-- Language/Haskell/TH/Desugar/Reify.hs | 202 +++++++++++++++++++++------ Test/Run.hs | 80 +++++++++++ 4 files changed, 262 insertions(+), 54 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 74d9b55..4e9fbe0 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -51,6 +51,8 @@ Version 1.18 [????.??.??] * Also add `matchUpSAKWithDecl`, `tvbForAllTyFlagsToSpecs`, and `tvbForAllTyFlagsToBndrVis` functions, which work over `TyVarBndr` instead of `DTyVarBndr`. +* TODO RGS: Improved reification changes wrt T199 and T220. (Don't forget that + the type of `dsCon` has changed!) Version 1.17 [2024.05.12] ------------------------- diff --git a/Language/Haskell/TH/Desugar/Core.hs b/Language/Haskell/TH/Desugar/Core.hs index 0b50b81..a5671f0 100644 --- a/Language/Haskell/TH/Desugar/Core.hs +++ b/Language/Haskell/TH/Desugar/Core.hs @@ -827,12 +827,19 @@ dsDataDec :: DsMonad q -> Maybe Kind -> [Con] -> [DerivingClause] -> q [DDec] dsDataDec nd cxt n tvbs mk cons derivings = do tvbs' <- mapM dsTvbVis tvbs - let h98_tvbs = case mk of - -- If there's an explicit return kind, we're dealing with a - -- GADT, so this argument goes unused in dsCon. - Just {} -> unusedArgument - Nothing -> tvbs' - h98_return_type = nonFamilyDataReturnType n tvbs' + h98_tvbs <- + case mk of + -- If there's an explicit return kind, we're dealing with a + -- GADT, so this argument goes unused in dsCon. + Just {} -> pure unusedArgument + -- TODO RGS: Docs + Nothing -> do + mb_sak <- dsReifyType n + let tvbSpecs = changeDTVFlags SpecifiedSpec tvbs' + pure $ maybe tvbSpecs dtvbForAllTyFlagsToSpecs $ do + sak <- mb_sak + dMatchUpSAKWithDecl sak tvbs' + let h98_return_type = nonFamilyDataReturnType n tvbs' (:[]) <$> (DDataD nd <$> dsCxt cxt <*> pure n <*> pure tvbs' <*> mapM dsType mk <*> concatMapM (dsCon h98_tvbs h98_return_type) cons @@ -847,7 +854,7 @@ dsDataInstDec nd cxt n mtvbs tys mk cons derivings = do tys' <- mapM dsTypeArg tys let lhs' = applyDType (DConT n) tys' h98_tvbs = - changeDTVFlags defaultBndrFlag $ + changeDTVFlags SpecifiedSpec $ case (mk, mtvbs') of -- If there's an explicit return kind, we're dealing with a -- GADT, so this argument goes unused in dsCon. @@ -997,10 +1004,10 @@ dsTopLevelLetDec = fmap (map DLetDec . fst) . dsLetDec -- we require passing these as arguments. (If we desugar an actual GADT -- constructor, these arguments are ignored.) dsCon :: DsMonad q - => [DTyVarBndrVis] -- ^ The universally quantified type variables - -- (used if desugaring a non-GADT constructor). - -> DType -- ^ The original data declaration's type - -- (used if desugaring a non-GADT constructor). + => [DTyVarBndrSpec] -- ^ The universally quantified type variables + -- (used if desugaring a non-GADT constructor). + -> DType -- ^ The original data declaration's type + -- (used if desugaring a non-GADT constructor). -> Con -> q [DCon] dsCon univ_dtvbs data_type con = do dcons' <- dsCon' con @@ -1008,8 +1015,7 @@ dsCon univ_dtvbs data_type con = do case m_gadt_type of Nothing -> let ex_dtvbs = dtvbs - expl_dtvbs = changeDTVFlags SpecifiedSpec univ_dtvbs ++ - ex_dtvbs + expl_dtvbs = univ_dtvbs ++ ex_dtvbs impl_dtvbs = changeDTVFlags SpecifiedSpec $ toposortKindVarsOfTvbs expl_dtvbs in DCon (impl_dtvbs ++ expl_dtvbs) dcxt n fields data_type diff --git a/Language/Haskell/TH/Desugar/Reify.hs b/Language/Haskell/TH/Desugar/Reify.hs index eccadac..2ba05ff 100644 --- a/Language/Haskell/TH/Desugar/Reify.hs +++ b/Language/Haskell/TH/Desugar/Reify.hs @@ -283,14 +283,47 @@ reifyInDec n _ dec@(TypeDataD n' _ _ _) | n `nameMatches` n' = Just (n', TyConI #endif reifyInDec n decs (DataD _ ty_name tvbs _mk cons _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name tvbs' h98_res_ty cons = Just info + where + -- TODO RGS: Docs, factor this out + tvbs' :: [TyVarBndrSpec] + tvbs' = + fromMaybe (changeTVFlags SpecifiedSpec tvbs) $ do + sak <- findKind False ty_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl sak tvbs + + -- TODO RGS: Factor out? + h98_res_ty :: Type + h98_res_ty = applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs) reifyInDec n decs (NewtypeD _ ty_name tvbs _mk con _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) [con] + | Just info <- maybeReifyCon n decs ty_name tvbs' h98_res_ty [con] = Just info -reifyInDec n _decs (ClassD _ ty_name tvbs _ sub_decs) + where + -- TODO RGS: Docs, factor this out + tvbs' :: [TyVarBndrSpec] + tvbs' = + fromMaybe (changeTVFlags SpecifiedSpec tvbs) $ do + sak <- findKind False ty_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl sak tvbs + + -- TODO RGS: Factor out? + h98_res_ty :: Type + h98_res_ty = applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs) +reifyInDec n decs (ClassD _ cls_name cls_tvbs _ sub_decs) | Just (n', ty) <- findType n sub_decs - = Just (n', ClassOpI n (quantifyClassMethodType ty_name tvbs True ty) ty_name) + = Just (n', ClassOpI n (quantifyClassMethodType cls_tvbs' cls_pred True ty) cls_name) + where + -- TODO RGS: Docs, factor this out + cls_tvbs' :: [TyVarBndrSpec] + cls_tvbs' = + fromMaybe (changeTVFlags SpecifiedSpec cls_tvbs) $ do + cls_sak <- findKind False cls_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl cls_sak cls_tvbs + + -- TODO RGS: Factor out? + cls_pred :: Pred + cls_pred = applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs) reifyInDec n decs (ClassD _ _ _ _ sub_decs) | Just info <- firstMatch (reifyInDec n decs) sub_decs -- Important: don't pass (sub_decs ++ decs) to reifyInDec @@ -310,32 +343,108 @@ reifyInDec n decs (PatSynD pat_syn_name args _ _) = Just (n', VarI n full_sel_ty Nothing) #endif #if __GLASGOW_HASKELL__ >= 807 -reifyInDec n decs (DataInstD _ _ lhs _ cons _) +reifyInDec n decs (DataInstD _ mtvbs lhs _ cons _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys cons + , Just info <- maybeReifyCon n decs ty_name + (mk_tvbs tys) (mk_h98_res_ty ty_name tys) cons = Just info -reifyInDec n decs (NewtypeInstD _ _ lhs _ con _) + where + -- TODO RGS: Docs, factor this out + mk_tvbs :: [TypeArg] -> [TyVarBndrSpec] + mk_tvbs tys = + changeTVFlags SpecifiedSpec $ + case mtvbs of + Just tvbs -> + tvbs + Nothing -> + freeVariablesWellScoped $ + map probablyWrongUnTypeArg tys + + -- TODO RGS: Why do we compute this instead of just reusing `lhs`? Explain + -- that it's necessary to preserve GHC's behavior when looking up infix + -- names, which don't use InfixT. (Cite the R40 test case as an example.) + mk_h98_res_ty :: Name -> [TypeArg] -> Type + mk_h98_res_ty ty_name tys = applyType (ConT ty_name) tys +reifyInDec n decs (NewtypeInstD _ mtvbs lhs _ con _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys [con] + , Just info <- maybeReifyCon n decs ty_name + (mk_tvbs tys) (mk_h98_res_ty ty_name tys) [con] = Just info + where + -- TODO RGS: Docs, factor this out + mk_tvbs :: [TypeArg] -> [TyVarBndrSpec] + mk_tvbs tys = + changeTVFlags SpecifiedSpec $ + case mtvbs of + Just tvbs -> + tvbs + Nothing -> + freeVariablesWellScoped $ + map probablyWrongUnTypeArg tys + + -- TODO RGS: Why do we compute this instead of just reusing `lhs`? Explain + -- that it's necessary to preserve GHC's behavior when looking up infix + -- names, which don't use InfixT. (Cite the R40 test case as an example.) + mk_h98_res_ty :: Name -> [TypeArg] -> Type + mk_h98_res_ty ty_name tys = applyType (ConT ty_name) tys #else reifyInDec n decs (DataInstD _ ty_name tys _ cons _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) cons + | Just info <- maybeReifyCon n decs ty_name tvbs h98_res_ty cons = Just info + where + -- TODO RGS: Docs, factor this out + tvbs :: [TyVarBndrSpec] + tvbs = + changeTVFlags SpecifiedSpec $ + freeVariablesWellScoped tys + + -- TODO RGS: Factor out? + h98_res_ty :: Type + h98_res_ty = applyType (ConT ty_name) (map TANormal tys) reifyInDec n decs (NewtypeInstD _ ty_name tys _ con _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) [con] + | Just info <- maybeReifyCon n decs ty_name tvbs h98_res_ty [con] = Just info + where + -- TODO RGS: Docs, factor this out + tvbs :: [TyVarBndrSpec] + tvbs = + changeTVFlags SpecifiedSpec $ + freeVariablesWellScoped tys + + -- TODO RGS: Factor out? + h98_res_ty :: Type + h98_res_ty = applyType (ConT ty_name) (map TANormal tys) #endif #if __GLASGOW_HASKELL__ >= 906 reifyInDec n decs (TypeDataD ty_name tvbs _mk cons) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name tvbs' h98_res_ty cons = Just info + where + -- TODO RGS: Docs, factor this out + tvbs' :: [TyVarBndrSpec] + tvbs' = + fromMaybe (changeTVFlags SpecifiedSpec tvbs) $ do + sak <- findKind False ty_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl sak tvbs + + -- TODO RGS: Factor out? + h98_res_ty :: Type + h98_res_ty = applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs) #endif reifyInDec _ _ _ = Nothing -maybeReifyCon :: Name -> [Dec] -> Name -> [TypeArg] -> [Con] -> Maybe (Named Info) -maybeReifyCon n _decs ty_name ty_args cons +maybeReifyCon :: + Name + -> [Dec] + -> Name + -> [TyVarBndrSpec] + -- ^ TODO RGS: Docs + -> Type + -- ^ TODO RGS: Docs + -> [Con] + -> Maybe (Named Info) +maybeReifyCon n _decs ty_name h98_tvbs h98_res_ty cons | Just (n', con) <- findCon n cons -- See Note [Use unSigType in maybeReifyCon] , let full_con_ty = unSigType $ con_to_type h98_tvbs h98_res_ty con @@ -355,7 +464,11 @@ maybeReifyCon n _decs ty_name ty_args cons extract_rec_sel_info rec_sel_info = case rec_sel_info of RecSelH98 sel_ty -> - ( changeTVFlags SpecifiedSpec h98_tvbs + let -- TODO RGS: Docs, factor out? + all_h98_tvbs = + let h98_kvbs = freeKindVariablesWellScoped h98_tvbs in + changeTVFlags SpecifiedSpec h98_kvbs ++ h98_tvbs in + ( all_h98_tvbs , sel_ty , h98_res_ty ) @@ -374,11 +487,7 @@ maybeReifyCon n _decs ty_name ty_args cons , con_res_ty ) - h98_tvbs = freeVariablesWellScoped $ - map probablyWrongUnTypeArg ty_args - h98_res_ty = applyType (ConT ty_name) ty_args - -maybeReifyCon _ _ _ _ _ = Nothing +maybeReifyCon _ _ _ _ _ _ = Nothing #if __GLASGOW_HASKELL__ >= 801 -- | Attempt to reify the type of a pattern synonym record selector @n@. @@ -540,7 +649,7 @@ This is contrast to GHC's own reification, which will produce `D a` -} -- Reverse-engineer the type of a data constructor. -con_to_type :: [TyVarBndrUnit] -- The type variables bound by a data type head. +con_to_type :: [TyVarBndrSpec] -- The type variables bound by a data type head. -- Only used for Haskell98-style constructors. -> Type -- The constructor result type. -- Only used for Haskell98-style constructors. @@ -548,9 +657,7 @@ con_to_type :: [TyVarBndrUnit] -- The type variables bound by a data type head. con_to_type h98_tvbs h98_result_ty con = case go con of (is_gadt, ty) | is_gadt -> ty - | otherwise -> maybeForallT - (changeTVFlags SpecifiedSpec h98_tvbs) - [] ty + | otherwise -> maybeForallT all_h98_tvbs [] ty where -- Note that we deliberately ignore linear types and use (->) everywhere. -- See [Gracefully handling linear types] in L.H.TH.Desugar.Core. @@ -562,6 +669,12 @@ con_to_type h98_tvbs h98_result_ty con = go (GadtC _ stys rty) = (True, mkArrows (map snd stys) rty) go (RecGadtC _ vstys rty) = (True, mkArrows (map thdOf3 vstys) rty) + -- TODO RGS: Docs, factor out? + all_h98_tvbs :: [TyVarBndrSpec] + all_h98_tvbs = + let h98_kvbs = freeKindVariablesWellScoped h98_tvbs in + changeTVFlags SpecifiedSpec h98_kvbs ++ h98_tvbs + mkVarI :: Name -> [Dec] -> Info mkVarI n decs = mkVarITy n (maybe (no_type n) snd $ findType n decs) @@ -710,7 +823,11 @@ quantifyClassDecMethods (ClassD cxt cls_name cls_tvbs fds sub_decs) sub_decs' = mapMaybe go sub_decs go (SigD n ty) = Just $ SigD n - $ quantifyClassMethodType cls_name cls_tvbs prepend_cls ty + $ quantifyClassMethodType + (changeTVFlags SpecifiedSpec cls_tvbs) + (applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)) + prepend_cls + ty go d@(TySynInstD {}) = Just d go d@(OpenTypeFamilyD {}) = Just d go d@(DataFamilyD {}) = Just d @@ -731,8 +848,8 @@ quantifyClassDecMethods dec = dec -- [d| class C a where -- method :: a -> b -> a |] -- --- If one invokes `quantifyClassMethodType C [a] prepend (a -> b -> a)`, then --- the output will be: +-- If one invokes `quantifyClassMethodType [a] (C a) prepend (a -> b -> a)`, +-- then the output will be: -- -- 1. `forall a. C a => forall b. a -> b -> a` (if `prepend` is True) -- 2. `forall b. a -> b -> a` (if `prepend` is False) @@ -744,22 +861,19 @@ quantifyClassDecMethods dec = dec -- a single class method, like `method`, then one needs the class context to -- appear in the reified type, so `True` is appropriate. quantifyClassMethodType - :: Name -- ^ The class name. - -> [TyVarBndrVis] -- ^ The class's type variable binders. - -> Bool -- ^ If 'True', prepend a class predicate. - -> Type -- ^ The method type. + :: [TyVarBndrSpec] -- ^ The class's type variable binders. + -> Pred -- ^ The class context. + -> Bool -- ^ If 'True', prepend a class predicate. + -> Type -- ^ The method type. -> Type -quantifyClassMethodType cls_name cls_tvbs prepend meth_ty = +quantifyClassMethodType cls_tvbs cls_pred prepend meth_ty = add_cls_cxt quantified_meth_ty where add_cls_cxt :: Type -> Type add_cls_cxt - | prepend = ForallT (changeTVFlags SpecifiedSpec all_cls_tvbs) cls_cxt + | prepend = ForallT all_cls_tvbs [cls_pred] | otherwise = id - cls_cxt :: Cxt - cls_cxt = [applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)] - quantified_meth_ty :: Type quantified_meth_ty | null meth_tvbs @@ -770,13 +884,19 @@ quantifyClassMethodType cls_name cls_tvbs prepend meth_ty = = ForallT meth_tvbs [] meth_ty meth_tvbs :: [TyVarBndrSpec] - meth_tvbs = changeTVFlags SpecifiedSpec $ - List.deleteFirstsBy ((==) `on` tvName) - (freeVariablesWellScoped [meth_ty]) all_cls_tvbs + meth_tvbs = List.deleteFirstsBy ((==) `on` tvName) + (changeTVFlags SpecifiedSpec + (freeVariablesWellScoped [meth_ty])) + all_cls_tvbs - -- Explicitly quantify any kind variables bound by the class, if any. - all_cls_tvbs :: [TyVarBndrUnit] - all_cls_tvbs = freeVariablesWellScoped $ map tvbToTypeWithSig cls_tvbs + -- All of the type variables bound by the class, with any implicitly + -- quantified kind variables made explicit. + -- + -- TODO RGS: Factor this out? + all_cls_tvbs :: [TyVarBndrSpec] + all_cls_tvbs = + let cls_kvbs = freeKindVariablesWellScoped cls_tvbs in + changeTVFlags SpecifiedSpec cls_kvbs ++ cls_tvbs stripInstanceDec :: Dec -> Dec stripInstanceDec (InstanceD over cxt ty _) = InstanceD over cxt ty [] diff --git a/Test/Run.hs b/Test/Run.hs index 194fe42..1cee404 100644 --- a/Test/Run.hs +++ b/Test/Run.hs @@ -72,6 +72,8 @@ import qualified Data.Map as M import Data.Proxy #if __GLASGOW_HASKELL__ >= 900 +import qualified Control.Monad.Trans as Trans +import Data.Kind (Constraint) import Prelude as P #endif @@ -696,6 +698,45 @@ test_t188 = toposortKindVarsOfTvbs [DKindedTV a1 () (DVarT a2), DKindedTV a2 () (DVarT a1)] == [DPlainTV a2 ()] +#if __GLASGOW_HASKELL__ >= 900 +-- TODO RGS: What does this test do? +test_t199 :: [Bool] +test_t199 = + $(do decs <- [d| type P :: forall {k}. k -> Type + data P (a :: k) = MkP |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + p = mkName "P" + mkP = mkName "MkP" + pTy = DConT p `DAppT` DVarT a + mbPInfo <- dsReify p + let b1 = + case mbPInfo of + Just (DTyConI (DDataD _ _ _ _ _ [conActual] _) _) -> + let conExpected = + DCon [kTvb, aTvb] [] mkP (DNormalC False []) pTy in + conExpected `eqTH` conActual + _ -> + False + + mbMkPInfo <- dsReify mkP + let b2 = + case mbMkPInfo of + Just (DVarI _ conTyActual _) -> + let conTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) pTy in + conTyExpected `eqTH` conTyActual + _ -> + False + + -- TODO RGS: Define Quote instance for DsM? + Trans.lift [| [b1, b2] |]) +#endif + -- Unit tests for unboxedTupleNameDegree_maybe and unboxedSumNameDegree_maybe. -- These also act as a regression test for #213. test_t213 :: [Bool] @@ -740,6 +781,36 @@ test_t213 = ] #endif +#if __GLASGOW_HASKELL__ >= 900 +-- TODO RGS: What does this test do? +test_t220 :: Bool +test_t220 = + $(do decs <- [d| type C :: forall {k}. k -> Constraint + class C (a :: k) where + m :: Proxy a |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + c = mkName "C" + m = mkName "m" + cTy = DConT c `DAppT` DVarT a + mbMInfo <- dsReify m + -- TODO RGS: Define Quote instance for DsM? + Trans.lift $ + case mbMInfo of + Just (DVarI _ mTyActual _) -> + let mTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) $ + DConstrainedT [cTy] $ + DConT ''Proxy `DAppT` DVarT a in + mTyExpected `eqTHSplice` mTyActual + _ -> + [| False |]) +#endif + -- Unit tests for functions that compute free variables (e.g., fvDType) test_fvs :: [Bool] test_fvs = @@ -979,9 +1050,18 @@ main = hspec $ do it "computes free kind variables correctly in a telescope that uses shadowing" $ test_t188 +#if __GLASGOW_HASKELL__ >= 900 + zipWithM (\b n -> it ("correctly reifies the type of a data constructor with an inferred type variable binder " ++ show n) b) + test_t199 [1..] +#endif + zipWithM (\b n -> it ("recognizes unboxed {tuple,sum} names with unboxed{Tuple,Sum}Degree_maybe correctly " ++ show n) b) test_t213 [1..] +#if __GLASGOW_HASKELL__ >= 900 + it "correctly reifies the type of a class method with an inferred type variable binder" $ test_t220 +#endif + -- Remove map pprints here after switch to th-orphans zipWithM (\t t' -> it ("can do Type->DType->Type of " ++ t) $ t == t') $(sequence round_trip_types >>= Syn.lift . map pprint)