[Git][ghc/ghc][wip/T25647] 2 commits: Revert "align wildcard with named typevar on wether it is skolem"
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Sat Feb 8 08:10:39 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
69bdf58d by Patrick at 2025-02-08T14:12:42+08:00
Revert "align wildcard with named typevar on wether it is skolem"
This reverts commit d1f61858328cc190de9b34c9a24e8d6b28ee5fa9.
- - - - -
f2dafbf2 by Patrick at 2025-02-08T16:10:27+08:00
add WildCardTv to forbid wildcard from defaulting
- - - - -
13 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/indexed-types/should_compile/T11450a.hs
- testsuite/tests/indexed-types/should_compile/T17536.hs
- testsuite/tests/indexed-types/should_compile/T17536c.hs
- testsuite/tests/indexed-types/should_compile/all.T
- testsuite/tests/typecheck/should_compile/T25647a.hs
- testsuite/tests/typecheck/should_compile/T25725.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -777,18 +777,17 @@ There is also the possibility of mentioning a wildcard
-}
-tcFamTyPats :: (Maybe SkolemInfo)
- -> TyCon
+tcFamTyPats :: 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 skol_info fam_tc hs_pats
+tcFamTyPats fam_tc hs_pats
= do { traceTc "tcFamTyPats {" $
vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
- ; mode <- mkHoleMode TypeLevel (HM_FamPat skol_info)
+ ; mode <- mkHoleMode TypeLevel HM_FamPat
-- HM_FamPat: See Note [Wildcards in family instances] in
-- GHC.Rename.Module
; let fun_ty = mkTyConApp fam_tc []
@@ -968,7 +967,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 (Maybe SkolemInfo) -- Family instances: F _ Int = Bool
+ | HM_FamPat -- Family instances: F _ Int = Bool
| HM_VTA -- Visible type and kind application:
-- f @(Maybe _)
-- Maybe @(_ -> _)
@@ -991,10 +990,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 })
@@ -2213,7 +2212,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 <- mk_wc_details
+ ; wc_details <- newWildCardTvDetailsAtLevel hole_lvl
; wc_name <- newMetaTyVarName wc_nm
; let kv = mkTcTyVar kv_name liftedTypeKind kv_details
wc_kind = mkTyVarTy kv
@@ -2231,21 +2230,17 @@ 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 Nothing tc_fam_tc hs_pats
+ do { (_fam_app, res_kind) <- tcFamTyPats 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 <+> ppr outer_bndrs
+ vcat [ ppr loc, ppr fam_tc <+> ppr hs_pats
, 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 (Just skol_info) fam_tc hs_pats
+ do { (lhs_ty, rhs_kind) <- tcFamTyPats 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 (Just skol_info) fam_tc hs_pats
+ ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
; (lhs_applied_ty, lhs_applied_kind)
<- tcInstInvisibleTyBinders lhs_ty lhs_kind
-- See Note [Data family/instance return kinds]
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -34,7 +34,8 @@ module GHC.Tc.Utils.TcMType (
newMultiplicityVar,
readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
- newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
+ newWildCardTvDetailsAtLevel, newTauTvDetailsAtLevel,
+ newMetaDetails, newMetaTyVarName,
isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
--------------------------------
@@ -692,6 +693,16 @@ the thinking.
* *
********************************************************************* -}
+{- Note [WildCardTv]
+~~~~~~~~~~~~~~~~~
+A WildCardTv behaves like a TauTv, except that it can not be defaulted.
+
+It is used for a anonymous wildcard in a type signature, e.g.
+ f :: _ -> Int
+ f = ...
+
+-}
+
{- Note [TyVarTv]
~~~~~~~~~~~~~~~~~
A TyVarTv can unify with type *variables* only, including other TyVarTvs and
@@ -740,6 +751,7 @@ metaInfoToTyVarName :: MetaInfo -> FastString
metaInfoToTyVarName meta_info =
case meta_info of
TauTv -> fsLit "t"
+ WildCardTv -> fsLit "_"
TyVarTv -> fsLit "a"
RuntimeUnkTv -> fsLit "r"
CycleBreakerTv -> fsLit "b"
@@ -853,6 +865,13 @@ newTauTvDetailsAtLevel tclvl
, mtv_ref = ref
, mtv_tclvl = tclvl }) }
+newWildCardTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails
+newWildCardTvDetailsAtLevel tclvl
+ = do { ref <- newMutVar Flexi
+ ; return (MetaTv { mtv_info = WildCardTv
+ , mtv_ref = ref
+ , mtv_tclvl = tclvl }) }
+
newConcreteTvDetailsAtLevel :: ConcreteTvOrigin -> TcLevel -> TcM TcTyVarDetails
newConcreteTvDetailsAtLevel conc_orig tclvl
= do { ref <- newMutVar Flexi
@@ -1841,7 +1860,10 @@ defaultTyVar :: DefaultingStrategy
-> TcTyVar -- If it's a MetaTyVar then it is unbound
-> TcM Bool -- True <=> defaulted away altogether
defaultTyVar def_strat tv
- | not (isMetaTyVar tv)
+ | not (isMetaTyVar tv )
+ || isWildCardMetaTyVar tv
+ -- do not default WildcardTvs, wildcardTvs are are only meant to be unified
+ -- or be on its own but never defaulted.
|| isTyVarTyVar tv
-- Do not default TyVarTvs. Doing so would violate the invariants
-- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType.
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -51,7 +51,8 @@ module GHC.Tc.Utils.TcType (
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTvUnk,
MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo,
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
- tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar,
+ isWildCardMetaTyVar, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar,
+ isTyConableTyVar,
ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar,
isConcreteTyVarTy, isConcreteTyVarTy_maybe, concreteInfo_maybe,
ConcreteTyVars, noConcreteTyVars,
@@ -640,7 +641,8 @@ data MetaInfo
= TauTv -- ^ This MetaTv is an ordinary unification variable
-- A TauTv is always filled in with a tau-type, which
-- never contains any ForAlls.
-
+ | WildCardTv -- ^ A variant of TauTv, except that is should not be
+ -- defaulted.
| TyVarTv -- ^ A variant of TauTv, except that it should not be
-- unified with a type, only with a type variable
-- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
@@ -670,6 +672,8 @@ instance Outputable MetaInfo where
ppr RuntimeUnkTv = text "rutv"
ppr CycleBreakerTv = text "cbv"
ppr (ConcreteTv {}) = text "conc"
+ ppr (WildCardTv) = text "wc"
+
-- | What caused us to create a 'ConcreteTv' metavariable?
-- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete.
@@ -1179,7 +1183,7 @@ isImmutableTyVar :: TyVar -> Bool
isImmutableTyVar tv = isSkolemTyVar tv
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
- isMetaTyVar, isAmbiguousTyVar, isCycleBreakerTyVar :: TcTyVar -> Bool
+ isMetaTyVar, isAmbiguousTyVar, isCycleBreakerTyVar, isWildCardMetaTyVar :: TcTyVar -> Bool
isTyConableTyVar tv
-- True of a meta-type variable that can be filled in
@@ -1220,6 +1224,13 @@ isMetaTyVar tv
_ -> False
| otherwise = False
+isWildCardMetaTyVar tv
+ | isTyVar tv -- See Note [Coercion variables in free variable lists]
+ = case tcTyVarDetails tv of
+ MetaTv { mtv_info = WildCardTv } -> True
+ _ -> False
+ | otherwise = False
+
-- isAmbiguousTyVar is used only when reporting type errors
-- It picks out variables that are unbound, namely meta
-- type variables and the RuntimeUnk variables created by
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2574,8 +2574,9 @@ lhsPriority tv
CycleBreakerTv -> 0
TyVarTv -> 1
ConcreteTv {} -> 2
- TauTv -> 3
- RuntimeUnkTv -> 4
+ WildCardTv -> 3
+ TauTv -> 4
+ RuntimeUnkTv -> 5
{- Note [Unification preconditions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/indexed-types/should_compile/T11450a.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T11450a where
+
+class C x where
+ type T x
+
+instance C (Either a b) where
+ type T (Either _ b) = b -> b
=====================================
testsuite/tests/indexed-types/should_compile/T17536.hs
=====================================
@@ -28,27 +28,3 @@ 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
=====================================
@@ -15,11 +15,3 @@ type family R r a where
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/indexed-types/should_compile/all.T
=====================================
@@ -315,3 +315,4 @@ test('T25611a', normal, compile, [''])
test('T25611b', normal, compile, [''])
test('T25611c', normal, compile, [''])
test('T25611d', normal, compile, [''])
+test('T11450a', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_compile/T25647a.hs
=====================================
@@ -72,11 +72,3 @@ 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
=====================================
testsuite/tests/typecheck/should_compile/T25725.hs
=====================================
@@ -9,7 +9,7 @@ import GHC.Exts
data D :: TYPE r -> Type where
MkD :: p -> D p
--- But this was rejected
+-- now this is OK too
data family Dix4 :: Type -> k
data instance Dix4 Int :: TYPE r -> Type where
DIn4 :: p -> Dix4 Int p
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -936,3 +936,4 @@ test('T25597', normal, compile, [''])
test('T25647a', normal, compile, [''])
test('T25647b', normal, compile, [''])
test('T25647_fail', normal, compile_fail, [''])
+test('T25725', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ccc9152f23177ab7a542852ffedf626edcdcef95...f2dafbf21d3e46bd82ee8f43502a04c164ef37b2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ccc9152f23177ab7a542852ffedf626edcdcef95...f2dafbf21d3e46bd82ee8f43502a04c164ef37b2
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/20250208/a0ea33e8/attachment-0001.html>
More information about the ghc-commits
mailing list