[Git][ghc/ghc][wip/soulomoon/suggest-UnliftedNewtypes-unlifted-data-family-25593] 3 commits: user_guide: Note -pgmP/-optP are for /Haskell/-CPP
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Sat Jan 11 08:05:30 UTC 2025
Patrick pushed to branch wip/soulomoon/suggest-UnliftedNewtypes-unlifted-data-family-25593 at Glasgow Haskell Compiler / GHC
Commits:
023f36f5 by Rodrigo Mesquita at 2025-01-10T14:57:48-05:00
user_guide: Note -pgmP/-optP are for /Haskell/-CPP
Fixes #25574
- - - - -
e1c133f2 by Ben Gamari at 2025-01-10T14:58:25-05:00
dump-decls: Suppress unit-ids
While the testsuite driver already normalizes these away, they are
nevertheless a severe nuisance when diffing outside of the testsuite.
Intriguingly, this doesn't completely eliminate the unit IDs; some
wired-in names are still printed. However, this is a cheap and helpful
improvement over the status quo so I am simply going to accept this.
Fixes #25334.
- - - - -
56d509ab by Patrick at 2025-01-11T16:04:36+08:00
Fix #25611. Enhances the kind inference for data family instances,
by including the RHS's constraints when kind-checking LHS.
Type checker changes:
In `tcDataFamInstHeader`, `kcConDecls` the H98-style decls
and newtype decls, even those in GADT syntax, but NOT for
general GADT decls.
Testsuite changes:
1. The test to ensure kind specialization remains correctly handled even
if we include the RHS's constrains:
* T25611d
2. Infer result kind from datacon.
* H98 newtype case: T25611a
* H98 data case: T25611b
3. Two tests with additional errors report:
* UnliftedNewtypesFamilyKindFail2
* UnliftedNewtypesInstanceFail
4. Due to better kind inference,
move should_fail test UnliftedNewtypesUnassociatedFamilyFail
to should_compile test T25611c.
5. Additional test to we default the kind of the data instance correctly
without UnliftedNewtypes or UnliftedDatatypes:
* DataInstanceKindsDefaults
Also a few notes are updated to reflect the changes.
Co-authored-by: Simon Peyton Jones <simon.peytonjones at gmail.com>
- - - - -
18 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- docs/users_guide/phases.rst
- + testsuite/tests/indexed-types/should_compile/dataInstanceKindsDefaults.hs
- testsuite/tests/indexed-types/should_fail/all.T
- + testsuite/tests/rep-poly/DataInstanceKindsDefaults.hs
- + testsuite/tests/rep-poly/T25611a.hs
- + testsuite/tests/rep-poly/T25611b.hs
- + testsuite/tests/rep-poly/T25611c.hs
- + testsuite/tests/rep-poly/T25611d.hs
- testsuite/tests/rep-poly/all.T
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
- − testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
- testsuite/tests/typecheck/should_fail/all.T
- utils/dump-decls/Main.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -42,7 +42,8 @@ module GHC.Tc.Gen.HsType (
-- Type checking type and class decls, and instances thereof
bindTyClTyVars, bindTyClTyVarsAndZonk,
tcFamTyPats,
- etaExpandAlgTyCon, tcbVisibilities,
+ maybeEtaExpandAlgTyCon, tcbVisibilities,
+ etaExpandAlgTyCon,
-- tyvars
zonkAndScopedSort,
@@ -2467,7 +2468,7 @@ kcCheckDeclHeader_cusk name flav
++ map (mkExplicitTyConBinder mentioned_kv_set) tc_bndrs
-- Eta expand if necessary; we are building a PolyTyCon
- ; (eta_tcbs, res_kind) <- etaExpandAlgTyCon flav skol_info all_tcbs res_kind
+ ; (eta_tcbs, res_kind) <- maybeEtaExpandAlgTyCon flav skol_info all_tcbs res_kind
; let all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ binderVars tc_bndrs)
final_tcbs = all_tcbs `chkAppend` eta_tcbs
@@ -3920,14 +3921,20 @@ Hence using zonked_kinds when forming tvs'.
-}
-----------------------------------
-etaExpandAlgTyCon :: TyConFlavour tc -> SkolemInfo
+maybeEtaExpandAlgTyCon :: TyConFlavour tc -> SkolemInfo
-> [TcTyConBinder] -> Kind
-> TcM ([TcTyConBinder], Kind)
-etaExpandAlgTyCon flav skol_info tcbs res_kind
+maybeEtaExpandAlgTyCon flav skol_info tcbs res_kind
| needsEtaExpansion flav
- = splitTyConKind skol_info in_scope avoid_occs res_kind
+ = etaExpandAlgTyCon skol_info tcbs res_kind
| otherwise
= return ([], res_kind)
+
+etaExpandAlgTyCon :: SkolemInfo
+ -> [TcTyConBinder] -> Kind
+ -> TcM ([TcTyConBinder], Kind)
+etaExpandAlgTyCon skol_info tcbs res_kind
+ = splitTyConKind skol_info in_scope avoid_occs res_kind
where
tyvars = binderVars tcbs
in_scope = mkInScopeSetList tyvars
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -1135,7 +1135,7 @@ generaliseTcTyCon (tc, skol_info, scoped_prs, tc_res_kind)
flav = tyConFlavour tc
-- Eta expand
- ; (eta_tcbs, tc_res_kind) <- etaExpandAlgTyCon flav skol_info all_tcbs tc_res_kind
+ ; (eta_tcbs, tc_res_kind) <- maybeEtaExpandAlgTyCon flav skol_info all_tcbs tc_res_kind
-- Step 6: Make the result TcTyCon
; let final_tcbs = all_tcbs `chkAppend` eta_tcbs
@@ -1252,7 +1252,7 @@ paths for
Note that neither code path worries about point (4) above, as this
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
-*after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.)
+*after* all this stuff, in tcDataDefn's call to maybeEtaExpandAlgTyCon.)
We can tell Inferred apart from Specified by looking at the scoped
tyvars; Specified are always included there.
@@ -2123,7 +2123,7 @@ DT3 Eta-expansion: Any forall-bound variables and function arguments in a result
data T a :: Type -> Type where ...
we really mean for T to have two parameters. The second parameter
- is produced by processing the return kind in etaExpandAlgTyCon,
+ is produced by processing the return kind in maybeEtaExpandAlgTyCon,
called in tcDataDefn.
See also Note [splitTyConKind] in GHC.Tc.Gen.HsType.
@@ -2218,14 +2218,20 @@ DF0 Where these kinds come from:
Type. This assumption is in getInitialKind for CUSKs or
get_fam_decl_initial_kind for non-signature & non-CUSK cases.
- Instances: The data family already has a known kind. The return kind
- of an instance is then calculated by applying the data family tycon
- to the patterns provided, as computed by the typeKind lhs_ty in the
- end of tcDataFamInstHeader. In the case of an instance written in GADT
- syntax, there are potentially *two* return kinds: the one computed from
- applying the data family tycon to the patterns, and the one given by
- the user. This second kind is checked by the tc_kind_sig function within
- tcDataFamInstHeader. See also DF3, below.
+ Instances: There are potentially *two* return kinds:
+ * Master kind:
+ The data family already has a known kind. The return kind of an instance
+ is then calculated by applying the data family tycon to the patterns
+ provided, as computed by the `tcFamTyPats fam_tc hs_pats` in the
+ tcDataFamInstHeader.
+ * Instance kind:
+ The kind specified by the user in GADT syntax. If H98 syntax is used,
+ with UnliftedNewtypes/UnliftedDatatypes, it defaults to newOpenTypeKind
+ for newtypes/datatypes, otherwise it defaults to liftedTypeKind.
+ This is checked or defaulted by the tc_kind_sig function within
+ tcDataFamInstHeader. Defaulting can be tricky for some cases,
+ See Note [Defaulting result kind of newtype/data family instance].
+ See also DF3, below.
DF1 In a data/newtype instance, we treat the kind of the /data family/,
once instantiated, as the "master kind" for the representation
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -8,6 +8,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -714,10 +715,9 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
-- Do /not/ check that the number of patterns = tyConArity fam_tc
-- See [Arity of data families] in GHC.Core.FamInstEnv
; skol_info <- mkSkolemInfo FamInstSkol
- ; let new_or_data = dataDefnConsNewOrData hs_cons
; (qtvs, non_user_tvs, pats, tc_res_kind, stupid_theta)
<- tcDataFamInstHeader mb_clsinfo skol_info fam_tc outer_bndrs fixity
- hs_ctxt hs_pats m_ksig new_or_data
+ hs_ctxt hs_pats m_ksig hs_cons
-- Eta-reduce the axiom if possible
-- Quite tricky: see Note [Implementing eta reduction for data families]
@@ -742,8 +742,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
-- we did it before the "extra" tvs from etaExpandAlgTyCon
-- would always be eta-reduced
--
- ; let flav = newOrDataToFlavour new_or_data
- ; (extra_tcbs, tc_res_kind) <- etaExpandAlgTyCon flav skol_info full_tcbs tc_res_kind
+ ; (extra_tcbs, tc_res_kind) <- etaExpandAlgTyCon skol_info full_tcbs tc_res_kind
-- Check the result kind; it may come from a user-written signature.
-- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a)
@@ -917,8 +916,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about.
tcDataFamInstHeader
:: AssocInstInfo -> SkolemInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
-> LexicalFixity -> Maybe (LHsContext GhcRn)
- -> HsFamEqnPats GhcRn -> Maybe (LHsKind GhcRn)
- -> NewOrData
+ -> HsFamEqnPats GhcRn -> Maybe (LHsKind GhcRn) -> DataDefnCons (LConDecl GhcRn)
-> TcM ([TcTyVar], TyVarSet, [TcType], TcKind, TcThetaType)
-- All skolem TcTyVars, all zonked so it's clear what the free vars are
-- The "header" of a data family instance is the part other than
@@ -926,7 +924,7 @@ tcDataFamInstHeader
-- e.g. data instance D [a] :: * -> * where ...
-- Here the "header" is the bit before the "where"
tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
- hs_ctxt hs_pats m_ksig new_or_data
+ hs_ctxt hs_pats m_ksig hs_cons
= do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
; (tclvl, wanted, (outer_bndrs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
<- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
@@ -942,16 +940,17 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
-- with its parent class
; addConsistencyConstraints mb_clsinfo lhs_ty
- -- Add constraints from the result signature
- ; res_kind <- tc_kind_sig m_ksig
-
- -- Do not add constraints from the data constructors
- -- See Note [Kind inference for data family instances]
+ -- Add constraints from the data constructors
+ -- Fix #25611
+ -- See DESIGN CHOICE in Note [Kind inference for data family instances]
+ ; when is_H98_or_newtype $ kcConDecls lhs_applied_kind hs_cons
-- Check that the result kind of the TyCon applied to its args
-- is compatible with the explicit signature (or Type, if there
-- is none)
; let hs_lhs = nlHsTyConApp NotPromoted fixity (getName fam_tc) hs_pats
+ -- Add constraints from the result signature
+ ; res_kind <- tc_kind_sig m_ksig
; _ <- unifyKind (Just . HsTypeRnThing $ unLoc hs_lhs) lhs_applied_kind res_kind
; traceTc "tcDataFamInstHeader" $
@@ -1003,9 +1002,16 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
where
fam_name = tyConName fam_tc
data_ctxt = DataKindCtxt fam_name
+ new_or_data = dataDefnConsNewOrData hs_cons
+ is_H98_or_newtype = case hs_cons of
+ NewTypeCon{} -> True
+ DataTypeCons _ cons -> all isH98 cons
+ isH98 (L _ (ConDeclH98 {})) = True
+ 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 result kind of newtype/data family instance].
tc_kind_sig Nothing
= do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes
@@ -1031,6 +1037,21 @@ 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 result kind of 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
+constrain the result kind of a newtype instance to `Type`.
+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
@@ -1185,31 +1206,48 @@ 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 data/newtype family instance declarations, we ignore
-the /data constructor/ declarations altogether, 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 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 Haskell-98.
-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 /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 could take the
- data constructors into account. Again we don't, for the same reason.
+This choice is implemented by the guarded call to `kcConDecls` in
+`tcDataFamInstHeader`.
-So for now at least, we keep the simplest choice. See #18891 and !4419
-for more discussion of this issue.
+Observations:
+* 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 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`
+ for this newtype instance.
+
+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
takes a slightly different approach.
=====================================
docs/users_guide/phases.rst
=====================================
@@ -25,11 +25,12 @@ given compilation phase:
Use ⟨cmd⟩ as the literate pre-processor.
.. ghc-flag:: -pgmP ⟨cmd⟩
- :shortdesc: Use ⟨cmd⟩ as the C pre-processor (with :ghc-flag:`-cpp` only)
+ :shortdesc: Use ⟨cmd⟩ as the Haskell C pre-processor (with :ghc-flag:`-cpp` only)
:type: dynamic
:category: phase-programs
- Use ⟨cmd⟩ as the C pre-processor (with :ghc-flag:`-cpp` only).
+ Use ⟨cmd⟩ as the Haskell C pre-processor (with :ghc-flag:`-cpp` only).
+ Note that the Haskell C pre-processor only pre-processes Haskell files.
.. ghc-flag:: -pgmJSP ⟨cmd⟩
:shortdesc: Use ⟨cmd⟩ as the JavaScript C pre-processor (only for javascript-backend)
@@ -177,7 +178,11 @@ the following flags:
:type: dynamic
:category: phase-options
- Pass ⟨option⟩ to CPP (makes sense only if :ghc-flag:`-cpp` is also on).
+ Pass ⟨option⟩ to the Haskell CPP (makes sense only if :ghc-flag:`-cpp` is also on).
+ Note that the Haskell pre-processor options only apply to pre-processing
+ invocations on Haskell files, and, e.g., to use different options to
+ pre-process Javascript or Cmm, one should use ``-optJSP``, or
+ ``-optCmmP``, respectively).
.. ghc-flag:: -optJSP ⟨option⟩
:shortdesc: pass ⟨option⟩ to JavaScript C pre-processor (only for javascript-backend)
=====================================
testsuite/tests/indexed-types/should_compile/dataInstanceKindsDefaults.hs
=====================================
@@ -0,0 +1,26 @@
+{-# language DataKinds, PolyKinds, GADTs, TypeFamilies, RankNTypes,
+ TypeOperators, ConstraintKinds #-}
+
+module DataInstanceKindsDefaults where
+
+import Data.Kind
+
+-- This test checks if we default the kind of the data instance correctly without UnliftedNewtypes
+-- or UnliftedDatatypes.
+-- Assumptions:
+-- If we default the result kind of the data instance to `TYPE r`,
+-- then `checkNewDataCon` would through the error since the result kind of the data instance
+-- should be `Type` without UnliftedNewtypes or UnliftedDatatypes.
+
+data family A :: k -> k
+newtype instance A a = MkA a
+
+data family B :: k -> k
+data instance B a = MkB a
+
+data family C :: k -> k
+data instance C a where MkC :: a -> C a
+
+data family D :: k -> k
+newtype instance D a where MkD :: a -> D a
+
=====================================
testsuite/tests/indexed-types/should_fail/all.T
=====================================
@@ -171,4 +171,4 @@ test('T20521', normal, compile_fail, [''])
test('T21896', normal, compile_fail, [''])
test('HsBootFam', [extra_files(['HsBootFam_aux.hs','HsBootFam_aux.hs-boot'])], multimod_compile_fail, ['HsBootFam', ''])
test('BadFamInstDecl', [extra_files(['BadFamInstDecl_aux.hs'])], multimod_compile_fail, ['BadFamInstDecl', ''])
-test('T19773', [], multimod_compile_fail, ['T19773', '-Wall'])
+test('T19773', [], multimod_compile_fail, ['T19773', '-Wall'])
\ No newline at end of file
=====================================
testsuite/tests/rep-poly/DataInstanceKindsDefaults.hs
=====================================
@@ -0,0 +1,26 @@
+{-# language DataKinds, PolyKinds, GADTs, TypeFamilies, RankNTypes,
+ TypeOperators, ConstraintKinds #-}
+
+module DataInstanceKindsDefaults where
+
+import Data.Kind
+
+-- This test checks if we default the kind of the data instance correctly without UnliftedNewtypes
+-- or UnliftedDatatypes.
+-- Assumptions:
+-- If we default the result kind of the data instance to `TYPE r`,
+-- then `checkNewDataCon` would through the error since the result kind of the data instance
+-- should be `Type` without UnliftedNewtypes or UnliftedDatatypes.
+
+data family A :: k -> k
+newtype instance A a = MkA a
+
+data family B :: k -> k
+data instance B a = MkB a
+
+data family C :: k -> k
+data instance C a where MkC :: a -> C a
+
+data family D :: k -> k
+newtype instance D a where MkD :: a -> D a
+
=====================================
testsuite/tests/rep-poly/T25611a.hs
=====================================
@@ -0,0 +1,17 @@
+{-# language DataKinds, PolyKinds, GADTs, TypeFamilies, RankNTypes,
+ TypeOperators, ConstraintKinds, UnliftedNewtypes #-}
+
+module T25611a where
+
+import Data.Kind
+
+-- Enhanced kind inference for data family instance in !13767
+-- this is the h98 newtype instance case
+
+data family Fix0 :: (k -> Type) -> k
+newtype instance Fix0 f = In0 { out0 :: f (Fix0 f) }
+
+-- This is the GADT newtype instance case
+-- currently not enabled since !9116 (closed) impose `A newtype must not be a GADT`
+-- data family Fix2 :: (k -> Type) -> k
+-- newtype instance Fix2 f where In2 :: f (Fix2 f) -> Fix2 f
=====================================
testsuite/tests/rep-poly/T25611b.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+
+module T25611b where
+
+import GHC.Base (Type, TYPE, RuntimeRep (IntRep, BoxedRep), Levity (Unlifted))
+
+
+-- Enhanced kind inference for data family instance in !13767
+-- this is the h98 data instance case
+
+data family V :: (k -> Type) -> k
+data instance V f = MkV (f (TYPE (BoxedRep 'Unlifted)))
=====================================
testsuite/tests/rep-poly/T25611c.hs
=====================================
@@ -0,0 +1,29 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE GADTs #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Exts (TYPE,RuntimeRep(IntRep,WordRep,TupleRep))
+
+data family DF :: TYPE (r :: RuntimeRep)
+
+-- it used to be failed: see #18891 and !4419
+-- See Note [Kind inference for data family instances]
+-- in GHC.Tc.TyCl.Instance
+-- but succ now see #25611
+newtype instance DF = MkDF1a Int#
+newtype instance DF = MkDF2a Word#
+newtype instance DF = MkDF3a (# Int#, Word# #)
+
+go = 1
+ where
+ x :: DF @IntRep
+ x = MkDF1a 3#
=====================================
testsuite/tests/rep-poly/T25611d.hs
=====================================
@@ -0,0 +1,37 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MagicHash #-}
+
+module T25611d where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Types
+
+-- | A data family with a kind signature
+data family T :: forall k. (k->v) -> k -> v
+-- ensure the kind specialization is correctly handled in the GADT-style data instance
+-- see Note [Kind inference for data family instances]
+-- p will specialize differently in the two constructors
+data instance T p q where
+ MkkT :: forall r. r Int -> T r Int
+ MkkV :: forall l. l Int# -> T l Int#
+
+type N :: TYPE r -> TYPE r
+newtype N a = MkN a
+
+f :: Int# -> N Int#
+f x = MkN x
+
+g :: Int -> N Int
+g x = MkN x
+
+data family D :: Type -> k -> k
+newtype instance D Int a = MkD a
+
+f1 :: Int# -> D Int Int#
+f1 x = MkD x
+
+g1 :: Int -> D Int Int
+g1 x = MkD x
=====================================
testsuite/tests/rep-poly/all.T
=====================================
@@ -111,6 +111,11 @@ test('RepPolyWrappedVar', normal, compile_fail, [''])
test('RepPolyWrappedVar2', [js_skip], compile, [''])
test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
+test('DataInstanceKindsDefaults', normal, compile, [''])
+test('T25611a', normal, compile, [''])
+test('T25611b', normal, compile, [''])
+test('T25611c', normal, compile, [''])
+test('T25611d', normal, compile, [''])
###############################################################################
## The following tests require rewriting in RuntimeReps, ##
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -931,4 +931,4 @@ test('T23501b', normal, compile, [''])
test('T25266', normal, compile, [''])
test('T25266a', normal, compile_fail, [''])
test('T25266b', normal, compile, [''])
-test('T25597', normal, compile, [''])
+test('T25597', normal, compile, [''])
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
=====================================
@@ -5,3 +5,11 @@ UnliftedNewtypesFamilyKindFail2.hs:12:20: error: [GHC-83865]
• In the first argument of ‘F’, namely ‘5’
In the newtype instance declaration for ‘F’
+UnliftedNewtypesFamilyKindFail2.hs:12:31: [GHC-83865]
+ Expected a type,
+ but ‘5’ has kind
+ ‘GHC.Internal.Bignum.Natural.Natural’
+ In the first argument of ‘F’, namely ‘5’
+ In the type ‘(F 5)’
+ In the definition of data constructor ‘MkF’
+
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
=====================================
@@ -3,3 +3,9 @@ UnliftedNewtypesInstanceFail.hs:13:3: error: [GHC-83865]
• Expected a WordRep type, but ‘Bar Bool’ is an IntRep type
• In the newtype instance declaration for ‘Bar’
In the instance declaration for ‘Foo Bool’
+
+UnliftedNewtypesInstanceFail.hs:14:17: [GHC-83865]
+ Expected an IntRep type, but ‘Word#’ is a WordRep type
+ In the type ‘Word#’
+ In the definition of data constructor ‘BarBoolC’
+ In the newtype instance declaration for ‘Bar’
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr deleted
=====================================
@@ -1,32 +0,0 @@
-
-UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error: [GHC-25897]
- • Couldn't match kind ‘t’ with ‘IntRep’
- Expected a type, but ‘Int#’ has kind ‘TYPE IntRep’
- ‘t’ is a rigid type variable bound by
- a family instance declaration
- at UnliftedNewtypesUnassociatedFamilyFail.hs:21:1-33
- • In the type ‘Int#’
- In the definition of data constructor ‘MkDF1a’
- In the newtype instance declaration for ‘DF’
-
-UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error: [GHC-25897]
- • Couldn't match kind ‘t’ with ‘WordRep’
- Expected a type, but ‘Word#’ has kind ‘TYPE WordRep’
- ‘t’ is a rigid type variable bound by
- a family instance declaration
- at UnliftedNewtypesUnassociatedFamilyFail.hs:22:1-34
- • In the type ‘Word#’
- In the definition of data constructor ‘MkDF2a’
- In the newtype instance declaration for ‘DF’
-
-UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error: [GHC-25897]
- • Couldn't match kind ‘t’ with ‘TupleRep [IntRep, WordRep]’
- Expected a type,
- but ‘(# Int#, Word# #)’ has kind ‘TYPE
- (TupleRep [IntRep, WordRep])’
- ‘t’ is a rigid type variable bound by
- a family instance declaration
- at UnliftedNewtypesUnassociatedFamilyFail.hs:23:1-46
- • In the type ‘(# Int#, Word# #)’
- In the definition of data constructor ‘MkDF3a’
- In the newtype instance declaration for ‘DF’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -552,7 +552,6 @@ test('UnliftedNewtypesConstraintFamily', normal, compile_fail, [''])
test('UnliftedNewtypesMismatchedKind', normal, compile_fail, [''])
test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
-test('UnliftedNewtypesUnassociatedFamilyFail', normal, compile_fail, [''])
test('T13834', normal, compile_fail, [''])
test('T17077', normal, compile_fail, [''])
test('T16512a', normal, compile_fail, [''])
=====================================
utils/dump-decls/Main.hs
=====================================
@@ -38,6 +38,7 @@ run root pkg_nm = runGhc (Just root) $ do
, "-dppr-cols=1000"
, "-fprint-explicit-runtime-reps"
, "-fprint-explicit-foralls"
+ , "-fsuppress-unit-ids"
]
dflags <- do
dflags <- getSessionDynFlags
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3b1d373cc523c0bb783694f5608a5ac7dbe5b129...56d509abfcd167daed1dbaf4c66766e09b417a8c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3b1d373cc523c0bb783694f5608a5ac7dbe5b129...56d509abfcd167daed1dbaf4c66766e09b417a8c
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/20250111/5c27dc74/attachment-0001.html>
More information about the ghc-commits
mailing list