[Git][ghc/ghc][wip/T25647] 2 commits: Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Feb 4 17:40:06 UTC 2025
Simon Peyton Jones pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
cd48e19b by Simon Peyton Jones at 2025-02-04T16:27:20+00:00
Wibbles
- - - - -
22849523 by Simon Peyton Jones at 2025-02-04T17:39:30+00:00
Default tyvars in data/newtype insnstances
This is what fixes #25647
- - - - -
4 changed files:
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- testsuite/tests/typecheck/should_compile/T25647.hs
Changes:
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -860,8 +860,7 @@ rnDataFamInstDecl :: AssocTyFamInfo
-> RnM (DataFamInstDecl GhcRn, FreeVars)
rnDataFamInstDecl atfi (DataFamInstDecl { dfid_eqn =
eqn@(FamEqn { feqn_tycon = tycon })})
- = do { (eqn', fvs) <-
- rnFamEqn (TyDataCtx tycon) atfi eqn rnDataDefn
+ = do { (eqn', fvs) <- rnFamEqn (TyDataCtx tycon) atfi eqn rnDataDefn
; return (DataFamInstDecl { dfid_eqn = eqn' }, fvs) }
-- Renaming of the associated types in instances.
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -1863,8 +1863,8 @@ kcConDecl new_or_data tc_res_kind
-- because that's done in tcConDecl
}
-kcConDecl new_or_data tc_res_kind
- -- ToDo: fix this comment NB: _tc_res_kind is unused. See (KCD3) in
+kcConDecl new_or_data _tc_res_kind
+ -- NB: _tc_res_kind is unused. See (KCD3) in
-- Note [kcConDecls: kind-checking data type decls]
(ConDeclGADT { con_names = names, con_bndrs = L _ outer_bndrs
, con_mb_cxt = cxt, con_g_args = args, con_res_ty = res_ty })
@@ -1876,9 +1876,10 @@ kcConDecl new_or_data tc_res_kind
-- Why "_Tv"? See Note [Using TyVarTvs for kind-checking GADTs]
do { _ <- tcHsContext cxt
; traceTc "kcConDecl:GADT {" (ppr names $$ ppr res_ty)
- ; _ <- tcCheckLHsTypeInContext res_ty (TheKind tc_res_kind)
+ ; con_res_kind <- newOpenTypeKind
+ ; _ <- tcCheckLHsTypeInContext res_ty (TheKind con_res_kind)
- ; let arg_exp_kind = getArgExpKind new_or_data tc_res_kind
+ ; let arg_exp_kind = getArgExpKind new_or_data con_res_kind
-- getArgExpKind: for newtypes, check that the argument kind
-- is the same the kind of `res_ty`, the data con's return type
-- See (KCD2) in Note [kcConDecls: kind-checking data type decls]
@@ -3752,30 +3753,30 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
; return (NE.singleton dc) }
-tcConDecl new_or_data dd_info rep_tycon tc_bndrs tc_res_kind tag_map
- -- TODO: fix this comment NB: don't use res_kind here, as it's ill-scoped. Instead,
+tcConDecl new_or_data dd_info rep_tycon tc_bndrs _tc_res_kind tag_map
+ -- NB: don't use _tc_res_kind here, as it's ill-scoped. Instead,
-- we get the res_kind by typechecking the result type.
(ConDeclGADT { con_names = names
, con_bndrs = L _ outer_hs_bndrs
, con_mb_cxt = cxt, con_g_args = hs_args
, con_res_ty = hs_res_ty })
= addErrCtxt (DataConDefCtxt names) $
- do { traceTc "tcConDecl 1 gadt" (ppr names $$ ppr tc_res_kind)
+ do { traceTc "tcConDecl 1 gadt" (ppr names $$ ppr _tc_res_kind)
; let L _ name :| _ = names
; skol_info <- mkSkolemInfo (DataConSkol name)
- ; (tclvl, wanted, (outer_bndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
+ ; (tclvl, wanted, (outer_bndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts, res_kind)))
<- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $
tcOuterTKBndrs skol_info outer_hs_bndrs $
- do { ctxt <- tcHsContext cxt
+ do { ctxt <- tcHsContext cxt
+
+ ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
+ -- See Note [GADT return kinds]
-- See Note [Datatype return kinds]
- ; let exp_kind = getArgExpKind new_or_data tc_res_kind
+ ; let exp_kind = getArgExpKind new_or_data res_kind
; btys <- tcConGADTArgs exp_kind hs_args
-
- ; res_ty <- tcCheckLHsType hs_res_ty tc_res_kind
- -- See Note [GADT return kinds]
- ; traceTc "tcConDecl 1a gadt" (ppr res_ty)
+ ; traceTc "tcConDecl 1a gadt" (ppr res_ty <+> dcolon <+> ppr res_kind)
-- For data instances (only), ensure that the return type,
-- res_ty, is a substitution instance of the header.
@@ -3792,7 +3793,7 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs tc_res_kind tag_map
; let (arg_tys, stricts) = unzip btys
; field_lbls <- lookupConstructorFields name
- ; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
+ ; return (ctxt, arg_tys, res_ty, field_lbls, stricts, res_kind)
}
; outer_bndrs <- scopedSortOuter outer_bndrs
@@ -3806,7 +3807,7 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs tc_res_kind tag_map
; traceTc "tcConDecl:GADT" (vcat [ text "names:" <+> ppr names
, text "tkvs:" <+> ppr tkvs
, text "res_ty:" <+> ppr res_ty
- , text "tc_res_kind" <+> ppr tc_res_kind ])
+ , text "res_kind:" <+> ppr res_kind ])
; reportUnsolvedEqualities skol_info tkvs tclvl wanted
; let tvbndrs = mkTyVarBinders InferredSpec tkvs ++ outer_tv_bndrs
@@ -3828,14 +3829,6 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs tc_res_kind tag_map
arg_tys' = substScaledTys arg_subst arg_tys
res_ty' = substTy arg_subst res_ty
- eq_preds' = pprTrace "eq_preds"
- (vcat [ ppr names
- , text "res_tmpl:" <+> ppr res_tmpl
- , text "res_ty:" <+> ppr res_ty
- , text "tc_res_kind:" <+> ppr tc_res_kind
- , text "eq_preds:" <+> ppr eq_preds ]) $
- eq_preds
-
-- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
; fam_envs <- tcGetFamInstEnvs
@@ -3848,7 +3841,7 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs tc_res_kind tag_map
; let bang_opts = SrcBangOpts (initBangOpts dflags)
; buildDataCon fam_envs bang_opts name is_infix
rep_nm stricts field_lbls
- univ_tvs ex_tvs tvbndrs' eq_preds'
+ univ_tvs ex_tvs tvbndrs' eq_preds
ctxt' arg_tys' res_ty' rep_tycon tag_map
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -975,7 +975,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
-- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
; dvs <- candidateQTyVarsWithBinders outer_tvs lhs_ty
- ; qtvs <- quantifyTyVars skol_info TryNotToDefaultNonStandardTyVars dvs
+ ; qtvs <- quantifyTyVars skol_info DefaultNonStandardTyVars dvs
; let final_tvs = scopedSort (qtvs ++ outer_tvs)
-- This scopedSort is important: the qtvs may be /interleaved/ with
-- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
=====================================
testsuite/tests/typecheck/should_compile/T25647.hs
=====================================
@@ -18,25 +18,33 @@ newtype Fix1b f where
-- A plain newtype, GADT syntax, with a return kind signature
-- Should infer Fix2 :: forall r k. (k -> TYPE r) -> TYPE r
-newtype Fix2 f :: TYPE r where
- In2 :: forall ff. ff (Fix2 ff) -> Fix2 ff
+-- Rejected because of deafulting; maybe that's OK
+-- newtype Fix2 f :: TYPE r where
+-- In2 :: forall ff. ff (Fix2 ff) -> Fix2 ff
-- Plain newtype, H98 syntax, standalone kind signature
--- Should get In3 :: forall r k (f :: k -> TYPE r). Fix4 @r @k f -> Fix4 @r @k f
---type Fix3 :: forall r k. (k -> TYPE r) -> k
---newtype Fix3 f = In3 (f (Fix3 f))
+-- Should get In3 :: forall r (f :: TYPE r -> TYPE r). Fix3 @r f -> Fix3 @r f
+type Fix3 :: forall r. (TYPE r -> TYPE r) -> TYPE r
+newtype Fix3 f = In3 (f (Fix3 f))
+
+-- This variant produces a /terrible/ message
+-- type Fix3a :: forall r k. (TYPE r -> TYPE r) -> TYPE r
+-- newtype Fix3a f = In3a (f (Fix3 f))
-{-
-- Plain newtype, H98 syntax, standalone kind signature
-- Should get In4 :: forall r k (f :: k -> TYPE r). Fix4 @r @k f -> Fix4 @r @k f
-type Fix4 :: forall r k. (k -> TYPE r) -> k
+type Fix4 :: forall r. (TYPE r -> TYPE r) -> TYPE r
newtype Fix4 f where
- In4 :: forall rr kk (ff :: kk -> TYPE rr).
- ff (Fix4 ff) -> Fix4 @rr @kk ff
--}
+ In4 :: forall rr (ff :: TYPE rr -> TYPE rr).
+ ff (Fix4 ff) -> Fix4 @rr ff
+
+-- Rejected because of defulting; maybe that's OK
+--type Fix4a :: forall r. (TYPE r -> TYPE r) -> TYPE r
+--newtype Fix4a f where
+-- In4a :: ff (Fix4a ff) -> Fix4a ff
+
-------------------- Data families with newtype instance -----------------
-{-
-- data instance in GADT sytntax
data family Dix1 :: (k -> Type) -> k
data instance Dix1 f where
@@ -47,17 +55,25 @@ data family Dix2 :: (k -> Type) -> k
newtype instance Dix2 f where
DIn2 :: forall ff. ff (Dix2 ff) -> Dix2 ff
+data family Dix2a :: (k -> Type) -> k
+newtype instance Dix2a f :: Type where
+ DIn2a :: forall ff. ff (Dix2a ff) -> Dix2a ff
+
-- newtype instance in H98 syntax
data family Dix3 :: (k -> Type) -> k
newtype instance Dix3 f = DIn3 (f (Dix3 f))
-- newtype instance in GADT syntax
+-- Rejected because of defaulting
data family Dix4 :: (k -> TYPE r) -> k
newtype instance Dix4 f where
DIn4 :: forall ff. ff (Dix4 ff) -> Dix4 ff
+--data family Dix4a :: (k -> TYPE r) -> k
+--newtype instance forall r f. Dix4a f :: TYPE r where
+-- DIn4a :: forall r (ff :: TYPE r -> TYPE r). ff (Dix4a ff) -> Dix4a ff
+
-- newtype instance in H98 syntax
data family Dix5 :: (k -> TYPE r) -> k
newtype instance Dix5 f = DIn5 (f (Dix5 f))
--}
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e605c5eed28d41163d210935dc36d9b75ff2f790...2284952331e54f87314c63cf449a80dc9f68db6c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e605c5eed28d41163d210935dc36d9b75ff2f790...2284952331e54f87314c63cf449a80dc9f68db6c
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/20250204/b4b53c93/attachment-0001.html>
More information about the ghc-commits
mailing list