[Git][ghc/ghc][wip/T23070-unify] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Apr 29 14:38:06 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
f2ad5ba8 by Simon Peyton Jones at 2023-04-29T15:39:36+01:00
More wibbles
- - - - -
14 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/rep-poly/T13929.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -39,8 +39,8 @@ module GHC.Core.Coercion (
mkSymCo, mkTransCo,
mkSelCo, getNthFun, getNthFromType, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
- mkFunCo1, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
- mkNakedFunCo1, mkNakedFunCo2,
+ mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
+ mkNakedFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
@@ -811,29 +811,20 @@ mkFunCoNoFTF r w arg_co res_co
-- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b at .
-- This (most common) version takes a single FunTyFlag, which is used
-- for both fco_afl and ftf_afr of the FunCo
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo1 r af w arg_co res_co
+mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo r af w arg_co res_co
= mkFunCo2 r af af w arg_co res_co
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
--- This version of mkFunCo1 does not check FunCo invariants (checkFunCo)
--- It is called during typechecking on un-zonked types;
--- in particular there may be un-zonked coercion variables.
-mkNakedFunCo1 r af w arg_co res_co
- = mkNakedFunCo2 r af af w arg_co res_co
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This version of mkFunCo does not check FunCo invariants (checkFunCo)
+-- It's a historical vestige; See Note [No assertion check on mkFunCo]
+mkNakedFunCo = mkFunCo
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag
- -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag
+ -> CoercionN -> Coercion -> Coercion -> Coercion
-- This is the smart constructor for FunCo; it checks invariants
mkFunCo2 r afl afr w arg_co res_co
- = assertPprMaybe (checkFunCo r afl afr w arg_co res_co) $
- mkNakedFunCo2 r afl afr w arg_co res_co
-
-mkNakedFunCo2 :: Role -> FunTyFlag -> FunTyFlag
- -> CoercionN -> Coercion -> Coercion -> Coercion
--- This is the smart constructor for FunCo
--- "Naked"; it does not check invariants
-mkNakedFunCo2 r afl afr w arg_co res_co
+ -- See Note [No assertion check on mkFunCo]
| Just (ty1, _) <- isReflCo_maybe arg_co
, Just (ty2, _) <- isReflCo_maybe res_co
, Just (w, _) <- isReflCo_maybe w
@@ -844,6 +835,19 @@ mkNakedFunCo2 r afl afr w arg_co res_co
, fco_mult = w, fco_arg = arg_co, fco_res = res_co }
+{- Note [No assertion check on mkFunCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used to have a checkFunCo assertion on mkFunCo, but during typechecking
+we can (legitimately) have not-full-zonked types or coercion variables, so
+the assertion spuriously fails (test T11480b is a case in point). Lint
+checks all these things anyway.
+
+We used to get around the problem by calling mkNakedFunCo from within the
+typechecker, which dodged the assertion check. But then mkAppCo calls
+mkTyConAppCo, which calls tyConAppFunCo_maybe, which calls mkFunCo.
+Duplicating this stack of calls with "naked" versions of each seems too much.
+
+-- Commented out: see Note [No assertion check on mkFunCo]
checkFunCo :: Role -> FunTyFlag -> FunTyFlag
-> CoercionN -> Coercion -> Coercion
-> Maybe SDoc
@@ -875,6 +879,7 @@ checkFunCo _r afl afr _w arg_co res_co
ok ty = isTYPEorCONSTRAINT (typeKind ty)
pp_ty str ty = text str <> colon <+> hang (ppr ty)
2 (dcolon <+> ppr (typeKind ty))
+-}
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
@@ -2068,7 +2073,7 @@ ty_co_subst !lc role ty
liftCoSubstTyVar lc r tv
go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys)
- go r (FunTy af w t1 t2) = mkFunCo1 r af (go Nominal w) (go r t1) (go r t2)
+ go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2)
go r t@(ForAllTy (Bndr v _) ty)
= let (lc', v', h) = liftCoSubstVarBndr lc v
body_co = ty_co_subst lc' r ty in
@@ -2658,7 +2663,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
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 })
= assert (af1 == af2) $
- mkFunCo1 Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
+ mkFunCo Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
go (TyConApp tc1 args1) (TyConApp tc2 args2)
= assert (tc1 == tc2) $
@@ -2745,7 +2750,7 @@ has_co_hole_co :: Coercion -> Monoid.Any
-- | Is there a hetero-kind coercion hole in this type?
-- (That is, a coercion hole with ch_hetero_kind=True.)
--- See wrinkle (2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
+-- See wrinkle (W2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -17,9 +17,9 @@ mkReflCo :: Role -> Type -> Coercion
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkAppCo :: Coercion -> Coercion -> Coercion
mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkCoVarCo :: CoVar -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
=====================================
compiler/GHC/Core/Reduction.hs
=====================================
@@ -361,8 +361,8 @@ mkFunRedn r af
(Reduction arg_co arg_ty)
(Reduction res_co res_ty)
= mkReduction
- (mkFunCo1 r af w_co arg_co res_co)
- (mkFunTy af w_ty arg_ty res_ty)
+ (mkFunCo r af w_co arg_co res_co)
+ (mkFunTy af w_ty arg_ty res_ty)
{-# INLINE mkFunRedn #-}
-- | Create a 'Reduction' associated to a Π type,
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1459,7 +1459,7 @@ data CoercionHole
, ch_hetero_kind :: Bool
-- True <=> arises from a kind-level equality
-- See Note [Equalities with incompatible kinds]
- -- in GHC.Tc.Solver.Equality, wrinkle (2)
+ -- in GHC.Tc.Solver.Equality, wrinkle (W2)
}
coHoleCoVar :: CoercionHole -> CoVar
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -273,7 +273,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
, mkTyConAppCo, mkAppCo
, mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
- , mkKindCo, mkSubCo, mkFunCo1
+ , mkKindCo, mkSubCo, mkFunCo
, decomposePiCos, coercionKind
, coercionRKind, coercionType
, isReflexiveCo, seqCo
@@ -1329,7 +1329,7 @@ tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion]
-- ^ Return Just if this TyConAppCo should be represented as a FunCo
tyConAppFunCo_maybe r tc cos
| Just (af, mult, arg, res) <- ty_con_app_fun_maybe (mkReflCo r manyDataConTy) tc cos
- = Just (mkFunCo1 r af mult arg res)
+ = Just (mkFunCo r af mult arg res)
| otherwise = Nothing
ty_con_app_fun_maybe :: (HasDebugCallStack, Outputable a) => a -> TyCon -> [a]
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1672,7 +1672,7 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
return (main_msg, [])
-- Incompatible kinds
- -- This is wrinkle (4) in Note [Equalities with incompatible kinds]
+ -- This is wrinkle (W2) in Note [Equalities with incompatible kinds]
-- in GHC.Tc.Solver.Equality
| hasCoercionHoleCo co1 || hasCoercionHoleTy ty2
= return (mkBlockedEqErr item, [])
@@ -1856,7 +1856,7 @@ misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2
-- See Note [Suppress redundant givens during error reporting]
-- These are for the "blocked" equalities, as described in TcCanonical
--- Note [Equalities with incompatible kinds], wrinkle (2). There should
+-- Note [Equalities with incompatible kinds], wrinkle (W2). There should
-- always be another unsolved wanted around, which will ordinarily suppress
-- this message. But this can still be printed out with -fdefer-type-errors
-- (sigh), so we must produce a message.
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -4520,7 +4520,7 @@ data TcSolverReportMsg
| BlockedEquality ErrorItem
-- These are for the "blocked" equalities, as described in
-- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical,
- -- wrinkle (2). There should always be another unsolved wanted around,
+ -- wrinkle (W2). There should always be another unsolved wanted around,
-- which will ordinarily suppress this message. But this can still be printed out
-- with -fdefer-type-errors (sigh), so we must produce a message.
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -388,7 +388,7 @@ kcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM ()
-- meth :: forall a (x :: f a). Proxy x -> ()
-- When instantiating Proxy with kappa, we must unify kappa := f a. But we're
-- still working out the kind of f, and thus f a will have a coercion in it.
--- Coercions block unification (Note [Equalities with incompatible kinds] in
+-- Coercions may block unification (Note [Equalities with incompatible kinds] in
-- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll
-- end up promoting kappa to the top level (because kind-generalization is
-- normally done right before adding a binding to the context), and then we
@@ -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 <- uTypeAndEmit KindLevel origin act_kind' exp_kind
+ else do { co_k <- unifyTypeAndEmit KindLevel origin act_kind' exp_kind
; traceTc "checkExpectedKind" (vcat [ ppr act_kind
, ppr exp_kind
, ppr co_k ])
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -872,10 +872,6 @@ doLocalFunDepImprovement :: Ct -> TcS Bool
doLocalFunDepImprovement (CDictCan { cc_ev = work_ev, cc_class = cls })
= do { inerts <- getInertCans
; foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) }
- -- No need to check flavour; fundeps work between
- -- any pair of constraints, regardless of flavour
- -- Importantly we don't throw workitem back in the
- -- worklist because this can cause loops (see #5236)
where
work_pred = ctEvPred work_ev
work_loc = ctEvLoc work_ev
@@ -895,8 +891,6 @@ doLocalFunDepImprovement (CDictCan { cc_ev = work_ev, cc_class = cls })
; unifs <- emitFunDepWanteds work_ev $
improveFromAnother (derived_loc, inert_rewriters)
inert_pred work_pred
- -- We don't really rewrite tys2, see below
- -- _rewritten_tys2, so that's ok
; return (so_far || unifs)
}
where
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -179,10 +179,10 @@ can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-- Then, get rid of casts
can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
- | isNothing (canEqLHS_maybe ty2) -- See (3) in Note [Equalities with incompatible kinds]
+ | isNothing (canEqLHS_maybe ty2) -- See (W3) in Note [Equalities with incompatible kinds]
= canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
- | isNothing (canEqLHS_maybe ty1) -- See (3) in Note [Equalities with incompatible kinds]
+ | isNothing (canEqLHS_maybe ty1) -- See (W3) in Note [Equalities with incompatible kinds]
= canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
----------------------
@@ -1277,7 +1277,7 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2)
; mult <- uType mult_env m1 m2
; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2
; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2
- ; return (mkNakedFunCo1 role af mult arg res) }
+ ; return (mkNakedFunCo role af mult arg res) }
; setWantedEq dest co }
CtGiven { ctev_evar = evar }
@@ -1508,12 +1508,10 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
-- kind_co :: ki2 ~# ki1 -- Same orientiation as ev
-- type_ev :: (xi2 |> kind_co) ~r# lhs1
- = do { (kind_co, rewriters) <- mk_kind_eq -- :: ki1 ~N ki2
- ; if isWanted ev && isEmptyRewriterSet rewriters
- -- Made kinds equal with no deferred rewrites so we must have done
- -- some unifications; start again to do the zonking
- -- For Givens we never want to go round again,
- -- and the rewriter set is empty, so we must check isWanted.
+ = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq -- :: ki1 ~N ki2
+ ; if unifs_happened
+ -- Unifications happened, so start again to do the zonking
+ -- Otherwise we might put something in the inert set that isn't inert
then startAgainWith (mkNonCanonical ev)
else
do { let lhs_redn = mkReflRedn role ps_xi1
@@ -1531,7 +1529,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }}
where
- mk_kind_eq :: TcS (CoercionN, RewriterSet)
+ mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool)
-- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped
-- Returned Bool = True if unifications happened, so we should retry
mk_kind_eq = case ev of
@@ -1541,13 +1539,13 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
kind_loc = mkKindEqLoc xi1 xi2 (ctev_loc ev)
; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
; emitWorkNC [kind_ev]
- ; return (ctEvCoercion kind_ev, emptyRewriterSet) }
+ ; return (ctEvCoercion kind_ev, emptyRewriterSet, False) }
CtWanted {}
- -> do { (kind_co, cts, _) <- wrapUnifierTcS ev Nominal $ \uenv ->
- let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
- in unSwap swapped (uType uenv') ki1 ki2
- ; return (kind_co, rewriterSetFromCts cts) }
+ -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
+ let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
+ in unSwap swapped (uType uenv') ki1 ki2
+ ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) }
xi1 = canEqLHSType lhs1
role = eqRelRole eq_rel
@@ -1942,12 +1940,12 @@ k2 and use this to cast. To wit, from
Wrinkles:
- (1) When X is W, the new type-level wanted is effectively rewritten by the
+(W1) When X is W, the new type-level wanted is effectively rewritten by the
kind-level one. We thus include the kind-level wanted in the RewriterSet
for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
This is done in canEqCanLHSHetero.
- (2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce
+(W2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce
[W] w : a ~ (b |> kw)
[W] kw : Type ~ (Type->Type)
@@ -1965,13 +1963,13 @@ Wrinkles:
Instead, it lands in the inert_irreds in the inert set, awaiting solution of
that `kw`.
- (2a) We must later indeed unify if/when the kind-level wanted, `kw` gets
+ (W2a) We must later indeed unify if/when the kind-level wanted, `kw` gets
solved. This is done in kickOutAfterFillingCoercionHole, which kicks out
all equalities whose RHS mentions the filled-in coercion hole. Note that
it looks for type family equalities, too, because of the use of unifyTest
in canEqTyVarFunEq.
- (2b) What if the RHS mentions /other/ coercion holes. How can that happen? The
+ (W2b) What if the RHS mentions /other/ coercion holes. How can that happen? The
main way is like this. Assume F :: forall k. k -> Type
[W] kw : k ~ Type
[W] w : a ~ F k t
@@ -1979,7 +1977,8 @@ Wrinkles:
[W] w' : a ~ F Type (t |> kw)
The cast on the second argument of `F` is necessary to keep the appliation well-kinded.
There is nothing special here; no reason not treat w' as canonical, and use it for
- rewriting. Indeed tests JuanLopez only typechecks if we do.
+ rewriting. Indeed tests JuanLopez only typechecks if we do. So we'd like to treat
+ this kind of equality as canonical.
Hence the ch_hetero_kind field in CoercionHole: it is True of constraints
created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise:
@@ -1991,7 +1990,7 @@ Wrinkles:
KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends. We
set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`.
- (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
+(W3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
algorithm detailed here, producing [W] co :: k1 ~ k2, and adding
[W] (a :: k1) ~ ((rhs |> sym co) :: k1) to the irreducibles. Some time
later, we solve co, and fill in co's coercion hole. This kicks out
@@ -2749,9 +2748,9 @@ like the right thing to do.
When this was originally conceived, it was necessary to avoid a loop in T13135.
That loop is now avoided by continuing with the kind equality (not the type
-equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds]
-in GHC.Tc.Solver.Canonical). However, the idea of working left-to-right still
-seems worthwhile, and so the calls to 'reverse' remain.
+equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds]).
+However, the idea of working left-to-right still seems worthwhile, and so the calls
+to 'reverse' remain.
Note [Improvement orientation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -419,7 +419,7 @@ kickOutAfterUnification new_tv
; setInertCans ics2
; return n_kicked }
--- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+-- See Wrinkle (W2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
-- It's possible that this could just go ahead and unify, but could there be occurs-check
-- problems? Seems simpler just to kick out.
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -230,7 +230,7 @@ mkWpEta xs wrap = foldr eta_one wrap xs
mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
mk_wp_fun_co mult arg_co res_co
- = mkNakedFunCo1 Representational FTF_T_T (multToCo mult) arg_co res_co
+ = mkNakedFunCo Representational FTF_T_T (multToCo mult) arg_co res_co
-- FTF_T_T: WpFun is always (->)
mkWpCastR :: TcCoercionR -> HsWrapper
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -21,7 +21,7 @@ module GHC.Tc.Utils.Unify (
-- Various unifications
unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
- uTypeAndEmit, promoteTcType,
+ unifyTypeAndEmit, promoteTcType,
swapOverTyVars, touchabilityAndShapeTest,
UnifyEnv(..), updUEnvLoc, setUEnvRole,
uType,
@@ -1147,7 +1147,7 @@ tcEqMult origin w_actual w_expected = do
{
-- Note that here we do not call to `submult`, so we check
-- for strict equality.
- ; coercion <- uTypeAndEmit TypeLevel origin w_actual w_expected
+ ; coercion <- unifyTypeAndEmit TypeLevel origin w_actual w_expected
; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
@@ -1713,7 +1713,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
- = uTypeAndEmit TypeLevel origin ty1 ty2
+ = unifyTypeAndEmit TypeLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty1
, uo_expected = ty2
@@ -1725,18 +1725,18 @@ unifyInvisibleType :: TcTauType -> TcTauType -- ty1 (actual), ty2 (expected)
-- Actual and expected types
-- Returns a coercion : ty1 ~ ty2
unifyInvisibleType ty1 ty2
- = uTypeAndEmit TypeLevel origin ty1 ty2
+ = unifyTypeAndEmit TypeLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty1
, uo_expected = ty2
, uo_thing = Nothing
- , uo_visible = False }
+ , uo_visible = False } -- This is the "invisible" bit
unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
-- Like unifyType, but swap expected and actual in error messages
-- This is used when typechecking patterns
unifyTypeET ty1 ty2
- = uTypeAndEmit TypeLevel origin ty1 ty2
+ = unifyTypeAndEmit TypeLevel origin ty1 ty2
where
origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped
, uo_expected = ty1 -- NB swapped
@@ -1746,16 +1746,16 @@ unifyTypeET ty1 ty2
unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN
unifyKind mb_thing ty1 ty2
- = uTypeAndEmit KindLevel origin ty1 ty2
+ = unifyTypeAndEmit 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
+unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
-- Make a ref-cell, unify, emit the collected constraints
-uTypeAndEmit t_or_k orig ty1 ty2
+unifyTypeAndEmit t_or_k orig ty1 ty2
= do { ref <- newTcRef emptyBag
; loc <- getCtLocM orig (Just t_or_k)
; let env = UE { u_loc = loc, u_role = Nominal
@@ -1931,7 +1931,7 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
= 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 }
+ ; return $ mkNakedFunCo role af1 co_w co_l co_r }
-- Always defer if a type synonym family (type function)
-- is involved. (Data families behave rigidly.)
@@ -2320,8 +2320,9 @@ There are five reasons not to unify:
Suppose our equality is
(alpha :: k) ~ (Int |> {co})
where co :: Type ~ k is an unsolved wanted. Note that this equality
- is homogeneous; both sides have kind k. We refrain from unifying here --
- see Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Solver.Equality.
+ is homogeneous; both sides have kind k. We refrain from unifying here, because
+ of the coercion hold in the RHS -- see Wrinkle (W2) in
+ Note [Equalities with incompatible kinds] in GHC.Solver.Equality.
Needless to say, all there are wrinkles:
@@ -2591,7 +2592,7 @@ matchExpectedFunKind hs_ty n k = go n k
go n (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res })
| isVisibleFunArg af
= do { co <- go (n-1) res
- ; return (mkNakedFunCo1 Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) }
+ ; return (mkNakedFunCo Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) }
go n other
= defer n other
@@ -2605,7 +2606,7 @@ matchExpectedFunKind hs_ty n k = go n k
, uo_thing = Just hs_ty
, uo_visible = True
}
- ; uTypeAndEmit KindLevel origin k new_fun }
+ ; unifyTypeAndEmit KindLevel origin k new_fun }
{- *********************************************************************
* *
=====================================
testsuite/tests/rep-poly/T13929.stderr
=====================================
@@ -3,7 +3,7 @@ T13929.hs:29:24: error: [GHC-55287]
• The tuple argument in first position
does not have a fixed runtime representation.
Its type is:
- a0 :: TYPE k00
+ GUnboxed f rf :: TYPE k00
Cannot unify ‘rf’ with the type variable ‘k00’
because it is not a concrete ‘RuntimeRep’.
• In the expression: (# gunbox x, gunbox y #)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f2ad5ba81bd998afa2947add6a9187e9f97dcf35
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f2ad5ba81bd998afa2947add6a9187e9f97dcf35
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/20230429/da27aa0b/attachment-0001.html>
More information about the ghc-commits
mailing list