diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index dfebb878138165aff98aefe8a50531a8ffb0a922..d540272a5356b3dcd689c25ed727d8d5bcdbc466 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1483,19 +1483,15 @@ canCFunEqCan ev fn tys fsk
; return (ev', fsk) }
else do { (ev', new_co, new_fsk)
<- newFlattenSkolem flav (ctEvLoc ev) fn tys'
- ; case flav of
- Given -> return () -- nothing more to do.
- -- NB: new_co is stored within ev',
- -- and will be put in the flat_cache below
- _ -> do { let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
- -- sym lhs_co :: F tys ~ F tys'
- -- new_co :: F tys' ~ new_fsk
- -- co :: F tys ~ (new_fsk |> kind_co)
- co = mkTcSymCo lhs_co `mkTcTransCo`
- (new_co `mkTcCoherenceRightCo` kind_co)
-
- ; traceTcS "Discharging fmv due to hetero flattening" empty
- ; dischargeFmv ev fsk co xi }
+ ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
+ -- sym lhs_co :: F tys ~ F tys'
+ -- new_co :: F tys' ~ new_fsk
+ -- co :: F tys ~ (new_fsk |> kind_co)
+ co = mkTcSymCo lhs_co `mkTcTransCo`
+ (new_co `mkTcCoherenceRightCo` kind_co)
+
+ ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev)
+ ; dischargeFunEq ev fsk co xi
; return (ev', new_fsk) }
; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev')
@@ -1588,16 +1584,12 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
| CtGiven { ctev_evar = evar } <- ev
-- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
-- swapped : tm :: (rhs :: ki2) ~ (lhs :: ki1)
- = do { kind_ev_id <- newBoundEvVarId kind_pty
- (evCoercion $ mkTcKindCo $ mkTcCoVarCo evar)
- -- kind_ev_id :: (ki1 :: *) ~ (ki2 :: *) (whether swapped or not)
- ; let kind_ev = CtGiven { ctev_pred = kind_pty
- , ctev_evar = kind_ev_id
- , ctev_loc = kind_loc }
+ = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar)
+ ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
+ ; let -- kind_ev :: (ki1 :: *) ~ (ki2 :: *) (whether swapped or not)
-- co1 :: kind(tv1) ~N ki1
-- homo_co :: ki2 ~N kind(tv1)
- homo_co = mkTcSymCo (mkCoVarCo kind_ev_id) `mkTcTransCo` mkTcSymCo co1
-
+ homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
rhs' = mkCastTy xi2 homo_co -- :: kind(tv1)
ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1)
rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
@@ -1608,7 +1600,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
-- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
; traceTcS "Hetero equality gives rise to given kind equality"
- (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
+ (ppr kind_ev <+> dcolon <+> ppr kind_pty)
; emitWorkNC [kind_ev]
; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 09cfd15a3002b97c8d0cf7dc5597c40bd3237998..b2be509b698a8569087cb83fc4380777353f7f2b 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1432,20 +1432,9 @@ reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
-> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
-> TcS ()
reactFunEq from_this fsk1 solve_this fsk2
- | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
- = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
- ctEvCoercion from_this
- -- :: fsk2 ~ fsk1
- fsk_eq_pred = mkTcEqPredLikeEv solve_this
- (mkTyVarTy fsk2) (mkTyVarTy fsk1)
-
- ; new_ev <- newGivenEvVar loc (fsk_eq_pred, evCoercion fsk_eq_co)
- ; emitWorkNC [new_ev] }
-
- | otherwise -- Wanted
- = do { traceTcS "reactFunEq (Wanted/Derived)"
+ = do { traceTcS "reactFunEq"
(vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
- ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
+ ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
ppr solve_this $$ ppr fsk2) }
@@ -1892,40 +1881,25 @@ reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
-> TcS (StopOrContinue Ct)
-- We have found an applicable top-level axiom: use it to reduce
-- Precondition: fsk is not free in rhs_ty
--- old_ev is not Derived
reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
- | isDerived old_ev
- = do { emitNewDerivedEq loc Nominal (mkTyVarTy fsk) rhs_ty
- ; stopWith old_ev "Fun/Top (derived)" }
-
- | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
+ | not (isDerived old_ev) -- Precondition of shortCutReduction
+ , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
, isTypeFamilyTyCon tc
, tc_args `lengthIs` tyConArity tc -- Short-cut
= -- RHS is another type-family application
-- Try shortcut; see Note [Top-level reductions for type functions]
- shortCutReduction old_ev fsk ax_co tc tc_args
-
- | isGiven old_ev -- Not shortcut
- = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
- -- final_co :: fsk ~ rhs_ty
- ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
- evCoercion final_co)
- ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
- ; stopWith old_ev "Fun/Top (given)" }
+ do { shortCutReduction old_ev fsk ax_co tc tc_args
+ ; stopWith old_ev "Fun/Top (shortcut)" }
- | otherwise -- So old_ev is Wanted (cannot be Derived)
+ | otherwise
= ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
, ppr old_ev $$ ppr rhs_ty )
-- Guaranteed by Note [FunEq occurs-check principle]
- do { dischargeFmv old_ev fsk ax_co rhs_ty
+ do { dischargeFunEq old_ev fsk ax_co rhs_ty
; traceTcS "doTopReactFunEq" $
vcat [ text "old_ev:" <+> ppr old_ev
, nest 2 (text ":=") <+> ppr ax_co ]
- ; stopWith old_ev "Fun/Top (wanted)" }
-
- where
- loc = ctEvLoc old_ev
- deeper_loc = bumpCtLocDepth loc
+ ; stopWith old_ev "Fun/Top" }
improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
-- See Note [FunDep and implicit parameter reactions]
@@ -2020,7 +1994,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
- -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
+ -> TyCon -> [TcType] -> TcS ()
-- See Note [Top-level reductions for type functions]
-- Previously, we flattened the tc_args here, but there's no need to do so.
-- And, if we did, this function would have all the complication of
@@ -2045,8 +2019,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
, cc_tyargs = tc_args, cc_fsk = fsk }
- ; updWorkListTcS (extendWorkListFunEq new_ct)
- ; stopWith old_ev "Fun/Top (shortcut)" }
+ ; updWorkListTcS (extendWorkListFunEq new_ct) }
where
deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index f5d6ca9aa7553d2b6ee3998bdc51a3f9c84d8081..d26275b83976665508df20fc1cd06b49540ece29 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -83,7 +83,7 @@ module TcSMonad (
-- The flattening cache
lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems
- dischargeFmv, pprKicked,
+ dischargeFunEq, pprKicked,
-- Inert CFunEqCans
updInertFunEqs, findFunEq,
@@ -3044,12 +3044,14 @@ demoteUnfilledFmv fmv
; TcM.writeMetaTyVar fmv tv_ty } }
-----------------------------
-dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv ev fmv co ty)
--- [W] ev :: F tys ~ fmv
--- co :: F tys ~ xi
--- Precondition: fmv is not filled, and fmv `notElem` xi
--- ev is Wanted or Derived
+dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
+-- (dischargeFunEqCan ev tv co ty)
+-- Preconditions
+-- - ev :: F tys ~ tv is a CFunEqCan
+-- - tv is a FlatMetaTv of FlatSkolTv
+-- - co :: F tys ~ xi
+-- - fmv/fsk `notElem` xi
+-- - fmv not filled (for Wanteds)
--
-- Then for [W] or [WD], we actually fill in the fmv:
-- set fmv := xi,
@@ -3057,24 +3059,32 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- kick out any inert things that are now rewritable
--
-- For [D], we instead emit an equality that must ultimately hold
--- emit xi ~ fmv
+-- [D] xi ~ fmv
-- Does not evaluate 'co' if 'ev' is Derived
--
+-- For [G], emit this equality
+-- [G] (sym ev; co) :: fsk ~ xi
+
-- See TcFlatten Note [The flattening story],
-- especially "Ownership of fsk/fmv"
-dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
+dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
+ = do { new_ev <- newGivenEvVar loc ( new_pred, evCoercion new_co )
+ ; emitWorkNC [new_ev] }
+ where
+ new_pred = mkPrimEqPred (mkTyVarTy fsk) xi
+ new_co = mkTcSymCo (mkTcCoVarCo old_evar) `mkTcTransCo` co
+
+dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi
= ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
do { setWantedEvTerm dest (EvExpr (evCoercion co))
; unflattenFmv fmv xi
; n_kicked <- kickOutAfterUnification fmv
; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
-dischargeFmv (CtDerived { ctev_loc = loc }) fmv _co xi
+dischargeFunEq (CtDerived { ctev_loc = loc }) fmv _co xi
= emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
-- FunEqs are always at Nominal role
-dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
-
pprKicked :: Int -> SDoc
pprKicked 0 = empty
pprKicked n = parens (int n <+> text "kicked out")
diff --git a/testsuite/tests/indexed-types/should_compile/T15122.hs b/testsuite/tests/indexed-types/should_compile/T15122.hs
new file mode 100644
index 0000000000000000000000000000000000000000..44a3c0523f128adc589ec46ab32708d175ea24ca
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15122.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T15122 where
+
+import Data.Kind
+import Data.Proxy
+
+data IsStar (a :: k) where
+ IsStar :: IsStar (a :: *)
+
+type family F (a :: k) :: k
+
+foo :: (F a ~ F b) => IsStar a -> Proxy b
+ -> Proxy (F a) -> Proxy (F b)
+foo IsStar _ p = p
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 9f0d9b4a8d8ff24781de3ebbeff7bbe2c3291341..5a6ae27aac414f71a1e33a470039d6794d3291f0 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -281,3 +281,4 @@ test('T14554', normal, compile, [''])
test('T14680', normal, compile, [''])
test('T15057', normal, compile, [''])
test('T15144', normal, compile, [''])
+test('T15122', normal, compile, [''])