[Git][ghc/ghc][wip/T25647] handle explicit implicit binders seperately
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Mon Mar 10 23:40:35 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
881da0f0 by Patrick at 2025-03-11T07:40:26+08:00
handle explicit implicit binders seperately
- - - - -
3 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -72,7 +72,7 @@ module GHC.Tc.Gen.HsType (
HoleMode(..),
-- Utils
- tyLitFromLit, tyLitFromOverloadedLit,
+ tyLitFromLit, tyLitFromOverloadedLit, expliciteOuterTyVars, impliciteOuterTyVars,
) where
@@ -3281,6 +3281,19 @@ outerTyVars :: HsOuterTyVarBndrs flag GhcTc -> [TcTyVar]
outerTyVars (HsOuterImplicit { hso_ximplicit = tvs }) = tvs
outerTyVars (HsOuterExplicit { hso_xexplicit = tvbs }) = binderVars tvbs
+expliciteOuterTyVars :: HsOuterTyVarBndrs flag GhcTc -> [TcTyVar]
+-- The returned [TcTyVar] is not necessarily in dependency order
+-- at least for the HsOuterImplicit case
+expliciteOuterTyVars (HsOuterImplicit {}) = []
+expliciteOuterTyVars (HsOuterExplicit { hso_xexplicit = tvbs }) = binderVars tvbs
+
+impliciteOuterTyVars :: HsOuterTyVarBndrs flag GhcTc -> [TcTyVar]
+-- The returned [TcTyVar] is not necessarily in dependency order
+impliciteOuterTyVars (HsOuterImplicit { hso_ximplicit = tvs }) = tvs
+impliciteOuterTyVars (HsOuterExplicit {}) = []
+
+
+
---------------
outerTyVarBndrs :: HsOuterTyVarBndrs Specificity GhcTc -> [InvisTVBinder]
outerTyVarBndrs (HsOuterImplicit{hso_ximplicit = imp_tvs}) = [Bndr tv SpecifiedSpec | tv <- imp_tvs]
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -21,7 +21,7 @@ module GHC.Tc.TyCl (
tcFamTyPats, tcTyFamInstEqn,
tcAddOpenTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
unravelFamInstPats, addConsistencyConstraints,
- checkFamTelescope
+ checkFamTelescope, tcFamInsLHSBinders
) where
import GHC.Prelude
@@ -39,7 +39,7 @@ import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Unify( unifyType, emitResidualTvConstraint )
-import GHC.Tc.Types.Constraint( emptyWC )
+import GHC.Tc.Types.Constraint( emptyWC, WantedConstraints )
import GHC.Tc.Validity
import GHC.Tc.Zonk.Type
import GHC.Tc.Zonk.TcType
@@ -248,6 +248,51 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
; return (gbl_env'', inst_info, deriv_info,
th_bndrs' `plusNameEnv` th_bndrs) }
+
+-- tcFamInsLHSBinders :: FamEqn TyVar Name -> TcM [TyVar]
+tcFamInsLHSBinders :: TcLevel -> SkolemInfo -> HsOuterFamEqnTyVarBndrs GhcTc -> HsOuterFamEqnTyVarBndrs GhcRn
+ -> [TcTyVar] -> Type -> WantedConstraints -> IOEnv (Env TcGblEnv TcLclEnv) ([TyCoVar], [TcTyVar])
+tcFamInsLHSBinders tclvl skol_info outer_bndrs hs_outer_bndrs wcs lhs_ty wanted = do
+ -- This code (and the stuff immediately above) is very similar
+ -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the
+ -- common code; but for the moment I concluded that it's
+ -- clearer to duplicate it. Still, if you fix a bug here,
+ -- check there too!
+
+ -- See Note [Type variables in type families instance decl]
+ ; let outer_exp_tvs = scopedSort $ expliciteOuterTyVars outer_bndrs
+ ; let outer_imp_tvs = impliciteOuterTyVars outer_bndrs
+ ; checkFamTelescope tclvl hs_outer_bndrs outer_exp_tvs
+ ; outer_imp_wc_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVarsMaybe $ outer_imp_tvs ++ wcs
+ -- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
+ ; (dvs, cqdvs) <- candidateQTyVarsWithBinders (outer_imp_wc_tvs ++ outer_exp_tvs) lhs_ty
+ ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
+ -- Have to make a same defaulting choice for reuslt kind here
+ -- and the `kindGeneralizeAll` in `tcConDecl`.
+ -- see (GT4) in
+ -- GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
+
+ ; let final_tvs = scopedSort (qtvs ++ outer_exp_tvs)
+
+ ; traceTc "tcFamInsLHSBinders" $
+ vcat [
+ -- ppr fam_tc
+ text "lhs_ty:" <+> ppr lhs_ty
+ , text "final_tvs:" <+> pprTyVars final_tvs
+ , text "outer_imp_tvs:" <+> pprTyVars outer_imp_tvs
+ , text "outer_exp_tvs:" <+> pprTyVars outer_exp_tvs
+ , text "wcs:" <+> pprTyVars wcs
+ , text "outer_imp_wc_tvs:" <+> pprTyVars outer_imp_wc_tvs
+ , text "outer_bndrs:" <+> ppr outer_bndrs
+ , text "qtvs:" <+> pprTyVars qtvs
+ , text "cqdvs:" <+> pprTyVars cqdvs
+ , text "dvs:" <+> ppr dvs
+ ]
+ -- This scopedSort is important: the qtvs may be /interleaved/ with
+ -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
+ ; reportUnsolvedEqualities skol_info final_tvs tclvl wanted
+ return (final_tvs, qtvs)
+
-- Gives the kind for every TyCon that has a standalone kind signature
type KindSigEnv = NameEnv Kind
@@ -3439,37 +3484,8 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
; traceTc "tcTyFamInstEqnGuts 0" (ppr outer_bndrs $$ ppr skol_info)
- -- See Note [Type variables in type families instance decl]
- ; let outer_tvs = (outerTyVars outer_bndrs)
- ; checkFamTelescope tclvl outer_hs_bndrs outer_tvs
- ; outer_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVarsMaybe $ outer_tvs ++ wcs
-
- ; traceTc "tcTyFamInstEqnGuts 1" (
- vcat [
- text "wildcards" <+> ppr wcs,
- text "outer_tvs" <+> pprTyVars outer_tvs,
- ppr skol_info
- ]
- )
-
- -- This code (and the stuff immediately above) is very similar
- -- to that in tcDataFamInstHeader. Maybe we should abstract the
- -- common code; but for the moment I concluded that it's
- -- clearer to duplicate it. Still, if you fix a bug here,
- -- check there too!
-
- -- See Note [Generalising in tcTyFamInstEqnGuts]
- ; (dvs, cqdvs) <- candidateQTyVarsWithBinders outer_tvs lhs_ty
- ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
- ; let final_tvs = scopedSort qtvs
- -- This scopedSort is important: the qtvs may be /interleaved/ with
- -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
- ; reportUnsolvedEqualities skol_info final_tvs tclvl wanted
-
- ; traceTc "tcTyFamInstEqnGuts 2" $
- vcat [ ppr fam_tc
- , text "lhs_ty:" <+> ppr lhs_ty
- , text "final_tvs:" <+> pprTyVars final_tvs ]
+ -- -- See Note [Type variables in type families instance decl]
+ ; (final_tvs, qtvs) <- tcFamInsLHSBinders tclvl skol_info outer_bndrs outer_hs_bndrs wcs lhs_ty wanted
-- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
-- Example: typecheck/should_fail/T17301
@@ -3509,7 +3525,7 @@ checkFamTelescope tclvl hs_outer_bndrs outer_tvs
, let b_last = last bndrs
= do { skol_info <- mkSkolemInfo (ForAllSkol $ HsTyVarBndrsRn (map unLoc bndrs))
; setSrcSpan (combineSrcSpans (getLocA b_first) (getLocA b_last)) $ do
- emitResidualTvConstraint skol_info (scopedSort outer_tvs) tclvl emptyWC }
+ emitResidualTvConstraint skol_info outer_tvs tclvl emptyWC }
| otherwise
= return ()
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -92,7 +92,6 @@ import Control.Monad
import Data.Tuple
import GHC.Data.Maybe
import Data.List( mapAccumL )
-import GHC.Core.TyCo.Ppr (pprTyVars)
{-
@@ -969,6 +968,7 @@ tcDataFamInstDecl is processing a non-associated data family instance, this
TyVarEnv will simply be empty, and there is nothing to worry about.
-}
+
-----------------------
tcDataFamInstHeader
:: AssocInstInfo -> SkolemInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
@@ -1017,37 +1017,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
, lhs_applied_kind
, res_kind ) }
- -- This code (and the stuff immediately above) is very similar
- -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the
- -- common code; but for the moment I concluded that it's
- -- clearer to duplicate it. Still, if you fix a bug here,
- -- check there too!
-
- -- See Note [Type variables in type families instance decl]
- ; let outer_tvs = (outerTyVars outer_bndrs)
- ; checkFamTelescope tclvl hs_outer_bndrs outer_tvs
- ; outer_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVarsMaybe $ outer_tvs ++ wcs
-
- -- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
- ; (dvs, cqdvs) <- candidateQTyVarsWithBinders outer_tvs lhs_ty
- ; qtvs <- quantifyTyVarsWithBinders cqdvs skol_info dvs
- -- Have to make a same defaulting choice for reuslt kind here
- -- and the `kindGeneralizeAll` in `tcConDecl`.
- -- see (GT4) in
- -- GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
-
- ; let final_tvs = scopedSort qtvs
- ; traceTc "tcDataFamInstHeader 1" $
- vcat [
- text "skol_info:" <+> ppr skol_info,
- text "outer_tvs:" <+> pprTyVars outer_tvs,
- text "dvs:" <+> ppr dvs,
- text "wcs:" <+> ppr wcs,
- text "final_tvs:" <+> ppr final_tvs
- ]
- -- This scopedSort is important: the qtvs may be /interleaved/ with
- -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts]
- ; reportUnsolvedEqualities skol_info final_tvs tclvl wanted
+ ; (final_tvs, qtvs) <- tcFamInsLHSBinders tclvl skol_info outer_bndrs hs_outer_bndrs wcs lhs_ty wanted
; (final_tvs, non_user_tvs, lhs_ty, master_res_kind, instance_res_kind, stupid_theta) <-
liftZonkM $ do
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/881da0f013b84e1226adceb1bbe7e6c006232e35
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/881da0f013b84e1226adceb1bbe7e6c006232e35
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/20250310/fabb110c/attachment-0001.html>
More information about the ghc-commits
mailing list