[Git][ghc/ghc][wip/T25647] align wildcard with named typevar on wether it is skolem
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Fri Feb 7 14:13:54 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
a25221e6 by Patrick at 2025-02-07T22:13:34+08:00
align wildcard with named typevar on wether it is skolem
- - - - -
6 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- testsuite/tests/indexed-types/should_compile/T17536.hs
- testsuite/tests/indexed-types/should_compile/T17536c.hs
- testsuite/tests/typecheck/should_compile/T25647a.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -777,17 +777,18 @@ There is also the possibility of mentioning a wildcard
-}
-tcFamTyPats :: TyCon
+tcFamTyPats :: (Maybe SkolemInfo)
+ -> TyCon
-> HsFamEqnPats GhcRn -- Patterns
-> TcM (TcType, TcKind) -- (lhs_type, lhs_kind)
-- Check the LHS of a type/data family instance
-- e.g. type instance F ty1 .. tyn = ...
-- Used for both type and data families
-tcFamTyPats fam_tc hs_pats
+tcFamTyPats skol_info fam_tc hs_pats
= do { traceTc "tcFamTyPats {" $
vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
- ; mode <- mkHoleMode TypeLevel HM_FamPat
+ ; mode <- mkHoleMode TypeLevel (HM_FamPat skol_info)
-- HM_FamPat: See Note [Wildcards in family instances] in
-- GHC.Rename.Module
; let fun_ty = mkTyConApp fam_tc []
@@ -967,7 +968,7 @@ type HoleInfo = Maybe (TcLevel, HoleMode)
-- HoleMode says how to treat the occurrences
-- of anonymous wildcards; see tcAnonWildCardOcc
data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
- | HM_FamPat -- Family instances: F _ Int = Bool
+ | HM_FamPat (Maybe SkolemInfo) -- Family instances: F _ Int = Bool
| HM_VTA -- Visible type and kind application:
-- f @(Maybe _)
-- Maybe @(_ -> _)
@@ -990,10 +991,10 @@ mkHoleMode tyki hm
, mode_holes = Just (lvl,hm) }) }
instance Outputable HoleMode where
- ppr HM_Sig = text "HM_Sig"
- ppr HM_FamPat = text "HM_FamPat"
- ppr HM_VTA = text "HM_VTA"
- ppr HM_TyAppPat = text "HM_TyAppPat"
+ ppr HM_Sig = text "HM_Sig"
+ ppr (HM_FamPat _) = text "HM_FamPat"
+ ppr HM_VTA = text "HM_VTA"
+ ppr HM_TyAppPat = text "HM_TyAppPat"
instance Outputable TcTyMode where
ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
@@ -2212,7 +2213,7 @@ tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }
-- esp the bullet on nested forall types
= do { kv_details <- newTauTvDetailsAtLevel hole_lvl
; kv_name <- newMetaTyVarName (fsLit "k")
- ; wc_details <- newTauTvDetailsAtLevel hole_lvl
+ ; wc_details <- mk_wc_details
; wc_name <- newMetaTyVarName wc_nm
; let kv = mkTcTyVar kv_name liftedTypeKind kv_details
wc_kind = mkTyVarTy kv
@@ -2230,17 +2231,21 @@ tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }
-- so we have to do it properly (T14140a)
; checkExpectedKind ty (mkTyVarTy wc_tv) wc_kind exp_kind }
where
+ -- make sure we align with none-wild card type variables
+ mk_wc_details = case hole_mode of
+ HM_FamPat (Just skol_info) -> return $ SkolemTv skol_info hole_lvl False
+ _ -> newTauTvDetailsAtLevel hole_lvl
-- See Note [Wildcard names]
wc_nm = case hole_mode of
HM_Sig -> fsLit "w"
- HM_FamPat -> fsLit "_"
+ HM_FamPat _ -> fsLit "_"
HM_VTA -> fsLit "w"
HM_TyAppPat -> fsLit "_"
emit_holes = case hole_mode of
- HM_Sig -> True
- HM_FamPat -> False
- HM_VTA -> False
+ HM_Sig -> True
+ HM_FamPat _ -> False
+ HM_VTA -> False
HM_TyAppPat -> False
tcAnonWildCardOcc is_extra _ _ _
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3253,7 +3253,7 @@ kcTyFamInstEqn tc_fam_tc
; discardResult $
bindOuterFamEqnTKBndrs_Q_Tv outer_bndrs $
- do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
+ do { (_fam_app, res_kind) <- tcFamTyPats Nothing tc_fam_tc hs_pats
; tcCheckLHsTypeInContext hs_rhs_ty (TheKind res_kind) }
-- Why "_Tv" here? Consider (#14066)
-- type family Bar x y where
@@ -3275,7 +3275,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
, feqn_rhs = hs_rhs_ty }))
= setSrcSpanA loc $
do { traceTc "tcTyFamInstEqn" $
- vcat [ ppr loc, ppr fam_tc <+> ppr hs_pats
+ vcat [ ppr loc, ppr fam_tc <+> ppr hs_pats <+> ppr outer_bndrs
, text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc)
, case mb_clsinfo of
NotAssociated {} -> empty
@@ -3430,7 +3430,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
; (tclvl, wanted, (outer_bndrs, (lhs_ty, rhs_ty)))
<- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
bindOuterFamEqnTKBndrs skol_info outer_hs_bndrs $
- do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
+ do { (lhs_ty, rhs_kind) <- tcFamTyPats (Just skol_info) fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
; addConsistencyConstraints mb_clsinfo lhs_ty
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -933,7 +933,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
<- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
bindOuterFamEqnTKBndrs skol_info hs_outer_bndrs $ -- Binds skolem TcTyVars
do { stupid_theta <- tcHsContext hs_ctxt
- ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
+ ; (lhs_ty, lhs_kind) <- tcFamTyPats (Just skol_info) fam_tc hs_pats
; (lhs_applied_ty, lhs_applied_kind)
<- tcInstInvisibleTyBinders lhs_ty lhs_kind
-- See Note [Data family/instance return kinds]
=====================================
testsuite/tests/indexed-types/should_compile/T17536.hs
=====================================
@@ -28,3 +28,27 @@ type family M m where
g :: M One -> Int
g x = x
+
+
+-- make sure wildcard and non-wildcard type variables are treated the same
+
+type R1 :: RuntimeRep -> Type
+type family R1 r where
+ R1 r = Int
+
+r1 :: R1 FloatRep -> Int
+r1 x = x
+
+type L1 :: Levity -> Type
+type family L1 l where
+ L1 l = Int
+
+l1 :: L1 Unlifted -> Int
+l1 x = x
+
+type M1 :: Multiplicity -> Type
+type family M1 m where
+ M1 m = Int
+
+g1 :: M1 One -> Int
+g1 x = x
=====================================
testsuite/tests/indexed-types/should_compile/T17536c.hs
=====================================
@@ -11,7 +11,15 @@ import GHC.Exts
type R :: forall (r :: RuntimeRep) -> TYPE r -> Type
type family R r a where
- R _ _ = Int
+ R r a = Int
r :: R FloatRep Float# -> Int
r x = x
+
+-- make sure wildcard and non-wildcard type variables are treated the same
+type R1 :: forall (r :: RuntimeRep) -> TYPE r -> Type
+type family R1 r a where
+ R1 r a = Int
+
+r1 :: R1 FloatRep Float# -> Int
+r1 x = x
=====================================
testsuite/tests/typecheck/should_compile/T25647a.hs
=====================================
@@ -72,3 +72,11 @@ newtype instance Dix5 f = DIn5 (f (Dix5 f))
data family Dix7 :: (k -> TYPE 'IntRep) -> k
newtype instance Dix7 f = DIn7 (f (Dix7 f))
+
+-- user written wildcards
+type Dix8 :: RuntimeRep -> Type
+data family Dix8 r
+newtype instance Dix8 _ = Dix8 Int
+
+dix8 :: Dix8 FloatRep -> Int
+dix8 (Dix8 x) = x
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a25221e671c9e0d550d844ca843a23a7f08fb5dc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a25221e671c9e0d550d844ca843a23a7f08fb5dc
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/20250207/1887ea64/attachment-0001.html>
More information about the ghc-commits
mailing list