Compare FunTys as if they were TyConApps.

See Note [Equality on FunTys] in TyCoRep.

Close #17675.
Close #17655, about documentation improvements included in
this patch.
Close #19677, about a further mistake around FunTy.

test cases: typecheck/should_compile/T19677

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