[Git][ghc/ghc][wip/soulomoon/suggest-UnliftedNewtypes-unlifted-data-family-25593] update Note [Kind inference for data family instances]

[Patrick (@soulomoon)]

Patrick pushed to branch wip/soulomoon/suggest-UnliftedNewtypes-unlifted-data-family-25593 at Glasgow Haskell Compiler / GHC


Commits:
c25bac01 by Patrick at 2025-01-08T22:51:56+08:00
update Note [Kind inference for data family instances]

- - - - -


1 changed file:

- compiler/GHC/Tc/TyCl/Instance.hs


Changes:

=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1196,28 +1196,43 @@ constraints arising from the data constructors should be considered
 local to the (GADT) data /constructor/ or should apply to the entire
 data instance.
 
-DESIGN CHOICE: in data/newtype family instance declarations, we take
-the /data constructor/ declarations into accound for Haskell-98 style
-data-instance and newtype-instance declarations. But for general
-GADT-style data-instance declarations, we are looking only at the data
-instance /header/.
+DESIGN CHOICE: in a data/newtype family instance declaration:
+* We take account of the data constructors (via `kcConDecls`) for
+  * Haskell-98 style data instance declarations
+  * All newtype instance declarations
+  For H-98 style declarations there is no GADT refinement. And for
+  GADT-style newtype declarations, no GADT matching is allowed anyway,
+  so it's just a syntactic difference from H-98.
 
-Observations:
-* We treat Haskell-98 style data-instance decls differently, by taking
-  the data constructors into account, since there are no GADT
-  issues.
+* We /ignore/ the data constructors for
+  * GADT-style data instance declarations
+  Here the instance kinds are influenced only by the header.
 
-* Newtypes can be declared in GADT syntax, but they can't do GADT-style
-  specialisation, so like Haskell-98 definitions we can take the
-  data constructors into account.
+This choice is implemented by the guarded call to `kcConDecls` in
+`tcDataFamInstHeader`.
 
+Observations:
 * With UnliftedNewtypes or UnliftedDatatypes, looking at the data
-  constructors is necessary to infer the kind of result type for certain
-  cases. Otherwise addtional kind signatures are required(see #25611).
-
-
-We are balancing between well rounded kind inference and the implementation
-simplicity. See #25611, #18891 and !4419 for more discussion of this issue.
+  constructors is necessary to infer the kind of result type for
+  certain cases. Otherwise addtional kind signatures are required.
+  Consider the following example in #25611:
+
+    data family Fix :: (k -> Type) -> k
+    newtype instance Fix f = In { out :: f (Fix f) }
+
+  If we are not looking at the data constructors.
+  * Without UnliftedNewtypes, it is accepted since `Fix f` is defaulted
+    to Type.
+  * But with UnliftedNewtypes, `Fix f` is defaulted to `TYPE a` where
+    a is not scoped over the data constructor. Then header `Fix f :: TYPE a`
+    will fail to kind unify with `f (Fix f) :: Type`.
+
+  Hence we need to look at the data constructor to infer `Fix f :: TYPE`
+  for this newtype instance.
+
+This DESIGN CHOICE strikes a balance between well rounded kind inference
+and the implementation simplicity. See #25611, #18891 and !4419 for more
+discussion of this issue.
 
 Kind inference for data types (Xie et al) https://arxiv.org/abs/1911.06153
 takes a slightly different approach.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c25bac01f724132dd8a96aa44837ad18fa2e5484

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c25bac01f724132dd8a96aa44837ad18fa2e5484
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20250108/944c4859/attachment-0001.html>