[Git][ghc/ghc][wip/T24676] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue May 28 22:44:37 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
af68929f by Simon Peyton Jones at 2024-05-28T23:43:50+01:00
More wibbles
- - - - -
4 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -342,31 +342,43 @@ tcApp rn_expr exp_res_ty
-- Instantiate
; do_ql <- wantQuickLook rn_fun
- ; (inst_args, app_res_rho, res_wrap)
+ ; (inst_args, app_res_rho)
<- setQLInstLevel do_ql $
- do { (inst_args, app_res_rho) <- tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
- ; res_wrap <- unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
- ; return (inst_args, app_res_rho, res_wrap) }
+ tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
-- Monomorphise any leftover instantiation variables
- ; case do_ql of
- DoQL -> monomorphiseQLInstVars inst_args app_res_rho
- NoQL -> return ()
+ ; res_wrap <- case do_ql of
+ NoQL -> case exp_res_ty of
+ Check res_ty ->
+ unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
+ Infer inf_res ->
+ do { co <- fillInferResult app_res_rho inf_res
+ ; return (mkWpCastN co) }
+
+ DoQL -> case exp_res_ty of
+ Check res_ty ->
+ do { res_wrap <- unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
+ ; monomorphiseQLInstVars inst_args app_res_rho
+ ; return res_wrap }
+ Infer inf_res ->
+ do { monomorphiseQLInstVars inst_args app_res_rho
+ ; co <- fillInferResult app_res_rho inf_res
+ ; return (mkWpCastN co) }
-- Typecheck the arguments
- ; tc_app <- finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
+ ; tc_app <- finishApp fun_ctxt tc_fun inst_args app_res_rho
; return (mkHsWrap res_wrap tc_app) }
setQLInstLevel :: QLFlag -> TcM a -> TcM a
setQLInstLevel DoQL thing_inside = setTcLevel QLInstVar thing_inside
setQLInstLevel NoQL thing_inside = thing_inside
-finishApp :: QLFlag -> AppCtxt
+finishApp :: AppCtxt
-> HsExpr GhcTc -> [HsExprArg 'TcpInst]
-> TcRhoType
-> TcM (HsExpr GhcTc)
-- At this point there are no more instantiation variables
-finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
+finishApp fun_ctxt tc_fun inst_args app_res_rho
= do { -- Typecheck the value arguments
; tc_args <- tcValArgs inst_args
@@ -381,7 +393,6 @@ finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
; whenDOptM Opt_D_dump_tc_trace $
do { inst_args <- liftZonkM $ mapM zonkArg inst_args -- Only when tracing
; traceTc "tcApp }" (vcat [ text "inst_args" <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
- , text "do_ql: " <+> ppr do_ql
, text "app_res_rho:" <+> ppr app_res_rho
, text "tc_fun:" <+> ppr tc_fun
, text "tc_args:" <+> ppr tc_args
@@ -392,31 +403,38 @@ finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
unifyResTy :: HsExpr GhcRn -> AppCtxt -> HsExpr GhcTc
-> [HsExprArg p]
- -> TcType -> ExpRhoType
+ -> TcType -> TcRhoType
-> TcM HsWrapper
-unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
+unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
-- Unify with expected type from the context
-- See Note [Unify with expected type before typechecking arguments]
--
-- Match up app_res_rho: the result type of rn_expr
--- with exp_res_ty: the expected result type
+-- with res_ty: the expected result type
= perhaps_add_res_ty_ctxt $
- do { ds_flag <- getDeepSubsumptionFlag
+ do { traceTc "unifyResTy {" $
+ vcat [ text "tc_fun:" <+> ppr tc_fun
+ , text "app_res_rho:" <+> ppr app_res_rho
+ , text "res_ty:" <+> ppr res_ty ]
+ ; ds_flag <- getDeepSubsumptionFlag
; case ds_flag of
Shallow -> -- No deep subsumption
- -- app_res_rho and exp_res_ty are both rho-types,
+ -- app_res_rho and res_ty are both rho-types,
-- so with simple subsumption we can just unify them
-- No need to zonk; the unifier does that
- do { co <- unifyExpectedType rn_expr app_res_rho exp_res_ty
+ do { co <- unifyExprType rn_expr app_res_rho res_ty
+ ; traceTc "unifyResTy 1 }" (ppr co)
; return (mkWpCastN co) }
Deep -> -- Deep subsumption
- -- Even though both app_res_rho and exp_res_ty are rho-types,
+ -- Even though both app_res_rho and res_ty are rho-types,
-- they may have nested polymorphism, so if deep subsumption
-- is on we must call tcSubType.
-- No need to zonk app_res_rho first; although QL may have instantiated some
-- delta variables to polytypes, tcSubType can cope with that
- tcSubTypeDS rn_expr app_res_rho exp_res_ty }
+ do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
+ ; traceTc "unifyResTy 2 }" (ppr wrap)
+ ; return wrap } }
where
-- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
-- more confusing than helpful because the function at the head isn't in
@@ -426,7 +444,7 @@ unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
| insideExpansion fun_ctxt
= addHeadCtxt fun_ctxt thing_inside
| otherwise
- = addFunResCtxt tc_fun inst_args app_res_rho exp_res_ty $
+ = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $
thing_inside
@@ -506,7 +524,7 @@ tcValArg (EValArgQL { eaql_status = ql_status
tcScalingUsage mult $
case ql_status of
QLUnified res_wrap
- -> do { tc_app <- finishApp DoQL ctxt tc_fun inst_args res_rho
+ -> do { tc_app <- finishApp ctxt tc_fun inst_args res_rho
; return (EValArg { ea_ctxt = ctxt
, ea_arg = L arg_loc (mkHsWrap res_wrap tc_app)
, ea_arg_ty = noExtField }) }
@@ -525,9 +543,9 @@ tcValArg (EValArgQL { eaql_status = ql_status
; (wrap, arg')
<- tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
do { emitConstraints wc
- ; res_wrap <- unifyResTy rn_expr ctxt tc_fun inst_args res_rho (mkCheckExpType arg_rho)
+ ; res_wrap <- unifyResTy rn_expr ctxt tc_fun inst_args res_rho arg_rho
; monomorphiseQLInstVars inst_args res_rho
- ; tc_app <- finishApp DoQL ctxt tc_fun inst_args res_rho
+ ; tc_app <- finishApp ctxt tc_fun inst_args res_rho
; return (mkHsWrap res_wrap tc_app) }
; traceTc "tcEValArgQL }" $
@@ -1743,8 +1761,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
-- No skolemisation of orig_arg_ty needed here:
-- tcIsDeepRho checked that there are no foralls to skolemise
do { emitConstraints wanted
- ; res_wrap <- unifyResTy arg fun_ctxt tc_fun inst_args app_res_rho
- (mkCheckExpType orig_arg_rho)
+ ; res_wrap <- unifyResTy arg fun_ctxt tc_fun inst_args app_res_rho orig_arg_rho
; traceTc "quickLookArg unify" (ppr rn_fun)
; return (mk_ql_arg (QLUnified res_wrap)) }
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1821,6 +1821,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
, text "lhs:" <+> ppr lhs
, text "rhs:" <+> ppr rhs ]
+ -- Assertion: no QL instantiation tyvars
+-- ; massertPpr (not (ql_inst_tv lhs)) (ppr lhs)
+
-- Assertion: (TyEq:K) is already satisfied
; massert (canEqLHSKind lhs `eqType` typeKind rhs)
@@ -1832,6 +1835,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
; canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs }
where
+ ql_inst_tv (TyVarLHS tv) = isQLInstTyVar tv
+ ql_inst_tv (TyFamLHS {}) = False
+
-- This is about (TyEq:N): check that we don't have a saturated application
-- of a newtype TyCon at the top level of the RHS, if the constructor
-- of the newtype is in scope.
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -55,7 +55,8 @@ module GHC.Tc.Utils.TcType (
isConcreteTyVarTy, isConcreteTyVarTy_maybe, isConcreteInfo,
ConcreteTyVars, noConcreteTyVars,
isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
- isFlexi, isIndirect, isRuntimeUnkSkol, isQLInstTyVar,
+ isFlexi, isIndirect, isRuntimeUnkSkol,
+ isQLInstTyVar, isRuntimeUnkTyVar,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
isTouchableMetaTyVar, isPromotableMetaTyVar,
findDupTyVarTvs, mkTyVarNamePairs,
@@ -1201,6 +1202,12 @@ isQLInstTyVar tv
MetaTv { mtv_tclvl = QLInstVar } -> True
_ -> False
+isRuntimeUnkTyVar :: TcTyVar -> Bool
+isRuntimeUnkTyVar tv
+ = case tcTyVarDetails tv of
+ MetaTv { mtv_info = RuntimeUnkTv } -> True
+ _ -> False
+
isCycleBreakerTyVar tv
| isTyVar tv -- See Note [Coercion variables in free variable lists]
, MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -24,7 +24,7 @@ module GHC.Tc.Utils.Unify (
-- Various unifications
unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
- unifyTypeAndEmit, promoteTcType,
+ unifyExprType, unifyTypeAndEmit, promoteTcType,
swapOverTyVars, touchabilityAndShapeTest,
UnifyEnv(..), updUEnvLoc, setUEnvRole,
uType,
@@ -1326,22 +1326,16 @@ tcSubType orig ctxt ty_actual ty_expected
---------------
tcSubTypeDS :: HsExpr GhcRn
-> TcRhoType -- Actual type -- a rho-type not a sigma-type
- -> ExpRhoType -- Expected type
+ -> TcRhoType -- Expected type
-- DeepSubsumption <=> when checking, this type
-- is deeply skolemised
-> TcM HsWrapper
-- Similar signature to unifyExpectedType; does deep subsumption
-- Only one call site, in GHC.Tc.Gen.App.tcApp
-tcSubTypeDS rn_expr act_rho res_ty
- = case res_ty of
- Check exp_rho -> tc_sub_type_deep (unifyType m_thing) orig
- GenSigCtxt act_rho exp_rho
-
- Infer inf_res -> do { co <- fillInferResult act_rho inf_res
- ; return (mkWpCastN co) }
+tcSubTypeDS rn_expr act_rho exp_rho
+ = tc_sub_type_deep (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
where
- orig = exprCtOrigin rn_expr
- m_thing = Just (HsExprRnThing rn_expr)
+ orig = exprCtOrigin rn_expr
---------------
tcSubTypeNC :: CtOrigin -- ^ Used when instantiating
@@ -1972,6 +1966,10 @@ The exported functions are all defined as versions of some
non-exported generic functions.
-}
+unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> TcM TcCoercionN
+unifyExprType rn_expr ty1 ty2
+ = unifyType (Just (HsExprRnThing rn_expr)) ty1 ty2
+
unifyType :: Maybe TypedThing -- ^ If present, the thing that has type ty1
-> TcTauType -> TcTauType -- ty1 (actual), ty2 (expected)
-> TcM TcCoercionN -- :: ty1 ~# ty2
@@ -2448,7 +2446,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
-- /any/ level outside this one as untouchable. Hence cur_lvl.
; if not (touchabilityAndShapeTest cur_lvl tv1 ty2
&& simpleUnifyCheck False tv1 ty2)
- then not_ok_so_defer
+ then not_ok_so_defer cur_lvl
else
do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs
@@ -2481,8 +2479,12 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
ty1 = mkTyVarTy tv1
defer = unSwap swapped (uType_defer env) ty1 ty2
- not_ok_so_defer =
- do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
+ not_ok_so_defer cur_lvl =
+ do { traceTc "uUnfilledVar2 not ok" $
+ vcat [ text "tv1:" <+> ppr tv1
+ , text "ty2:" <+> ppr ty2
+ , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck False tv1 ty2)
+ , text "touchability:" <+> ppr (touchabilityAndShapeTest cur_lvl tv1 ty2)]
-- Occurs check or an untouchable: just defer
-- NB: occurs check isn't necessarily fatal:
-- eg tv1 occurred in type family parameter
@@ -2870,45 +2872,48 @@ matchExpectedFunKind hs_ty n k = go n k
* *
********************************************************************* -}
-simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool
+simpleUnifyCheck :: Bool -- True <=> called from constraint solver
+ -- False <=> called from on-the-fly unifier
+ -> TcTyVar -> TcType -> Bool
-- A fast check: True <=> unification is OK
-- If it says 'False' then unification might still be OK, but
-- it'll take more work to do -- use the full checkTypeEq
--
--- * Always rejects foralls unless lhs_tv is RuntimeUnk
--- (used by GHCi debugger)
+-- * Rejects foralls unless
+-- lhs_tv is RuntimeUnk (used by GHCi debugger)
+-- or is a QL instantiation variable
-- * Rejects a non-concrete type if lhs_tv is concrete
-- * Rejects type families unless fam_ok=True
-- * Does a level-check for type variables
--
-- This function is pretty heavily used, so it's optimised not to allocate
-simpleUnifyCheck fam_ok lhs_tv rhs
+simpleUnifyCheck called_from_solver lhs_tv rhs
= go rhs
where
+ fam_ok = called_from_solver || is_ql_inst_tv
+
!(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv
lhs_tv_lvl = tcTyVarLevel lhs_tv
lhs_tv_is_concrete = isConcreteTyVar lhs_tv
- forall_ok = case tcTyVarDetails lhs_tv of
- MetaTv { mtv_info = RuntimeUnkTv } -> True
- MetaTv { mtv_tclvl = QLInstVar } -> True
- _ -> False
+ is_ql_inst_tv = isQLInstTyVar lhs_tv
+ forall_ok = is_ql_inst_tv || isRuntimeUnkTyVar lhs_tv
go (TyVarTy tv)
- | lhs_tv == tv = False
- | tcTyVarLevel tv > lhs_tv_lvl = False
- | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False
- | occ_in_ty $! (tyVarKind tv) = False
- | otherwise = True
+ | lhs_tv == tv = False
+ | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False
+ | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False
+ | occ_in_ty $! (tyVarKind tv) = False
+ | otherwise = True
go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
- | isInvisibleFunArg af, not forall_ok = False
+ | not forall_ok, isInvisibleFunArg af = False
| otherwise = go w && go a && go r
go (TyConApp tc tys)
| lhs_tv_is_concrete, not (isConcreteTyCon tc) = False
- | not (isTauTyCon tc) = False
- | not fam_ok, not (isFamFreeTyCon tc) = False
+ | not forall_ok, not (isTauTyCon tc) = False
+ | not fam_ok, not (isFamFreeTyCon tc) = False
| otherwise = all go tys
go (ForAllTy (Bndr tv _) ty)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/af68929f22b6fd62c06e2fd4cc1d979f5d9ba9ea
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/af68929f22b6fd62c06e2fd4cc1d979f5d9ba9ea
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/20240528/6e8232ce/attachment-0001.html>
More information about the ghc-commits
mailing list