[Git][ghc/ghc][wip/T23070-unify] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Apr 7 11:26:35 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
ec8d3344 by Simon Peyton Jones at 2023-04-07T12:28:09+01:00
Wibbles
- - - - -
6 changed files:
- 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/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -652,10 +652,13 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- See Note [Decomposing AppTy equalities]
can_eq_app ev s1 t1 s2 t2
| CtWanted { ctev_dest = dest } <- ev
- = do { (co,_) <- unifyWanteds ev Nominal $ \uenv ->
- do { co_s <- uType uenv s1 s2
- ; let arg_env = updUEnvLoc uenv (adjustCtLoc (isNextArgVisible s1) False)
+ = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1
+ , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2
+ , text "vis:" <+> ppr (isNextArgVisible s1) ])
+ ; (co,_) <- unifyWanteds ev Nominal $ \uenv ->
+ do { let arg_env = updUEnvLoc uenv (adjustCtLoc (isNextArgVisible s1) False)
; co_t <- uType arg_env t1 t2
+ ; co_s <- uType uenv s1 s2
; return (mkAppCo co_s co_t) }
; setWantedEq dest co
; stopWith ev "Decomposed [W] AppTy" }
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -179,8 +179,10 @@ 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 }
+extendWorkListEqs :: Bag Ct -> WorkList -> WorkList
+-- Add [eq1,...,eqn] to the work-list, retaining order
+extendWorkListEqs eqs wl
+ = wl { wl_eqs = foldr (:) (wl_eqs wl) eqs }
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1977,7 +1977,7 @@ unifyWanteds :: CtEvidence -> Role
-- Return coercions witnessing the equality of the two types,
-- emitting new work equalities where necessary to achieve that
-- Very good short-cut when the two types are equal, or nearly so
--- See Note [unifyWanted]
+-- See Note [unifyWanteds]
-- The returned coercion's role matches the input parameter
--
-- The [TcTyVar] is the list of unification variables
@@ -1985,7 +1985,7 @@ unifyWanteds :: CtEvidence -> Role
unifyWanteds ev role do_unifications
= do { (cos, unified, cts) <- wrapTcS $
- do { defer_ref <- TcM.newTcRef []
+ do { defer_ref <- TcM.newTcRef emptyBag
; unified_ref <- TcM.newTcRef []
; let env = UE { u_role = role
, u_rewriters = ctEvRewriters ev
@@ -2000,7 +2000,8 @@ unifyWanteds ev role do_unifications
; return (cos, unified, cts) }
-- Emit the deferred constraints
- ; updWorkListTcS (extendWorkListEqs cts)
+ ; unless (isEmptyBag cts) $
+ updWorkListTcS (extendWorkListEqs cts)
-- And kick out any inert constraint that we have unified
-- ToDo: treating the tyvars together might
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -2415,22 +2415,22 @@ mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
-- Adjust the CtLoc when decomposing a type constructor
adjustCtLocTyConBinder tc_bndr loc
- = adjustCtLoc is_invis is_kind loc
+ = adjustCtLoc is_vis is_kind loc
where
- is_invis = isInvisibleTyConBinder tc_bndr
- is_kind = isNamedTyConBinder tc_bndr
+ is_vis = isVisibleTyConBinder tc_bndr
+ is_kind = isNamedTyConBinder tc_bndr
-adjustCtLoc :: Bool -- True <=> An invisible argument
+adjustCtLoc :: Bool -- True <=> A visible argument
-> Bool -- True <=> A kind argument
-> CtLoc -> CtLoc
-- Adjust the CtLoc when decomposing a type constructor, application, etc
-adjustCtLoc is_invis is_kind loc
+adjustCtLoc is_vis is_kind loc
= loc2
where
loc1 | is_kind = toKindLoc loc
| otherwise = loc
- loc2 | is_invis = toInvisibleLoc loc1
- | otherwise = loc1
+ loc2 | is_vis = loc1
+ | otherwise = toInvisibleLoc loc1
-- | Take a CtLoc and moves it to the kind level
toKindLoc :: CtLoc -> CtLoc
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -2321,10 +2321,11 @@ isNextTyConArgVisible tc tys
= tcTyConVisibilities tc `getNth` length tys
-- | Should this type be applied to a visible argument?
+-- E.g. (s t): is `t` a visible argument of `s`?
isNextArgVisible :: TcType -> Bool
isNextArgVisible ty
- | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisiblePiTyBinder bndr
- | otherwise = True
+ | Just (bndr, _) <- tcSplitPiTy_maybe (typeKind ty) = isVisiblePiTyBinder bndr
+ | otherwise = True
-- this second case might happen if, say, we have an unzonked TauTv.
-- But TauTvs can't range over types that take invisible arguments
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1744,7 +1744,7 @@ unifyKind mb_thing ty1 ty2
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 []
+ = do { ref <- newTcRef emptyBag
; loc <- getCtLocM orig (Just t_or_k)
; let env = UE { u_loc = loc, u_role = Nominal
, u_rewriters = emptyRewriterSet -- ToDo: check this
@@ -1754,7 +1754,7 @@ uTypeAndEmit t_or_k orig ty1 ty2
; co <- uType env ty1 ty2
; cts <- readTcRef ref
- ; unless (null cts) (emitSimples (listToBag cts))
+ ; unless (null cts) (emitSimples cts)
; return co }
{-
@@ -1773,7 +1773,7 @@ data UnifyEnv
, u_rewriters :: RewriterSet
-- Deferred constraints
- , u_defer :: TcRef [Ct]
+ , u_defer :: TcRef (Bag Ct)
-- Which variables are unified;
-- if Nothing, we don't care
@@ -1815,7 +1815,7 @@ uType_defer (UE { u_loc = loc, u_defer = ref
, ctev_loc = loc
, ctev_rewriters = rewriters }
co = HoleCo hole
- ; updTcRef ref (ct :)
+ ; updTcRef ref (`snocBag` ct)
-- Error trace only
-- NB. do *not* call mkErrInfo unless tracing is on,
@@ -2135,7 +2135,7 @@ uUnfilledVar2 :: UnifyEnv
-- definitely not a /filled/ meta-tyvar
-> TcTauType -- Type 2, zonked
-> TcM CoercionN
-uUnfilledVar2 env swapped tv1 ty2
+uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) 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
@@ -2144,7 +2144,8 @@ uUnfilledVar2 env swapped tv1 ty2
&& simpleUnifyCheck False tv1 ty2)
then not_ok_so_defer
else
- do { co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1)
+ do { def_eqs <- readTcRef def_eq_ref
+ ; 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)
@@ -2160,9 +2161,13 @@ uUnfilledVar2 env swapped tv1 ty2
Just uref -> updTcRef uref (tv1 :)
; return (mkNomReflCo ty2) } -- Unification is always Nominal
- else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical
- -- Note [Equalities with incompatible kinds] for how
- -- this will be dealt with in the solver
+ else -- This cannot be solved now. See GHC.Tc.Solver.Canonical
+ -- Note [Equalities with incompatible kinds] for how this
+ -- will be dealt with in the solver
+ -- Since we are discarding co_k, also discard any constraints
+ -- emitted by kind unification; they are just useless clutter.
+ do { writeTcRef def_eq_ref def_eqs
+ ; defer }
}}
where
ty1 = mkTyVarTy tv1
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ec8d3344bce8fceddc158e1c4ce9e5e31695e4a2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ec8d3344bce8fceddc158e1c4ce9e5e31695e4a2
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/20230407/c9d0f912/attachment-0001.html>
More information about the ghc-commits
mailing list