[Git][ghc/ghc][wip/forall-vis-coercions] Refactoring
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 14 11:42:25 UTC 2023
Simon Peyton Jones pushed to branch wip/forall-vis-coercions at Glasgow Haskell Compiler / GHC
Commits:
148e83df by Simon Peyton Jones at 2023-06-14T12:40:58+01:00
Refactoring
I have just added to Matthew's patch
* Record type for ForAllCo
* Refactor can_eq_nc_forall to use uType
* Deall with mis-matched foralls in can_eq_nc_forall
- - - - -
17 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Types/Var.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,7 +41,7 @@ module GHC.Core.Coercion (
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
mkNakedFunCo,
- mkForAllCo, mkForAllCos, mkHomoForAllCos,
+ mkForAllCo, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
@@ -557,19 +557,25 @@ splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res)
splitFunCo_maybe _ = Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-splitForAllCo_maybe (ForAllCo tv vL vR k_co co) = Just (tv, vL, vR, k_co, co)
+splitForAllCo_maybe (ForAllCo { fco_tcv = tv, fco_visL = vL, fco_visR = vR
+ , fco_kind = k_co, fco_body = co })
+ = Just (tv, vL, vR, k_co, co)
splitForAllCo_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-splitForAllCo_ty_maybe (ForAllCo tv vL vR k_co co)
- | isTyVar tv = Just (tv, vL, vR, k_co, co)
+splitForAllCo_ty_maybe co
+ | Just stuff@(tv, _, _, _, _) <- splitForAllCo_maybe co
+ , isTyVar tv
+ = Just stuff
splitForAllCo_ty_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-splitForAllCo_co_maybe (ForAllCo cv vL vR k_co co)
- | isCoVar cv = Just (cv, vL, vR, k_co, co)
+splitForAllCo_co_maybe co
+ | Just stuff@(cv, _, _, _, _) <- splitForAllCo_maybe co
+ , isCoVar cv
+ = Just stuff
splitForAllCo_co_maybe _ = Nothing
@@ -972,7 +978,8 @@ mkForAllCo v visL visR kind_co co
, visL `eqForAllVis` visR
= mkReflCo r (mkTyCoForAllTy v visL ty)
| otherwise
- = ForAllCo v visL visR kind_co co
+ = ForAllCo { fco_tcv = v, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co }
-- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
-- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
@@ -987,21 +994,8 @@ mkForAllCo_NoRefl v visL visR kind_co co
= mkFunCoNoFTF (coercionRole co) (multToCo ManyTy) kind_co co
-- Functions from coercions are always unrestricted
| otherwise
- = ForAllCo v visL visR kind_co co
-
--- | Make nested ForAllCos, with 'Specified' visibility
-mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
--- We don't seem to use this for anything as of Apr 2023
-mkForAllCos bndrs co
- | Just (ty, r ) <- isReflCo_maybe co
- = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
- foldl' (flip step)
- (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
- non_refls_rev'd
- | otherwise
- = foldr step co bndrs
- where step (tcv, kind_co) inner_co
- = mkForAllCo_NoRefl tcv Specified Specified kind_co inner_co
+ = ForAllCo { fco_tcv = v, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co }
-- | Make a Coercion quantified over a type/coercion variable;
-- the variable has the same kind and visibility in both sides of the coercion
@@ -1171,7 +1165,7 @@ mkSelCo_maybe cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo r (getNthFromType cs ty))
- go SelForAll (ForAllCo _ _ _ kind_co _)
+ go SelForAll (ForAllCo { fco_kind = kind_co })
= Just kind_co
-- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
-- then (nth SelForAll co :: k1 ~N k2)
@@ -1239,7 +1233,7 @@ mkLRCo lr co
-- | Instantiates a 'Coercion'.
mkInstCo :: Coercion -> CoercionN -> Coercion
-mkInstCo (ForAllCo tcv _visL _visR _kind_co body_co) co
+mkInstCo (ForAllCo { fco_tcv = tcv, fco_body = body_co }) co
| Just (arg, _) <- isReflCo_maybe co
-- works for both tyvar and covar
= substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
@@ -1391,9 +1385,10 @@ setNominalRole_maybe r co
= TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
setNominalRole_maybe_helper (AppCo co1 co2)
= AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
- setNominalRole_maybe_helper (ForAllCo tv visL visR kind_co co)
+ setNominalRole_maybe_helper co@(ForAllCo { fco_visL = visL, fco_visR = visR, fco_body = body_co })
| visL `eqForAllVis` visR
- = ForAllCo tv visL visR kind_co <$> setNominalRole_maybe_helper co
+ = do { body_co' <- setNominalRole_maybe_helper body_co
+ ; return (co { fco_body = body_co' }) }
setNominalRole_maybe_helper (SelCo cs co) =
-- NB, this case recurses via setNominalRole_maybe, not
-- setNominalRole_maybe_helper!
@@ -1513,7 +1508,7 @@ promoteCoercion co = case co of
| otherwise
-> mkKindCo co
- ForAllCo tv _ _ _ g
+ ForAllCo { fco_tcv = tv, fco_body = g }
| isTyVar tv
-> promoteCoercion g
@@ -1671,7 +1666,7 @@ mkPiCos r vs co = foldr (mkPiCo r) co vs
-- | Make a forall 'Coercion', where both types related by the coercion
-- are quantified over the same variable.
mkPiCo :: Role -> Var -> Coercion -> Coercion
-mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v Specified] co
+mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v coreTyLamForAllTyFlag] co
| isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
-- We didn't call mkForAllCo here because if v does not appear
-- in co, the argument coercion will be nominal. But here we
@@ -2410,7 +2405,8 @@ coercionLKind co
go (GRefl _ ty _) = ty
go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos)
go (AppCo co1 co2) = mkAppTy (go co1) (go co2)
- go (ForAllCo tv1 visL _ _ co1) = mkTyCoForAllTy tv1 visL (go co1)
+ go (ForAllCo { fco_tcv = tv1, fco_visL = visL, fco_body = co1 })
+ = mkTyCoForAllTy tv1 visL (go co1)
go (FunCo { fco_afl = af, fco_mult = mult, fco_arg = arg, fco_res = res})
{- See Note [FunCo] -} = FunTy { ft_af = af, ft_mult = go mult
, ft_arg = go arg, ft_res = go res }
@@ -2489,7 +2485,8 @@ coercionRKind co
go (AxiomRuleCo ax cos) = pSnd $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
- go co@(ForAllCo tv1 _visL visR k_co co1) -- works for both tyvar and covar
+ go co@(ForAllCo { fco_tcv = tv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co1 }) -- works for both tyvar and covar
| isGReflCo k_co = mkTyCoForAllTy tv1 visR (go co1)
-- kind_co always has kind @Type@, thus @isGReflCo@
| otherwise = go_forall empty_subst co
@@ -2513,7 +2510,8 @@ coercionRKind co
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
- go_forall subst (ForAllCo tv1 _visL visR k_co co)
+ go_forall subst (ForAllCo { fco_tcv = tv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co })
-- See Note [Nested ForAllCos]
| isTyVar tv1
= mkForAllTy (Bndr tv2 visR) (go_forall subst' co)
@@ -2525,7 +2523,8 @@ coercionRKind co
| otherwise = extendTvSubst (extendSubstInScope subst tv2) tv1 $
TyVarTy tv2 `mkCastTy` mkSymCo k_co
- go_forall subst (ForAllCo cv1 _visL visR k_co co)
+ go_forall subst (ForAllCo { fco_tcv = cv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co })
| isCoVar cv1
= mkTyCoForAllTy cv2 visR (go_forall subst' co)
where
@@ -2575,26 +2574,26 @@ change reduces /total/ compile time by a factor of more than ten.
coercionRole :: Coercion -> Role
coercionRole = go
where
- go (Refl _) = Nominal
- go (GRefl r _ _) = r
- go (TyConAppCo r _ _) = r
- go (AppCo co1 _) = go co1
- go (ForAllCo _tcv _visL _visR _kco co) = go co
- go (FunCo { fco_role = r }) = r
- go (CoVarCo cv) = coVarRole cv
- go (HoleCo h) = coVarRole (coHoleCoVar h)
- go (AxiomInstCo ax _ _) = coAxiomRole ax
- go (UnivCo _ r _ _) = r
- go (SymCo co) = go co
- go (TransCo co1 _co2) = go co1
- go (SelCo SelForAll _co) = Nominal
- go (SelCo (SelTyCon _ r) _co) = r
- go (SelCo (SelFun fs) co) = funRole (coercionRole co) fs
- go (LRCo {}) = Nominal
- go (InstCo co _) = go co
- go (KindCo {}) = Nominal
- go (SubCo _) = Representational
- go (AxiomRuleCo ax _) = coaxrRole ax
+ go (Refl _) = Nominal
+ go (GRefl r _ _) = r
+ go (TyConAppCo r _ _) = r
+ go (AppCo co1 _) = go co1
+ go (ForAllCo { fco_body = co }) = go co
+ go (FunCo { fco_role = r }) = r
+ go (CoVarCo cv) = coVarRole cv
+ go (HoleCo h) = coVarRole (coHoleCoVar h)
+ go (AxiomInstCo ax _ _) = coAxiomRole ax
+ go (UnivCo _ r _ _) = r
+ go (SymCo co) = go co
+ go (TransCo co1 _co2) = go co1
+ go (SelCo SelForAll _co) = Nominal
+ go (SelCo (SelTyCon _ r) _co) = r
+ go (SelCo (SelFun fs) co) = funRole (coercionRole co) fs
+ go (LRCo {}) = Nominal
+ go (InstCo co _) = go co
+ go (KindCo {}) = Nominal
+ go (SubCo _) = Representational
+ go (AxiomRuleCo ax _) = coaxrRole ax
{-
Note [Nested InstCos]
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -376,7 +376,7 @@ opt_co4 env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos))
opt_co4 env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2))
= opt_co4_wrap env sym rep r (getNthFun fs w co1 co2)
-opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo _ _ _ eta _))
+opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo { fco_kind = eta }))
-- works for both tyvar and covar
= opt_co4_wrap env sym rep Nominal eta
@@ -384,7 +384,7 @@ opt_co4 env sym rep r (SelCo n co)
| Just nth_co <- case (co', n) of
(TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
(FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
- (ForAllCo _ _ _ eta _, SelForAll) -> Just eta
+ (ForAllCo { fco_kind = eta }, SelForAll) -> Just eta
_ -> Nothing
= if rep && (r == Nominal)
-- keep propagating the SubCo
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -386,8 +386,9 @@ orphNamesOfCo (Refl ty) = orphNamesOfType ty
orphNamesOfCo (GRefl _ ty mco) = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (ForAllCo _tcv _vL _vR kind_co co) = orphNamesOfCo kind_co
- `unionNameSet` orphNamesOfCo co
+orphNamesOfCo (ForAllCo { fco_kind = kind_co, fco_body = co })
+ = orphNamesOfCo kind_co
+ `unionNameSet` orphNamesOfCo co
orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
= orphNamesOfCo co_mult
`unionNameSet` orphNamesOfCo co1
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1488,7 +1488,7 @@ normalise_type ty
go (ForAllTy (Bndr tcvar vis) ty)
= do { (lc', tv', k_redn) <- normalise_var_bndr tcvar
; redn <- withLC lc' $ normalise_type ty
- ; return $ mkForAllRedn vis vis tv' k_redn redn }
+ ; return $ mkForAllRedn vis tv' k_redn redn }
go (TyVarTy tv) = normalise_tyvar tv
go (CastTy ty co)
= do { redn <- go ty
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2230,7 +2230,8 @@ lintCoercion co@(AppCo co1 co2)
; return (AppCo co1' co2') }
----------
-lintCoercion co@(ForAllCo tcv visL visR kind_co body_co)
+lintCoercion co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = body_co })
| not (isTyCoVar tcv)
= failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co)
| otherwise
@@ -2261,7 +2262,7 @@ lintCoercion co@(ForAllCo tcv visL visR kind_co body_co)
lintL (visL `eqForAllVis` visR) $
text "Nominal ForAllCo has mismatched visibilities: " <+> ppr co
- ; return (ForAllCo tcv' visL visR kind_co' body_co') } }
+ ; return (co { fco_tcv = tcv', fco_kind = kind_co', fco_body = body_co' }) } }
lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
, fco_mult = cow, fco_arg = co1, fco_res = co2 })
=====================================
compiler/GHC/Core/Reduction.hs
=====================================
@@ -370,15 +370,14 @@ mkFunRedn r af
--
-- Combines 'mkForAllCo' and 'mkForAllTy'.
mkForAllRedn :: ForAllTyFlag
- -> ForAllTyFlag
-> TyVar
-> ReductionN -- ^ kind reduction
-> Reduction -- ^ body reduction
-> Reduction
-mkForAllRedn vis1 vis2 tv1 (Reduction h ki') (Reduction co ty)
+mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
= mkReduction
- (mkForAllCo tv1 vis1 vis2 h co)
- (mkForAllTy (Bndr tv2 vis2) ty)
+ (mkForAllCo tv1 vis vis h co)
+ (mkForAllTy (Bndr tv2 vis) ty)
where
tv2 = setTyVarKind tv1 ki'
{-# INLINE mkForAllRedn #-}
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -631,7 +631,7 @@ tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
= (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
-tyCoFVsOfCo (ForAllCo tv _visL _visR kind_co co) fv_cand in_scope acc
+tyCoFVsOfCo (ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = co }) fv_cand in_scope acc
= (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_scope acc
= (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc
@@ -686,7 +686,7 @@ almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
almost_devoid_co_var_of_co (AppCo co arg) cv
= almost_devoid_co_var_of_co co cv
&& almost_devoid_co_var_of_co arg cv
-almost_devoid_co_var_of_co (ForAllCo v _visL _visR kind_co co) cv
+almost_devoid_co_var_of_co (ForAllCo { fco_tcv = v, fco_kind = kind_co, fco_body = co }) cv
= almost_devoid_co_var_of_co kind_co cv
&& (v == cv || almost_devoid_co_var_of_co co cv)
almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) cv
@@ -1109,7 +1109,8 @@ tyConsOfType ty
go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
- go_co (ForAllCo _ _ _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
+ go_co (ForAllCo { fco_kind = kind_co, fco_body = co })
+ = go_co kind_co `unionUniqSets` go_co co
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r
go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
@@ -1293,14 +1294,14 @@ occCheckExpand vs_to_avoid ty
go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
; arg' <- go_co cxt arg
; return (AppCo co' arg') }
- go_co cxt@(as, env) (ForAllCo tv visL visR kind_co body_co)
+ go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = body_co })
= do { kind_co' <- go_co cxt kind_co
; let tv' = setVarType tv $
coercionLKind kind_co'
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
; body' <- go_co (as', env') body_co
- ; return (ForAllCo tv' visL visR kind_co' body') }
+ ; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }
go_co cxt co@(FunCo { fco_mult = w, fco_arg = co1 ,fco_res = co2 })
= do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -488,9 +488,9 @@ This is done in mkCastTy.
In sum, in order to uphold (EQ), we need the following invariants:
- (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
- cast is one that relates either a FunTy to a FunTy or a
- ForAllTy to a ForAllTy.
+ (EQ1) No decomposable CastTy to the left of an AppTy,
+ where a "decomposable cast" is one that relates
+ either a FunTy to a FunTy, or a ForAllTy to a ForAllTy.
(EQ2) No reflexive casts in CastTy.
(EQ3) No nested CastTys.
(EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
@@ -851,11 +851,11 @@ data Coercion
-- See Note [Forall coercions]
| ForAllCo
- TyCoVar
- !ForAllTyFlag -- visibility of coercionLKind
- !ForAllTyFlag -- visibility of coercionRKind
- KindCoercion
- Coercion
+ { fco_tcv :: TyCoVar
+ , fco_visL :: !ForAllTyFlag -- visibility of coercionLKind
+ , fco_visR :: !ForAllTyFlag -- visibility of coercionRKind
+ , fco_kind :: KindCoercion
+ , fco_body :: Coercion }
-- ForAllCo :: _ -> N -> e -> e
| FunCo -- FunCo :: "e" -> N/P -> e -> e -> e
@@ -1167,41 +1167,53 @@ of the chosen branch.
Note [Forall coercions]
~~~~~~~~~~~~~~~~~~~~~~~
Constructing coercions between forall-types can be a bit tricky,
-because the kinds of the bound tyvars can be different.
+because the kinds of the bound otyvars can be different.
The typing rule is:
-
- kind_co : k1 ~ k2
- tv1:k1 |- co : t1 ~ t2
- -------------------------------------------------------------------
- ForAllCo tv1 vis1 vis2 kind_co co
- : all tv1:k1 <vis1>. t1 ~
- all tv1:k2 <vis2>. (t2[tv1 |-> tv1 |> sym kind_co])
-
-First, the TyCoVar stored in a ForAllCo is really an optimisation: this field
-should be a Name, as its kind is redundant. Thinking of the field as a Name
-is helpful in understanding what a ForAllCo means.
-The kind of TyCoVar always matches the left-hand kind of the coercion.
-
-The idea is that kind_co gives the two kinds of the tyvar. See how, in the
-conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
-
-Of course, a type variable can't have different kinds at the same time. So,
-we arbitrarily prefer the first kind when using tv1 in the inner coercion
-co, which shows that t1 equals t2.
-
-The last wrinkle is that we need to fix the kinds in the conclusion. In
-t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
-the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
-(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
-mentions the same name with different kinds, but it *is* well-kinded, noting
-that `(tv1:k2) |> sym kind_co` has kind k1.
-
-This all really would work storing just a Name in the ForAllCo. But we can't
-add Names to, e.g., VarSets, and there generally is just an impedance mismatch
-in a bunch of places. So we use tv1. When we need tv2, we can use
-setTyVarKind.
+ kind_co : k1 ~N k2
+ tv1:k1 |- co : t1 ~r t2
+ if r=N, then vis1=vis2
+ ------------------------------------
+ ForAllCo (tv1:k1) vis1 vis2 kind_co co
+ : forall (tv1:k1) <vis1>. t1
+ ~r
+ forall (tv1:k2) <vis2>. (t2[tv1 |-> (tv1:k2) |> sym kind_co])
+
+Several things to note here
+
+(FC1) First, the TyCoVar stored in a ForAllCo is really an optimisation: this
+ field should be a Name, as its kind is redundant. Thinking of the field as a
+ Name is helpful in understanding what a ForAllCo means. The kind of TyCoVar
+ always matches the left-hand kind of the coercion.
+
+ * The idea is that kind_co gives the two kinds of the tyvar. See how, in the
+ conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
+
+ * Of course, a type variable can't have different kinds at the same time.
+ So, in `co` itself we use (tv1 : k1); hence the premise
+ tv1:k1 |- co : t1 ~r t2
+
+ * The last wrinkle is that we need to fix the kinds in the conclusion. In
+ t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
+ the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
+ (tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
+ mentions the same name with different kinds, but it *is* well-kinded, noting
+ that `(tv1:k2) |> sym kind_co` has kind k1.
+
+ We could instead store just a Name in the ForAllCo. But we can't add Names
+ to, e.g., VarSets, and there generally is just an impedance mismatch in a
+ bunch of places. So we use tv1. When we need tv2, we can use setTyVarKind.
+
+(FC2) Note that the kind coercion must be Nominal; and that the role `r` of
+ the final coercion is the same as that of the body coercion.
+
+(FC3) A ForAllCo allows to cast between visibilities. For example:
+ ForAllCo a Required Specified (SubCo (Refl ty))
+ : (forall a -> ty) ~R (forall a. ty)
+ But only at Representational role. The two types are Representationally
+ equal but not Nominally equal. Hence the premise
+ if r=N, then vis1=vis2
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1821,7 +1833,8 @@ coercionSize (GRefl _ ty MRefl) = typeSize ty
coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
-coercionSize (ForAllCo _ _ _ h co) = 1 + coercionSize co + coercionSize h
+coercionSize (ForAllCo { fco_kind = h, fco_body = co })
+ = 1 + coercionSize co + coercionSize h
coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
+ coercionSize w
coercionSize (CoVarCo _) = 1
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -535,7 +535,8 @@ Note [Sym and ForAllCo]
In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
how do we push sym into a ForAllCo? It's a little ugly.
-Ignoring visibility, here is the typing rule:
+Ignoring visibility, here is the typing rule
+(see Note [Forall coercions] in GHC.Core.TyCo.Rep).
h : k1 ~# k2
(tv : k1) |- g : ty1 ~# ty2
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -548,7 +548,8 @@ expandTypeSynonyms ty
= mkTyConAppCo r tc (map (go_co subst) args)
go_co subst (AppCo co arg)
= mkAppCo (go_co subst co) (go_co subst arg)
- go_co subst (ForAllCo tv visL visR kind_co co)
+ go_co subst (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co })
= let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
mkForAllCo tv' visL visR kind_co' (go_co subst' co)
go_co subst (FunCo r afl afr w co1 co2)
@@ -990,7 +991,8 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
| otherwise
= mkTyConAppCo r tc <$> go_cos env cos
- go_co !env (ForAllCo tv visL visR kind_co co)
+ go_co !env (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co })
= do { kind_co' <- go_co env kind_co
; tycobinder env tv visL $ \env' tv' -> do
; co' <- go_co env' co
@@ -1050,8 +1052,6 @@ invariant: use it.
Note [Decomposing fat arrow c=>t]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This note needs updating since the Type/Constraint separation in Core...
-
Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
a partial application like ((=>) (Eq a)) which doesn't make sense in
source Haskell. In contrast, we *can* unify (a b) with (t1 -> t2).
@@ -1064,14 +1064,13 @@ The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
but suppose we want that. But then in the call to 'i', we end
up decomposing (Eq Int => Int), and we definitely don't want that.
-This really only applies to the type checker; in Core, '=>' and '->'
-are the same, as are 'Constraint' and '*'. But for now I've put
-the test in splitAppTyNoView_maybe, which applies throughout, because
-the other calls to splitAppTy are in GHC.Core.Unify, which is also used by
-the type checker (e.g. when matching type-function equations).
-
We are willing to split (t1 -=> t2) because the argument is still of
kind Type, not Constraint. So the criterion is isVisibleFunArg.
+
+In Core there is no real reason to avoid such decomposition. But for now I've
+put the test in splitAppTyNoView_maybe, which applies throughout, because the
+other calls to splitAppTy are in GHC.Core.Unify, which is also used by the
+type checker (e.g. when matching type-function equations).
-}
-- | Applies a type to another, as in e.g. @k a@
@@ -1938,22 +1937,20 @@ dropForAlls ty = go ty
go ty | Just ty' <- coreView ty = go ty'
go res = res
--- | Attempts to take a forall type apart, but only if it's a proper forall,
--- with a named binder
+-- | Attempts to take a ForAllTy apart, returning the full ForAllTyBinder
splitForAllForAllTyBinder_maybe :: Type -> Maybe (ForAllTyBinder, Type)
splitForAllForAllTyBinder_maybe ty
| ForAllTy bndr inner_ty <- coreFullView ty = Just (bndr, inner_ty)
| otherwise = Nothing
--- | Attempts to take a forall type apart, but only if it's a proper forall,
--- with a named binder
+-- | Attempts to take a ForAllTy apart, returning the Var
splitForAllTyCoVar_maybe :: Type -> Maybe (TyCoVar, Type)
splitForAllTyCoVar_maybe ty
| ForAllTy (Bndr tv _) inner_ty <- coreFullView ty = Just (tv, inner_ty)
| otherwise = Nothing
--- | Like 'splitForAllTyCoVar_maybe', but only returns Just if it is a tyvar binder.
+-- | Attempts to take a ForAllTy apart, but only if the binder is a TyVar
splitForAllTyVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyVar_maybe ty
| ForAllTy (Bndr tv _) inner_ty <- coreFullView ty
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1780,7 +1780,9 @@ pushRefl co =
Just (TyConApp tc tys, r)
-> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRoleListX r tc) tys))
Just (ForAllTy (Bndr tv vis) ty, r)
- -> Just (ForAllCo tv vis vis (mkNomReflCo (varType tv)) (mkReflCo r ty))
+ -> Just (ForAllCo { fco_tcv = tv, fco_visL = vis, fco_visR = vis
+ , fco_kind = mkNomReflCo (varType tv)
+ , fco_body = mkReflCo r ty })
-- NB: NoRefl variant. Otherwise, we get a loop!
_ -> Nothing
=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -21,7 +21,8 @@ module GHC.Core.Utils (
scaleAltsBy,
-- * Properties of expressions
- exprType, coreAltType, coreAltsType, mkLamType, mkLamTypes,
+ exprType, coreAltType, coreAltsType,
+ mkLamType, mkLamTypes,
mkFunctionType,
exprIsDupable, exprIsTrivial, getIdFromTrivialExpr,
getIdFromTrivialExpr_maybe,
@@ -166,7 +167,7 @@ mkLamTypes :: [Var] -> Type -> Type
mkLamType v body_ty
| isTyVar v
- = mkForAllTy (Bndr v Specified) body_ty
+ = mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
| isCoVar v
, v `elemVarSet` tyCoVarsOfType body_ty
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )
+import qualified GHC.Tc.Utils.Monad as TcM
import GHC.Core.Type
import GHC.Core.Predicate
@@ -477,27 +478,19 @@ can_eq_nc_forall :: CtEvidence -> EqRel
-- so we must proceed one binder at a time (#13879)
can_eq_nc_forall ev eq_rel s1 s2
- | CtWanted { ctev_loc = loc, ctev_dest = orig_dest, ctev_rewriters = rewriters } <- ev
- = do { let free_tvs = tyCoVarsOfTypes [s1,s2]
- (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
- (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
+ | CtWanted { ctev_dest = orig_dest } <- ev
+ = do { let free_tvs = tyCoVarsOfTypes [s1,s2]
+ (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2
+
hard_fail why = do { traceTcS ("Forall failure: " ++ why) $
- vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
- , ppr (binderFlags bndrs1)
- , ppr (binderFlags bndrs2) ]
- ; canEqHardFailure ev s1 s2 }
+ vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
+ , ppr (binderFlags bndrs1)
+ , ppr (binderFlags bndrs2) ]
+ ; canEqHardFailure ev s1 s2 }
; if | eq_rel == NomEq
- , not (and $ zipWith (eqForAllVis `on` binderFlag) bndrs1 bndrs2)
+ , not (all2 (eqForAllVis `on` binderFlag) bndrs1 bndrs2)
-> hard_fail "visibility mismatch"
- | not (equalLength bndrs1 bndrs2)
- -- I believe this relies on the (generally wrong) assumption
- -- that type families never return a forall-type.
- -- But newtypes can certainly wrap forall-types!
- -- So we definitely shouldn't just reject for ReprEq.
- -- See also #22537.
- -> hard_fail "unequal foralls-nesting-depth"
-
| otherwise -> do {
; traceTcS "Creating implication for polytype equality" $ ppr ev
; let empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs
@@ -508,33 +501,36 @@ can_eq_nc_forall ev eq_rel s1 s2
; let phi1' = substTy subst1 phi1
-- Unify the kinds, extend the substitution
- go :: [TcTyVar] -> Subst -> [TyVarBinder] -> [TyVarBinder]
- -> TcS (TcCoercion, Cts)
- go (skol_tv:skol_tvs) subst (bndr1:bndrs1) (bndr2:bndrs2)
- = do { let tv2 = binderVar bndr2
+ go :: UnifyEnv -> [TcTyVar] -> Subst
+ -> [TyVarBinder] -> [TyVarBinder] -> TcM.TcM TcCoercion
+ go uenv (skol_tv:skol_tvs) subst (bndr1:bndrs1) (bndr2:bndrs2)
+ = do { let tv2 = binderVar bndr2
vis1 = binderFlag bndr1
vis2 = binderFlag bndr2
- ; (kind_co, wanteds1) <- unify loc rewriters Nominal (tyVarKind skol_tv)
- (substTy subst (tyVarKind tv2))
+
+ ; kind_co <- uType (uenv `setUEnvRole` Nominal)
+ (tyVarKind skol_tv)
+ (substTy subst (tyVarKind tv2))
+
; let subst' = extendTvSubstAndInScope subst tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
-- skol_tv is already in the in-scope set, but the
-- free vars of kind_co are not; hence "...AndInScope"
- ; (co, wanteds2) <- go skol_tvs subst' bndrs1 bndrs2
- ; return ( mkForAllCo skol_tv vis1 vis2 kind_co co
- , wanteds1 `unionBags` wanteds2 ) }
+ ; co <- go uenv skol_tvs subst' bndrs1 bndrs2
+ ; return (mkForAllCo skol_tv vis1 vis2 kind_co co)}
-- Done: unify phi1 ~ phi2
- go [] subst bndrs1 bndrs2
+ go uenv [] subst bndrs1 bndrs2
= assert (null bndrs1 && null bndrs2) $
- unify loc rewriters (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
+ uType uenv phi1' (substTyUnchecked subst phi2)
- go _ _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
+ go _ _ _ _ _ = panic "can_eq_nc_forall" -- case (s:ss) []
empty_subst2 = mkEmptySubst (getSubstInScope subst1)
- ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
- go skol_tvs empty_subst2 bndrs1 bndrs2
+ ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
+ unifyForAllBody ev (eqRelRole eq_rel) $ \uenv ->
+ go uenv skol_tvs empty_subst2 bndrs1 bndrs2
; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds
; setWantedEq orig_dest all_co
@@ -546,16 +542,24 @@ can_eq_nc_forall ev eq_rel s1 s2
; stopWith ev "Discard given polytype equality" }
where
- unify :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
- -- This version returns the wanted constraint rather
- -- than putting it in the work list
- unify loc rewriters role ty1 ty2
- | ty1 `tcEqType` ty2
- = return (mkReflCo role ty1, emptyBag)
- | otherwise
- = do { (wanted, co) <- newWantedEq loc rewriters role ty1 ty2
- ; return (co, unitBag (mkNonCanonical wanted)) }
-
+ split_foralls :: TcType -> TcType
+ -> ([ForAllTyBinder], TcType, [ForAllTyBinder], TcType)
+ -- Split matching foralls; stop when the foralls don't match
+ -- See #22537. ToDo: amplify this note
+ split_foralls s1 s2
+ | n_bndrs1 == n_bndrs2 = ( bndrs1, phi1
+ , bndrs2, phi2)
+ | n_bndrs1 < n_bndrs2 = ( bndrs1, phi1
+ , take n_bndrs1 bndrs2
+ , mkForAllTys (drop n_bndrs1 bndrs2) phi2 )
+ | otherwise = ( take n_bndrs2 bndrs1
+ , mkForAllTys (drop n_bndrs2 bndrs1) phi1
+ , bndrs2, phi2 )
+ where
+ (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
+ (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
+ n_bndrs1 = length bndrs1
+ n_bndrs2 = length bndrs2
{- Note [Unwrap newtypes first]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -97,7 +97,7 @@ module GHC.Tc.Solver.Monad (
instDFunType,
-- Unification
- wrapUnifierTcS, unifyFunDeps, uPairsTcM,
+ wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
-- MetaTyVars
newFlexiTcSTy, instFlexiX,
@@ -1997,6 +1997,16 @@ unifyFunDeps ev role do_unifications
where
fvs = tyCoVarsOfType (ctEvPred ev)
+unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a)
+ -> TcS (a, Cts)
+unifyForAllBody ev role unify_body
+ = do { (res, cts, unified, _rewriters) <- wrapUnifierX ev role unify_body
+
+ -- Kick out any inert constraint that we have unified
+ ; _ <- kickOutAfterUnification unified
+
+ ; return (res, cts) }
+
wrapUnifierTcS :: CtEvidence -> Role
-> (UnifyEnv -> TcM a) -- Some calls to uType
-> TcS (a, Bag Ct, [TcTyVar])
@@ -2010,21 +2020,7 @@ wrapUnifierTcS :: CtEvidence -> Role
-- unified the process; the (Bag Ct) are the deferred constraints.
wrapUnifierTcS ev role do_unifications
- = do { (cos, unified, rewriters, cts) <- wrapTcS $
- do { defer_ref <- TcM.newTcRef emptyBag
- ; unified_ref <- TcM.newTcRef []
- ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
- ; let env = UE { u_role = role
- , u_rewriters = rewriters
- , u_loc = ctEvLoc ev
- , u_defer = defer_ref
- , u_unified = Just unified_ref}
-
- ; cos <- do_unifications env
-
- ; cts <- TcM.readTcRef defer_ref
- ; unified <- TcM.readTcRef unified_ref
- ; return (cos, unified, rewriters, cts) }
+ = do { (res, cts, unified, rewriters) <- wrapUnifierX ev role do_unifications
-- Emit the deferred constraints
-- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
@@ -2034,7 +2030,27 @@ wrapUnifierTcS ev role do_unifications
-- And kick out any inert constraint that we have unified
; _ <- kickOutAfterUnification unified
- ; return (cos, cts, unified) }
+ ; return (res, cts, unified) }
+
+wrapUnifierX :: CtEvidence -> Role
+ -> (UnifyEnv -> TcM a) -- Some calls to uType
+ -> TcS (a, Bag Ct, [TcTyVar], RewriterSet)
+wrapUnifierX ev role do_unifications
+ = wrapTcS $
+ do { defer_ref <- TcM.newTcRef emptyBag
+ ; unified_ref <- TcM.newTcRef []
+ ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
+ ; let env = UE { u_role = role
+ , u_rewriters = rewriters
+ , u_loc = ctEvLoc ev
+ , u_defer = defer_ref
+ , u_unified = Just unified_ref}
+
+ ; res <- do_unifications env
+
+ ; cts <- TcM.readTcRef defer_ref
+ ; unified <- TcM.readTcRef unified_ref
+ ; return (res, cts, unified, rewriters) }
{-
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -137,7 +137,8 @@ synonymTyConsOfType ty
go_co (GRefl _ ty mco) = go ty `plusNameEnv` go_mco mco
go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs
go_co (AppCo co co') = go_co co `plusNameEnv` go_co co'
- go_co (ForAllCo _ _ _ co co') = go_co co `plusNameEnv` go_co co'
+ go_co (ForAllCo { fco_kind = kind_co, fco_body = body_co })
+ = go_co kind_co `plusNameEnv` go_co body_co
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `plusNameEnv` go_co a `plusNameEnv` go_co r
go_co (CoVarCo _) = emptyNameEnv
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1447,7 +1447,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
go_co dv (CoVarCo cv) = go_cv dv cv
- go_co dv (ForAllCo tcv _visL _visR kind_co co)
+ go_co dv (ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = co })
= do { dv1 <- go_co dv kind_co
; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co }
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -69,6 +69,7 @@ module GHC.Types.Var (
ForAllTyFlag(Invisible,Required,Specified,Inferred),
Specificity(..),
isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag,
+ coreTyLamForAllTyFlag,
-- * FunTyFlag
FunTyFlag(..), isVisibleFunArg, isInvisibleFunArg, isFUNArg,
@@ -488,6 +489,12 @@ isInferredForAllTyFlag :: ForAllTyFlag -> Bool
isInferredForAllTyFlag (Invisible InferredSpec) = True
isInferredForAllTyFlag _ = False
+coreTyLamForAllTyFlag :: ForAllTyFlag
+-- ^ The ForAllTyFlag on a (Lam a e) term, where `a` is a type variable.
+-- If you want other ForAllTyFlag, use a cast.
+-- See Note [Forall coercions] in GHC.Core.TyCo.Rep
+coreTyLamForAllTyFlag = Specified
+
instance Outputable ForAllTyFlag where
ppr Required = text "[req]"
ppr Specified = text "[spec]"
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/148e83dff016be02f155ec116b52acb1ce8bb9f9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/148e83dff016be02f155ec116b52acb1ce8bb9f9
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/20230614/77569878/attachment-0001.html>
More information about the ghc-commits
mailing list