diff options
Diffstat (limited to 'compiler/GHC/Core/TyCo')
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 80 |
1 files changed, 71 insertions, 9 deletions
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 513001e42d..f1dcd8bfd6 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -166,10 +166,10 @@ data Type | CastTy Type KindCoercion -- ^ A kind cast. The coercion is always nominal. - -- INVARIANT: The cast is never reflexive - -- INVARIANT: The Type is not a CastTy (use TransCo instead) - -- INVARIANT: The Type is not a ForAllTy over a type variable - -- See Note [Respecting definitional equality] \(EQ2), (EQ3), (EQ4) + -- INVARIANT: The cast is never reflexive \(EQ2) + -- INVARIANT: The Type is not a CastTy (use TransCo instead) \(EQ3) + -- INVARIANT: The Type is not a ForAllTy over a tyvar \(EQ4) + -- See Note [Respecting definitional equality] | CoercionTy Coercion -- ^ Injection of a Coercion into a type @@ -302,6 +302,31 @@ When treated as a user type, In a FunTy { ft_af = InvisArg }, the argument type is always a Predicate type. +Note [Weird typing rule for ForAllTy] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Here are the typing rules for ForAllTy: + +tyvar : Type +inner : TYPE r +tyvar does not occur in r +------------------------------------ +ForAllTy (Bndr tyvar vis) inner : TYPE r + +inner : TYPE r +------------------------------------ +ForAllTy (Bndr covar vis) inner : Type + +Note that the kind of the result depends on whether the binder is a +tyvar or a covar. The kind of a forall-over-tyvar is the same as +the kind of the inner type. This is because quantification over types +is erased before runtime. By contrast, the kind of a forall-over-covar +is always Type, because a forall-over-covar is compiled into a function +taking a 0-bit-wide erased coercion argument. + +Because the tyvar form above includes r in its result, we must +be careful not to let any variables escape -- thus the last premise +of the rule above. + Note [Constraints in kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Do we allow a type constructor to have a kind like @@ -452,7 +477,7 @@ casting. The same is true of expressions of type σ. So in some sense, τ and σ are interchangeable. But let's be more precise. If we examine the typing rules of FC (say, those in -https://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf) +https://richarde.dev/papers/2015/equalities/equalities.pdf) there are several places where the same metavariable is used in two different premises to a rule. (For example, see Ty_App.) There is an implicit equality check here. What definition of equality should we use? By convention, we use @@ -470,7 +495,7 @@ equality check, can use any homogeneous relation that is smaller than ~, as those rules must also be admissible. A more drawn out argument around all of this is presented in Section 7.2 of -Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf). +Richard E's thesis (http://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf). What would go wrong if we insisted on the casts matching? See the beginning of Section 8 in the unpublished paper above. Theoretically, nothing at all goes @@ -482,8 +507,8 @@ then we couldn't discard -- the output of kind-checking would be enormous, and we would need enormous casts with lots of CoherenceCo's to straighten them out. -Would anything go wrong if eqType respected type families? No, not at all. But -that makes eqType rather hard to implement. +Would anything go wrong if eqType looked through type families? No, not at +all. But that makes eqType rather hard to implement. Thus, the guideline for eqType is that it should be the largest easy-to-implement relation that is still smaller than ~ and homogeneous. The @@ -497,6 +522,23 @@ Another helpful principle with eqType is this: This principle also tells us that eqType must relate only types with the same kinds. +Interestingly, it must be the case that the free variables of t1 and t2 +might be different, even if t1 `eqType` t2. A simple example of this is +if we have both cv1 :: k1 ~ k2 and cv2 :: k1 ~ k2 in the environment. +Then t1 = t |> cv1 and t2 = t |> cv2 are eqType; yet cv1 is in the free +vars of t1 and cv2 is in the free vars of t2. Unless we choose to implement +eqType to be just α-equivalence, this wrinkle around free variables +remains. + +Yet not all is lost: we can say that any two equal types share the same +*relevant* free variables. Here, a relevant variable is a shallow +free variable (see Note [Shallow and deep free variables] in GHC.Core.TyCo.FVs) +that does not appear within a coercion. Note that type variables can +appear within coercions (in, say, a Refl node), but that coercion variables +cannot appear outside a coercion. We do not (yet) have a function to +extract relevant free variables, but it would not be hard to write if +the need arises. + Besides eqType, another equality relation that upholds the (EQ) property above is /typechecker equality/, which is implemented as GHC.Tc.Utils.TcType.tcEqType. See @@ -525,7 +567,7 @@ to differ, leading to a contradiction. Thus, co is reflexive. Accordingly, by eliminating reflexive casts, splitTyConApp need not worry about outermost casts to uphold (EQ). Eliminating reflexive casts is done -in mkCastTy. +in mkCastTy. This is (EQ1) below. Unforunately, that's not the end of the story. Consider comparing (T a b c) =? (T a b |> (co -> <Type>)) (c |> co) @@ -548,6 +590,7 @@ our (EQ) property. In order to detect reflexive casts reliably, we must make sure not to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)). +This is (EQ2) below. One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy]. The kind of the body is the same as the kind of the ForAllTy. Accordingly, @@ -570,6 +613,25 @@ In sum, in order to uphold (EQ), we need the following invariants: These invariants are all documented above, in the declaration for Type. +Note [Equality on FunTys] +~~~~~~~~~~~~~~~~~~~~~~~~~ +A (FunTy vis mult arg res) is just an abbreviation for a + TyConApp funTyCon [mult, arg_rep, res_rep, arg, res] +where + arg :: TYPE arg_rep + res :: TYPE res_rep +Note that the vis field of a FunTy appears nowhere in the +equivalent TyConApp. In Core, this is OK, because we no longer +care about the visibility of the argument in a FunTy +(the vis distinguishes between arg -> res and arg => res). +In the type-checker, we are careful not to decompose FunTys +with an invisible argument. See also Note [Decomposing fat arrow c=>t] +in GHC.Core.Type. + +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 [Unused coercion variable in ForAllTy] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have |