Improve local reification and desugaring with respect to standalone k…

…ind signatures

Previously, `th-desugar` would not take standalone kind signatures into account
when locally reifying a class method (#220). Similarly, it would not take them
into account when locally reifying or desugaring a data constructor (#199).
This patch accomplishes this, mainly by using the `matchUpSAKWithDecl` function
(during local reification) and the `dMatchUpSAKWithDecl` function (during
desugaring) to match up kind information from the standalone kind signature to
the parent declaration's type variable binders.

Fixes #199. Fixes #220.

CHANGES.md

@@ -51,6 +51,40 @@ Version 1.18 [????.??.??]
   * Also add `matchUpSAKWithDecl`, `tvbForAllTyFlagsToSpecs`, and
     `tvbForAllTyFlagsToBndrVis` functions, which work over `TyVarBndr` instead
     of `DTyVarBndr`.
+* Local reifying the type of a data constructor or class method now yields type
+  signatures with more precise type variable information, as `th-desugar` now
+  incorporates information from the standalone kind signature (if any) for the
+  parent data type or class, respectively. For instance, consider the following
+  data type declaration:
+
+  ```hs
+  type P :: forall {k}. k -> Type
+  data P (a :: k) = MkP
+  ```
+
+  In previous versions of `th-desugar`, locally reifying `MkP` would yield the
+  following type:
+
+  ```hs
+  MkP :: forall k (a :: k). P a
+  ```
+
+  This was subtly wrong, as `k` is marked as specified (i.e., eligible for
+  visible type application), not inferred. In `th-desugar-1.18`, however, the
+  locally reified type will mark `k` as inferred, as expected:
+
+  ```hs
+  MkP :: forall {k} (a :: k). P a
+  ```
+
+  Similarly, desugaring `MkP` from Template Haskell to `th-desugar` results
+  in a data constructor with the expected type above.
+  * As a result of these changes, the type of `dsCon` has changed slightly:
+
+    ```diff
+    -dsCon :: DsMonad q => [DTyVarBndrUnit] -> DType -> Con -> q [DCon]
+    +dsCon :: DsMonad q => [DTyVarBndrSpec] -> DType -> Con -> q [DCon]
+    ```
 
 Version 1.17 [2024.05.12]
 -------------------------

Language/Haskell/TH/Desugar/Core.hs

@@ -827,12 +827,25 @@ 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
+      -- If there is no explicit return kind, we're dealing with a
+      -- Haskell98-style data type, so we must compute the type variable
+      -- binders to use in the types of the data constructors.
+      --
+      -- Rather than just returning `tvbs'` here, we propagate kind information
+      -- from the data type's standalone kind signature (if one exists) to make
+      -- the kinds more precise.
+      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 +860,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 +1010,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