[Git][ghc/ghc][wip/soulomoon/suggest-UnliftedNewtypes-unlifted-data-family-25593] update note

[Patrick (@soulomoon)]

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


Commits:
3af75d42 by Patrick at 2025-01-09T14:49:13+08:00
update note

- - - - -


1 changed file:

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


Changes:

=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1010,7 +1010,8 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
     isH98 _ = False
 
     -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2),
-    -- and Note [Implementation of UnliftedDatatypes].
+    -- , Note [Implementation of UnliftedDatatypes]
+    -- and Note [Defaulting newtype/data family instance].
     tc_kind_sig Nothing
       = do { unlifted_newtypes  <- xoptM LangExt.UnliftedNewtypes
            ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes
@@ -1027,6 +1028,8 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
                    -- Perhaps surprisingly, we don't need the skolemised tvs themselves
            ; return inner_kind' }
 
+
+
 {- Note [Result kind signature for a data family instance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The expected type might have a forall at the type. Normally, we
@@ -1036,6 +1039,22 @@ we actually have a place to put the regeneralised variables.
 Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcTopSkolemise
 Examples in indexed-types/should_compile/T12369
 
+Note [Defaulting newtype/data family instance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is tempting to let `tc_kind_sig` just return `newOpenTypeKind`
+even without `-XUnliftedNewtypes`, but we rely on `tc_kind_sig` to
+default the result kind of a newtype instance to `Type` when
+`-XUnliftedNewtypes` is not enabled.
+Consider the following example:
+
+  -- no UnliftedNewtypes
+  data family D :: k -> k
+  newtype instance D a = MkIntD a
+
+`tc_kind_sig` defaulting to `newOpenTypeKind` would result in `D a`
+having kind `forall r. TYPE r` instead of `Type`, which would be
+rejected validity checking. The same applies to Data Instances.
+
 Note [Implementing eta reduction for data families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1190,47 +1209,47 @@ kind -- that came from the family declaration, and is not influenced
 by the data instances -- and hence we /can/ specialise T's kind
 differently in different GADT data constructors.
 
-SHORT SUMMARY: in a data instance decl, it's not clear whether kind
+SHORT SUMMARY: In a data instance decl, it's not clear whether kind
 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 a data/newtype family instance declaration:
-* We take account of the data constructors (via `kcConDecls`) for
+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
+  For Haskell-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.
+  so it's just a syntactic difference from Haskell-98.
 
-* We /ignore/ the data constructors for
+* We /ignore/ the data constructors for:
   * GADT-style data instance declarations
-  Here the instance kinds are influenced only by the header.
+  Here, the instance kinds are influenced only by the header.
 
 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.
+* With `UnliftedNewtypes` or `UnliftedDatatypes`, looking at the data
+  constructors is necessary to infer the kind of the result type for
+  certain cases. Otherwise, additional 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`
+  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 r` where
+    `r` is not scoped over the data constructor. Then the header `Fix f :: TYPE r`
     will fail to kind unify with `f (Fix f) :: Type`.
 
-  Hence we need to look at the data constructor to infer `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
+This DESIGN CHOICE strikes a balance between well-rounded kind inference
+and 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



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

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