[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:
b79bf9fc by Patrick at 2025-01-08T17:16:38+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
=====================================
@@ -1198,26 +1198,28 @@ 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 ignore
-the /data constructor/ declarations altogether, looking only at the
-data instance /header/.
+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/.
 
 Observations:
-* This choice is simple to describe, as well as simple to implement.
-  For a data/newtype instance decl, the instance kinds are influenced
-  /only/ by the header.
-
-* We could treat Haskell-98 style data-instance decls differently, by
-  taking the data constructors into account, since there are no GADT
-  issues.  But we don't, for simplicity, and because it means you can
-  understand the data type instance by looking only at the header.
+* We treat Haskell-98 style data-instance decls differently, by taking
+  the data constructors into account, since there are no GADT
+  issues.
 
 * Newtypes can be declared in GADT syntax, but they can't do GADT-style
-  specialisation, so like Haskell-98 definitions we could take the
-  data constructors into account.  Again we don't, for the same reason.
+  specialisation, so like Haskell-98 definitions we can take the
+  data constructors into account.
+
+* 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).
+
 
-So for now at least, we keep the simplest choice. See #18891 and !4419
-for more discussion of this issue.
+We are balancing 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/b79bf9fcae7ebd7d0f76aab721fb9b97d68ad163

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b79bf9fcae7ebd7d0f76aab721fb9b97d68ad163
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/2cf14b3a/attachment-0001.html>