diff options
Diffstat (limited to 'compiler/GHC/Core/TyCo/Rep.hs')
| -rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 42 |
1 files changed, 38 insertions, 4 deletions
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index fae7c7de19..a08da28421 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -65,7 +65,7 @@ module GHC.Core.TyCo.Rep ( pickLR, -- ** Analyzing types - TyCoFolder(..), foldTyCo, + TyCoFolder(..), foldTyCo, noView, -- * Sizes typeSize, coercionSize, provSize, @@ -150,6 +150,7 @@ data Type | ForAllTy {-# UNPACK #-} !TyCoVarBinder Type -- ^ A Π type. + -- Note [When we quantify over a coercion variable] -- INVARIANT: If the binder is a coercion variable, it must -- be mentioned in the Type. See -- Note [Unused coercion variable in ForAllTy] @@ -624,6 +625,35 @@ In order to compare FunTys while respecting how they could expand into TyConApps, we must check the kinds of the arg and the res. +Note [When we quantify over a coercion variable] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The TyCoVarBinder in a ForAllTy can be (most often) a TyVar or (rarely) +a CoVar. We support quantifying over a CoVar here in order to support +a homogeneous (~#) relation (someday -- not yet implemented). Here is +the example: + + type (:~~:) :: forall k1 k2. k1 -> k2 -> Type + data a :~~: b where + HRefl :: a :~~: a + +Assuming homogeneous equality (that is, with + (~#) :: forall k. k -> k -> TYPE (TupleRep '[]) +) after rejigging to make equalities explicit, we get a constructor that +looks like + + HRefl :: forall k1 k2 (a :: k1) (b :: k2). + forall (cv :: k1 ~# k2). (a |> cv) ~# b + => (:~~:) k1 k2 a b + +Note that we must cast `a` by a cv bound in the same type in order to +make this work out. + +See also https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell/phase2 +which gives a general road map that covers this space. + +Having this feature in Core does *not* mean we have it in source Haskell. +See #15710 about that. + Note [Unused coercion variable in ForAllTy] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -1834,7 +1864,7 @@ We were also worried about `extendVarSet` tv Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf. -But, amazingly, we get good code here too. GHC is careful not to makr +But, amazingly, we get good code here too. GHC is careful not to mark TyCoFolder data constructor for deep_tcf as a loop breaker, so the record selections still cancel. And eta expansion still happens too. -} @@ -1843,8 +1873,8 @@ data TyCoFolder env a = TyCoFolder { tcf_view :: Type -> Maybe Type -- Optional "view" function -- E.g. expand synonyms - , tcf_tyvar :: env -> TyVar -> a - , tcf_covar :: env -> CoVar -> a + , tcf_tyvar :: env -> TyVar -> a -- Does not automatically recur + , tcf_covar :: env -> CoVar -> a -- into kinds of variables , tcf_hole :: env -> CoercionHole -> a -- ^ What to do with coercion holes. -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep". @@ -1916,6 +1946,10 @@ foldTyCo (TyCoFolder { tcf_view = view go_prov _ (PluginProv _) = mempty go_prov _ (CorePrepProv _) = mempty +-- | A view function that looks through nothing. +noView :: Type -> Maybe Type +noView _ = Nothing + {- ********************************************************************* * * typeSize, coercionSize |