[Git][ghc/ghc][wip/T23070-unify] First steps killing unifyWanted
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sun Apr 2 09:03:55 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
1f90b89f by Simon Peyton Jones at 2023-04-02T10:05:12+01:00
First steps killing unifyWanted
- - - - -
6 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1932,7 +1932,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind
; if act_kind' `tcEqType` exp_kind
then return res_ty -- This is very common
- else do { co_k <- uType KindLevel origin act_kind' exp_kind
+ else do { co_k <- uTypeAndEmit KindLevel origin act_kind' exp_kind
; traceTc "checkExpectedKind" (vcat [ ppr act_kind
, ppr exp_kind
, ppr co_k ])
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -653,9 +653,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
can_eq_app ev s1 t1 s2 t2
| CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
= do { co_s <- unifyWanted rewriters loc Nominal s1 s2
- ; let arg_loc
- | isNextArgVisible s1 = loc
- | otherwise = updateCtLocOrigin loc toInvisibleOrigin
+ ; let arg_loc = adjustCtLoc (isNextArgVisible s1) False loc
; co_t <- unifyWanted rewriters arg_loc Nominal t1 t2
; let co = mkAppCo co_s co_t
; setWantedEq dest co
@@ -1213,14 +1211,8 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-- do either of these changes. (Forgetting to do so led to #16188)
--
-- NB: infinite in length
- new_locs = [ new_loc
- | bndr <- tyConBinders tc
- , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
- | otherwise = loc
- new_loc | isInvisibleTyConBinder bndr
- = updateCtLocOrigin new_loc0 toInvisibleOrigin
- | otherwise
- = new_loc0 ]
+ new_locs = [ adjustCtLocTyConBinder bndr loc
+ | bndr <- tyConBinders tc ]
++ repeat loc
canDecomposableFunTy :: CtEvidence -> EqRel -> FunTyFlag
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -8,7 +8,7 @@ module GHC.Tc.Solver.InertSet (
-- * The work list
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
- extendWorkListCts, extendWorkListEq,
+ extendWorkListCts, extendWorkListEq, extendWorkListEqs,
appendWorkList, extendWorkListImplic,
workListSize,
selectWorkItem,
@@ -179,6 +179,9 @@ workListSize (WL { wl_eqs = eqs, wl_rest = rest })
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
+extendWorkListEqs :: [Ct] -> WorkList -> WorkList
+extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl }
+
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -179,7 +179,6 @@ import GHC.Data.Bag as Bag
import GHC.Data.Pair
import GHC.Utils.Monad
-import GHC.Utils.Misc( equalLength )
import GHC.Exts (oneShot)
import Control.Monad
@@ -1954,6 +1953,20 @@ unifyWanted :: RewriterSet -> CtLoc
-- Very good short-cut when the two types are equal, or nearly so
-- See Note [unifyWanted]
-- The returned coercion's role matches the input parameter
+
+unifyWanted _rewriters loc role ty1 ty2
+ = do { (co,cts) <- wrapTcS $
+ do { ref <- TcM.newTcRef []
+ ; let env = UE { u_role = role
+ , u_loc = loc
+ , u_defer = ref }
+ ; co <- uType env ty1 ty2
+ ; cts <- TcM.readTcRef ref
+ ; return (co, cts) }
+ ; updWorkListTcS (extendWorkListEqs cts)
+ ; return co }
+
+{-
unifyWanted rewriters loc Phantom ty1 ty2
= do { kind_co <- unifyWanted rewriters loc Nominal (typeKind ty1) (typeKind ty2)
; return (mkPhantomCo kind_co ty1 ty2) }
@@ -1998,7 +2011,7 @@ unifyWanted rewriters loc role orig_ty1 orig_ty2
| ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
-- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
| otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2
-
+-}
{-
Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -67,7 +67,7 @@ module GHC.Tc.Types.Constraint (
ctLocTypeOrKind_maybe,
ctLocDepth, bumpCtLocDepth, isGivenLoc,
setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
- pprCtLoc,
+ pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder,
-- CtEvidence
CtEvidence(..), TcEvDest(..),
@@ -2394,10 +2394,11 @@ dictionaries don't appear in the original source code.
-}
-data CtLoc = CtLoc { ctl_origin :: CtOrigin
- , ctl_env :: TcLclEnv
- , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure
- , ctl_depth :: !SubGoalDepth }
+data CtLoc
+ = CtLoc { ctl_origin :: CtOrigin
+ , ctl_env :: TcLclEnv
+ , ctl_t_or_k :: Maybe TypeOrKind -- Used only to improve error messages
+ , ctl_depth :: !SubGoalDepth }
-- The TcLclEnv includes particularly
-- source location: tcl_loc :: RealSrcSpan
@@ -2411,6 +2412,26 @@ mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
(KindEqOrigin s1 s2 (ctLocOrigin loc)
(ctLocTypeOrKind_maybe loc))
+adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
+-- Adjust the CtLoc when decomposing a type constructor
+adjustCtLocTyConBinder tc_bndr loc
+ = adjustCtLoc is_invis is_kind loc
+ where
+ is_invis = isInvisibleTyConBinder tc_bndr
+ is_kind = isNamedTyConBinder tc_bndr
+
+adjustCtLoc :: Bool -- True <=> An invisible argument
+ -> Bool -- True <=> A kind argument
+ -> CtLoc -> CtLoc
+-- Adjust the CtLoc when decomposing a type constructor, application, etc
+adjustCtLoc is_invis is_kind loc
+ = loc2
+ where
+ loc1 | is_kind = toKindLoc loc
+ | otherwise = loc
+ loc2 | is_invis = updateCtLocOrigin loc1 toInvisibleOrigin
+ | otherwise = loc1
+
-- | Take a CtLoc and moves it to the kind level
toKindLoc :: CtLoc -> CtLoc
toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -21,8 +21,9 @@ module GHC.Tc.Utils.Unify (
-- Various unifications
unifyType, unifyKind, unifyExpectedType,
- uType, promoteTcType,
+ uTypeAndEmit, promoteTcType,
swapOverTyVars, touchabilityAndShapeTest,
+ UnifyEnv(..), uType,
--------------------------------
-- Holes
@@ -1145,7 +1146,7 @@ tcEqMult origin w_actual w_expected = do
{
-- Note that here we do not call to `submult`, so we check
-- for strict equality.
- ; coercion <- uType TypeLevel origin w_actual w_expected
+ ; coercion <- uTypeAndEmit TypeLevel origin w_actual w_expected
; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
@@ -1711,7 +1712,7 @@ unifyType :: Maybe TypedThing -- ^ If present, the thing that has type ty1
-- Actual and expected types
-- Returns a coercion : ty1 ~ ty2
unifyType thing ty1 ty2
- = uType TypeLevel origin ty1 ty2
+ = uTypeAndEmit TypeLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty1
, uo_expected = ty2
@@ -1722,7 +1723,7 @@ unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
-- Like unifyType, but swap expected and actual in error messages
-- This is used when typechecking patterns
unifyTypeET ty1 ty2
- = uType TypeLevel origin ty1 ty2
+ = uTypeAndEmit TypeLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped
, uo_expected = ty1 -- NB swapped
@@ -1732,13 +1733,26 @@ unifyTypeET ty1 ty2
unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN
unifyKind mb_thing ty1 ty2
- = uType KindLevel origin ty1 ty2
+ = uTypeAndEmit KindLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty1
, uo_expected = ty2
, uo_thing = mb_thing
, uo_visible = True }
+uTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
+-- Make a ref-cell, unify, emit the collected constraints
+uTypeAndEmit t_or_k orig ty1 ty2
+ = do { ref <- newTcRef []
+ ; loc <- getCtLocM orig (Just t_or_k)
+ ; let env = UE { u_loc = loc, u_role = Nominal, u_defer = ref }
+
+ -- The hard work happens here
+ ; co <- uType env ty1 ty2
+
+ ; cts <- readTcRef ref
+ ; unless (null cts) (emitSimples (listToBag cts))
+ ; return co }
{-
%************************************************************************
@@ -1750,42 +1764,67 @@ unifyKind mb_thing ty1 ty2
uType is the heart of the unifier.
-}
+data UnifyEnv
+ = UE { u_role :: Role
+ , u_loc :: CtLoc
+ , u_defer :: TcRef [Ct] }
+
+mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
+-- Modify the UnifyEnv to be right for unifing
+-- the kinds of these two types
+mkKindEnv env@(UE { u_loc = ctloc }) ty1 ty2
+ | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc
+ , let kind_origin = KindEqOrigin ty1 ty2 origin t_or_k
+ = env { u_role = Nominal
+ , u_loc = ctloc { ctl_origin = kind_origin
+ , ctl_t_or_k = Just KindLevel } }
+
uType, uType_defer
- :: TypeOrKind
- -> CtOrigin
+ :: UnifyEnv
-> TcType -- ty1 is the *actual* type
-> TcType -- ty2 is the *expected* type
-> TcM CoercionN
---------------
-- It is always safe to defer unification to the main constraint solver
-- See Note [Deferred unification]
--- ty1 is "actual"
--- ty2 is "expected"
-uType_defer t_or_k origin ty1 ty2
- = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
+uType_defer (UE { u_loc = loc, u_defer = ref, u_role = role })
+ ty1 ty2 -- ty1 is "actual", ty2 is "expected"
+ = do { let pred_ty = mkPrimEqPredRole role ty1 ty2
+ ; hole <- newCoercionHole pred_ty
+ ; let ct = mkNonCanonical $
+ CtWanted { ctev_pred = pred_ty
+ , ctev_dest = HoleDest hole
+ , ctev_loc = loc
+ , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] }
+ co = HoleCo hole
+ ; updTcRef ref (ct :)
-- Error trace only
-- NB. do *not* call mkErrInfo unless tracing is on,
-- because it is hugely expensive (#5631)
- ; whenDOptM Opt_D_dump_tc_trace $ do
- { ctxt <- getErrCtxt
- ; doc <- mkErrInfo emptyTidyEnv ctxt
+ ; whenDOptM Opt_D_dump_tc_trace $
+ do { ctxt <- getErrCtxt
+ ; doc <- mkErrInfo emptyTidyEnv ctxt
; traceTc "utype_defer" (vcat [ debugPprType ty1
, debugPprType ty2
- , pprCtOrigin origin
, doc])
- ; traceTc "utype_defer2" (ppr co)
- }
+ ; traceTc "utype_defer2" (ppr co) }
+
; return co }
+
--------------
-uType t_or_k origin orig_ty1 orig_ty2
+uType env@(UE { u_role = role }) orig_ty1 orig_ty2
+ | Phantom <- role
+ = do { kind_co <- uType (mkKindEnv env orig_ty1 orig_ty2)
+ (typeKind orig_ty1) (typeKind orig_ty2)
+ ; return (mkPhantomCo kind_co orig_ty1 orig_ty2) }
+
+ | otherwise
= do { tclvl <- getTcLevel
; traceTc "u_tys" $ vcat
[ text "tclvl" <+> ppr tclvl
- , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
- , pprCtOrigin origin]
+ , sep [ ppr orig_ty1, text "~", ppr orig_ty2] ]
; co <- go orig_ty1 orig_ty2
; if isReflCo co
then traceTc "u_tys yields no coercion" Outputable.empty
@@ -1800,12 +1839,12 @@ uType t_or_k origin orig_ty1 orig_ty2
-- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
-- didn't do it this way, and then the unification above was deferred.
go (CastTy t1 co1) t2
- = do { co_tys <- uType t_or_k origin t1 t2
- ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
+ = do { co_tys <- uType env t1 t2
+ ; return (mkCoherenceLeftCo role t1 co1 co_tys) }
go t1 (CastTy t2 co2)
- = do { co_tys <- uType t_or_k origin t1 t2
- ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
+ = do { co_tys <- uType env t1 t2
+ ; return (mkCoherenceRightCo role t2 co2 co_tys) }
-- Variables; go for uUnfilledVar
-- Note that we pass in *original* (before synonym expansion),
@@ -1816,18 +1855,18 @@ uType t_or_k origin orig_ty1 orig_ty2
; case lookup_res of
Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
; go ty1 ty2 }
- Nothing -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
+ Nothing -> uUnfilledVar env NotSwapped tv1 ty2 }
go ty1 (TyVarTy tv2)
= do { lookup_res <- isFilledMetaTyVar_maybe tv2
; case lookup_res of
Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
; go ty1 ty2 }
- Nothing -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
+ Nothing -> uUnfilledVar env IsSwapped tv2 ty1 }
-- See Note [Expanding synonyms during unification]
go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
| tc1 == tc2
- = return $ mkNomReflCo ty1
+ = return $ mkReflCo role ty1
-- See Note [Expanding synonyms during unification]
--
@@ -1842,14 +1881,14 @@ uType t_or_k origin orig_ty1 orig_ty2
| Just ty2' <- coreView ty2 = go ty1 ty2'
-- Functions (t1 -> t2) just check the two parts
- -- Do not attempt (c => t); just defer
go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
(FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
- | isVisibleFunArg af1, af1 == af2
- = do { co_l <- uType t_or_k origin arg1 arg2
- ; co_r <- uType t_or_k origin res1 res2
- ; co_w <- uType t_or_k origin w1 w2
- ; return $ mkNakedFunCo1 Nominal af1 co_w co_l co_r }
+ | isVisibleFunArg af1 -- Do not attempt (c => t); just defer
+ , af1 == af2 -- Important! See #21530
+ = do { co_w <- uType (env { u_role = funRole role SelMult }) w1 w2
+ ; co_l <- uType (env { u_role = funRole role SelArg }) arg1 arg2
+ ; co_r <- uType (env { u_role = funRole role SelRes }) res1 res2
+ ; return $ mkNakedFunCo1 role af1 co_w co_l co_r }
-- Always defer if a type synonym family (type function)
-- is involved. (Data families behave rigidly.)
@@ -1861,41 +1900,39 @@ uType t_or_k origin orig_ty1 orig_ty2
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-- See Note [Mismatched type lists and application decomposition]
| tc1 == tc2, equalLength tys1 tys2
- = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $
- do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
- ; return $ mkTyConAppCo Nominal tc1 cos }
- where
- origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
- (tcTyConVisibilities tc1)
+ , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
+ = assertPpr (isGenerativeTyCon tc1 role) (ppr tc1) $
+ do { cos <- zipWith4M u_tc_arg (tyConBinders tc1)
+ (tyConRoleListX role tc1)
+ tys1 tys2
+ ; return $ mkTyConAppCo role tc1 cos }
go (LitTy m) ty@(LitTy n)
| m == n
- = return $ mkNomReflCo ty
+ = return $ mkReflCo role ty
-- See Note [Care with type applications]
-- Do not decompose FunTy against App;
-- it's often a type error, so leave it for the constraint solver
- go (AppTy s1 t1) (AppTy s2 t2)
- = go_app (isNextArgVisible s1) s1 t1 s2 t2
+ go ty1@(AppTy s1 t1) ty2@(AppTy s2 t2)
+ = go_app (isNextArgVisible s1) ty1 s1 t1 ty2 s2 t2
- go (AppTy s1 t1) (TyConApp tc2 ts2)
+ go ty1@(AppTy s1 t1) ty2@(TyConApp tc2 ts2)
| Just (ts2', t2') <- snocView ts2
= assert (not (tyConMustBeSaturated tc2)) $
- go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
+ go_app (isNextTyConArgVisible tc2 ts2')
+ ty1 s1 t1 ty2 (TyConApp tc2 ts2') t2'
- go (TyConApp tc1 ts1) (AppTy s2 t2)
+ go ty1@(TyConApp tc1 ts1) ty2@(AppTy s2 t2)
| Just (ts1', t1') <- snocView ts1
= assert (not (tyConMustBeSaturated tc1)) $
- go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
+ go_app (isNextTyConArgVisible tc1 ts1')
+ ty1 (TyConApp tc1 ts1') t1' ty2 s2 t2
- go (CoercionTy co1) (CoercionTy co2)
- = do { let ty1 = coercionType co1
- ty2 = coercionType co2
- ; kco <- uType KindLevel
- (KindEqOrigin orig_ty1 orig_ty2 origin
- (Just t_or_k))
- ty1 ty2
- ; return $ mkProofIrrelCo Nominal kco co1 co2 }
+ go ty1@(CoercionTy co1) ty2@(CoercionTy co2)
+ = do { kco <- uType (mkKindEnv env ty1 ty2)
+ (coercionType co1) (coercionType co2)
+ ; return $ mkProofIrrelCo role kco co1 co2 }
-- Anything else fails
-- E.g. unifying for-all types, which is relative unusual
@@ -1903,17 +1940,28 @@ uType t_or_k origin orig_ty1 orig_ty2
------------------
defer ty1 ty2 -- See Note [Check for equality before deferring]
- | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
- | otherwise = uType_defer t_or_k origin ty1 ty2
+ | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
+ | otherwise = uType_defer env ty1 ty2
+
------------------
- go_app vis s1 t1 s2 t2
- = do { co_s <- uType t_or_k origin s1 s2
- ; let arg_origin
- | vis = origin
- | otherwise = toInvisibleOrigin origin
- ; co_t <- uType t_or_k arg_origin t1 t2
+ u_tc_arg tc_bndr role ty1 ty2
+ = uType env_arg ty1 ty2
+ where
+ env_arg = env { u_loc = adjustCtLocTyConBinder tc_bndr (u_loc env)
+ , u_role = role }
+
+ ------------------
+ -- For AppTy, decompose only nominal equalities
+ -- See Note [Decomposing AppTy equalities] in GHC.Tc.Solver.Equality
+ go_app vis ty1 s1 t1 ty2 s2 t2
+ | Nominal <- role
+ = do { co_s <- uType env s1 s2
+ ; let env_arg = env { u_loc = adjustCtLoc vis False (u_loc env) }
+ ; co_t <- uType env_arg t1 t2
; return $ mkAppCo co_s co_t }
+ | otherwise
+ = defer ty1 ty2
{- Note [Check for equality before deferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2009,45 +2057,36 @@ back into @uTys@ if it turns out that the variable is already bound.
-}
----------
-uUnfilledVar :: CtOrigin
- -> TypeOrKind
- -> SwapFlag
- -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
- -- definitely not a /filled/ meta-tyvar
- -> TcTauType -- Type 2
- -> TcM Coercion
+uUnfilledVar, uUnfilledVar1
+ :: UnifyEnv
+ -> SwapFlag
+ -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
+ -- definitely not a /filled/ meta-tyvar
+ -> TcTauType -- Type 2
+ -> TcM CoercionN
-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
-- It might be a skolem, or untouchable, or meta
-uUnfilledVar origin t_or_k swapped tv1 ty2
- = do { ty2 <- zonkTcType ty2
- -- Zonk to expose things to the
- -- occurs check, and so that if ty2
- -- looks like a type variable then it
- -- /is/ a type variable
- ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
+uUnfilledVar env swapped tv1 ty2
+ = do { ty2 <- zonkTcType ty2 -- Zonk to expose things to the
+ -- occurs check, and so that if ty2
+ -- looks like a type variable then it
+ -- /is/ a type variable
+ ; uUnfilledVar1 env swapped tv1 ty2 }
-----------
-uUnfilledVar1 :: CtOrigin
- -> TypeOrKind
- -> SwapFlag
- -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
- -- definitely not a /filled/ meta-tyvar
- -> TcTauType -- Type 2, zonked
- -> TcM Coercion
-uUnfilledVar1 origin t_or_k swapped tv1 ty2
+uUnfilledVar1 env@(UE { u_role = role }) swapped tv1 ty2 -- ty2 is zonked
| Just tv2 <- getTyVar_maybe ty2
= go tv2
| otherwise
- = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+ = uUnfilledVar2 env swapped tv1 ty2
where
-- 'go' handles the case where both are
-- tyvars so we might want to swap
-- E.g. maybe tv2 is a meta-tyvar and tv1 is not
go tv2 | tv1 == tv2 -- Same type variable => no-op
- = return (mkNomReflCo (mkTyVarTy tv1))
+ = return (mkReflCo role (mkTyVarTy tv1))
| swapOverTyVars False tv1 tv2 -- Distinct type variables
-- Swap meta tyvar to the left if poss
@@ -2056,21 +2095,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
-- not have happened yet, and it's an invariant of
-- uUnfilledTyVar2 that ty2 is fully zonked
-- Omitting this caused #16902
- ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
- tv2 (mkTyVarTy tv1) }
+ ; uUnfilledVar2 env (flipSwap swapped) tv2 (mkTyVarTy tv1) }
| otherwise
- = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+ = uUnfilledVar2 env swapped tv1 ty2
----------
-uUnfilledVar2 :: CtOrigin
- -> TypeOrKind
+uUnfilledVar2 :: UnifyEnv
-> SwapFlag
-> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
-- definitely not a /filled/ meta-tyvar
-> TcTauType -- Type 2, zonked
- -> TcM Coercion
-uUnfilledVar2 origin t_or_k swapped tv1 ty2
+ -> TcM CoercionN
+uUnfilledVar2 env@(UE { u_role = role }) swapped tv1 ty2
= do { cur_lvl <- getTcLevel
-- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
-- Here we don't know about given equalities here; so we treat
@@ -2079,7 +2116,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
&& simpleUnifyCheck False tv1 ty2)
then not_ok_so_defer
else
- do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1)
+ do { co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
, ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
@@ -2090,7 +2127,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
-- NB: tv1 should still be unfilled, despite the kind unification
-- because tv1 is not free in ty2' (or, hence, in its kind)
then do { writeMetaTyVar tv1 ty2
- ; return (mkNomReflCo ty2) }
+ ; return (mkReflCo role ty2) }
else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical
-- Note [Equalities with incompatible kinds] for how
@@ -2098,9 +2135,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
}}
where
ty1 = mkTyVarTy tv1
- kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
-
- defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
+ defer = unSwap swapped (uType_defer env) ty1 ty2
not_ok_so_defer =
do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
@@ -2514,7 +2549,7 @@ matchExpectedFunKind hs_ty n k = go n k
, uo_thing = Just hs_ty
, uo_visible = True
}
- ; uType KindLevel origin k new_fun }
+ ; uTypeAndEmit KindLevel origin k new_fun }
{- *********************************************************************
* *
@@ -3228,4 +3263,3 @@ checkTopShape info xi
_ -> False
CycleBreakerTv -> False -- We never unify these
_ -> True
-
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f90b89fdf71e49bf6a69d8813ed34bafbe189a2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f90b89fdf71e49bf6a69d8813ed34bafbe189a2
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/20230402/5dd25b49/attachment-0001.html>
More information about the ghc-commits
mailing list