Draft: T199 T220 improve reification w.r.t. SAKs

TODO RGS: Finish me
TODO RGS: Cite T199 and T220

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]
 -------------------------

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,19 +1004,18 @@ 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
   return $ flip map dcons' $ \(n, dtvbs, dcxt, fields, m_gadt_type) ->
     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

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,17 +649,15 @@ 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.
             -> Con -> Type
 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 []