From 3d9cacd5b09019c4ce2ccea9a509220bb44e36a2 Mon Sep 17 00:00:00 2001
From: Patrick <fwy996602672@gmail.com>
Date: Tue, 14 Jan 2025 02:30:44 +0800
Subject: [PATCH] Enhance kind inference for data family instances This commit
improves kind inference for data family instances by kind-checking the
constructors, for H98 and newtype declarations (ONLY), as well as
kind-checking the result kind signature (when using GADT syntax). This fixes
#25611.
Typechecker changes:
In `tcDataFamInstHeader`, we now kind-check the constructors using
`kcConDecls`, for H98-style decls and newtype decls ONLY.
See Note [Kind inference for data family instances].
Testsuite changes:
- The T25611{a,b,c,d} tests test the new kind inference implementation.
- a,b: infer result kind from constructors (H98 case)
- c: renamed version of test UnliftedNewtypesUnassociatedFamilyFail,
which now passes
- d: GADT case, checking that we don't infer overly rigid kinds when
kind-checking the constructors in data family instances.
- DataInstanceKindsDefaults tests defaulting data instance kinds
without UnliftedNewtypes or UnliftedDatatypes, as outlined in
Note [Defaulting result kind of newtype/data family instance].
Also a few notes are updated to reflect the changes.
Co-authored-by: default avatarSimon Peyton Jones <simon.peytonjones@gmail.com>
---
compiler/GHC/Tc/Gen/HsType.hs | 17 +++-
compiler/GHC/Tc/TyCl.hs | 28 +++---
compiler/GHC/Tc/TyCl/Instance.hs | 99 +++++++++++++------
.../DataInstanceKindsDefaults.hs | 26 +++++
.../indexed-types/should_compile/T25611a.hs | 17 ++++
.../indexed-types/should_compile/T25611b.hs | 16 +++
.../should_compile/T25611c.hs} | 10 +-
.../indexed-types/should_compile/T25611d.hs | 38 +++++++
.../tests/indexed-types/should_compile/all.T | 5 +
.../UnliftedNewtypesFamilyKindFail2.stderr | 8 ++
.../UnliftedNewtypesInstanceFail.stderr | 5 +
...iftedNewtypesUnassociatedFamilyFail.stderr | 32 ------
testsuite/tests/typecheck/should_fail/all.T | 1 -
13 files changed, 221 insertions(+), 81 deletions(-)
create mode 100644 testsuite/tests/indexed-types/should_compile/DataInstanceKindsDefaults.hs
create mode 100644 testsuite/tests/indexed-types/should_compile/T25611a.hs
create mode 100644 testsuite/tests/indexed-types/should_compile/T25611b.hs
rename testsuite/tests/{typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs => indexed-types/should_compile/T25611c.hs} (79%)
create mode 100644 testsuite/tests/indexed-types/should_compile/T25611d.hs
delete mode 100644 testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index b214613f74a..276208cd0b4 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/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,
@@ -2468,7 +2469,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
@@ -3921,14 +3922,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
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 4f4797c373d..fc258c5fef4 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1140,7 +1140,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
@@ -1257,7 +1257,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.
@@ -2128,7 +2128,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.
@@ -2223,14 +2223,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
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 1e8a6ce80f9..280661f2907 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -8,6 +8,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -715,7 +716,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
; skol_info <- mkSkolemInfo FamInstSkol
; (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]
@@ -740,8 +741,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)
@@ -919,8 +919,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
@@ -928,7 +927,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" $
@@ -944,16 +943,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" $
@@ -1005,9 +1005,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
@@ -1033,6 +1040,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
@@ -1187,31 +1209,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.
diff --git a/testsuite/tests/indexed-types/should_compile/DataInstanceKindsDefaults.hs b/testsuite/tests/indexed-types/should_compile/DataInstanceKindsDefaults.hs
new file mode 100644
index 00000000000..ca39f820ffa
--- /dev/null
+++ b/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
+
diff --git a/testsuite/tests/indexed-types/should_compile/T25611a.hs b/testsuite/tests/indexed-types/should_compile/T25611a.hs
new file mode 100644
index 00000000000..b8992be35d9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/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
diff --git a/testsuite/tests/indexed-types/should_compile/T25611b.hs b/testsuite/tests/indexed-types/should_compile/T25611b.hs
new file mode 100644
index 00000000000..8ef320851c7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/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)))
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs b/testsuite/tests/indexed-types/should_compile/T25611c.hs
similarity index 79%
rename from testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
rename to testsuite/tests/indexed-types/should_compile/T25611c.hs
index 21b1b053fcf..3dd50981d00 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
+++ b/testsuite/tests/indexed-types/should_compile/T25611c.hs
@@ -6,7 +6,7 @@
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE GADTs #-}
-module UnliftedNewtypesUnassociatedFamily where
+module T25611c where
import GHC.Int (Int(I#))
import GHC.Word (Word(W#))
@@ -15,9 +15,15 @@ import GHC.Exts (TYPE,RuntimeRep(IntRep,WordRep,TupleRep))
data family DF :: TYPE (r :: RuntimeRep)
--- All these fail: see #18891 and !4419
+-- 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#
diff --git a/testsuite/tests/indexed-types/should_compile/T25611d.hs b/testsuite/tests/indexed-types/should_compile/T25611d.hs
new file mode 100644
index 00000000000..e72674f427f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T25611d.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index dcf20a247bf..af391bd0b05 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -310,3 +310,8 @@ test('T22717', normal, makefile_test, ['T22717'])
test('T22717_fam_orph', normal, multimod_compile, ['T22717_fam_orph', '-v0'])
test('T23408', normal, compile, [''])
test('T24134', normal, compile, [''])
+test('DataInstanceKindsDefaults', normal, compile, [''])
+test('T25611a', normal, compile, [''])
+test('T25611b', normal, compile, [''])
+test('T25611c', normal, compile, [''])
+test('T25611d', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
index b3e78e5d97d..a79eec0e62d 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
+++ b/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 family 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’
+
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
index 4d8374ac6c5..ebc882463a2 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
@@ -3,3 +3,8 @@ UnliftedNewtypesInstanceFail.hs:13:3: error: [GHC-83865]
• In the associated newtype family 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 associated newtype family instance declaration for ‘Bar’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
deleted file mode 100644
index c03d6908f49..00000000000
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
+++ /dev/null
@@ -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 family 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 family 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 family instance declaration for ‘DF’
-
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 0949e1c33dd..993fbbee387 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/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, [''])
--
GitLab