Compare FunTys as if they were TyConApps.wip/T17674

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

6 files changed, 125 insertions, 34 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index ac09b0a7c4..a7b4a33584 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -477,7 +477,7 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
        -> (TCvSubst,Kind)  -- Rhs kind of coercion
        -> [Type]           -- Arguments to that function
        -> ([CoercionN], Coercion)
-    -- Invariant:  co :: subst1(k2) ~ subst2(k2)
+    -- Invariant:  co :: subst1(k1) ~ subst2(k2)
 
     go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
       | Just (a, t1) <- splitForAllTyCoVar_maybe k1
diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index 32b3fe054b..15c624d8b3 100644
--- a/compiler/GHC/Core/Map/Type.hs
+++ b/compiler/GHC/Core/Map/Type.hs
@@ -48,13 +48,13 @@ import GHC.Types.Var.Env
 import GHC.Types.Unique.FM
 import GHC.Utils.Outputable
 
-import GHC.Data.Maybe
 import GHC.Utils.Panic
 
 import qualified Data.Map    as Map
 import qualified Data.IntMap as IntMap
 
 import Control.Monad ( (>=>) )
+import GHC.Data.Maybe
 
 -- NB: Be careful about RULES and type families (#5821).  So we should make sure
 -- to specify @Key TypeMapX@ (and not @DeBruijn Type@, the reduced form)
@@ -136,16 +136,17 @@ xtC (D env co) f (CoercionMapX m)
 type TypeMapG = GenMap TypeMapX
 
 -- | @TypeMapX a@ is the base map from @DeBruijn Type@ to @a@, but without the
--- 'GenMap' optimization.
+-- 'GenMap' optimization. See Note [Computing equality on types] in GHC.Core.Type.
 data TypeMapX a
   = TM { tm_var    :: VarMap a
-       , tm_app    :: TypeMapG (TypeMapG a)
+       , tm_app    :: TypeMapG (TypeMapG a)  -- Note [Equality on AppTys] in GHC.Core.Type
        , tm_tycon  :: DNameEnv a
 
          -- only InvisArg arrows here
        , tm_funty  :: TypeMapG (TypeMapG (TypeMapG a))
                        -- keyed on the argument, result rep, and result
                        -- constraints are never linear-restricted and are always lifted
+                       -- See also Note [Equality on FunTys] in GHC.Core.TyCo.Rep
 
        , tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr
        , tm_tylit  :: TyLitMap a
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
index 254b4420e1..fbae18f797 100644
--- a/compiler/GHC/Core/Reduction.hs
+++ b/compiler/GHC/Core/Reduction.hs
@@ -807,7 +807,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
        orig_ki_binders orig_inner_ki
        orig_roles orig_simplified_args
   where
-    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
+    orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs
 
     go :: LiftingContext  -- mapping from tyvars to rewriting coercions
        -> [TyCoBinder]    -- Unsubsted binders of function's kind
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
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 6b88262ff5..0d82c010c0 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -43,6 +43,7 @@ module GHC.Core.Type (
         tcSplitTyConApp_maybe,
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
+        tcRepSplitTyConApp_maybe,
 
         mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
         mkSpecForAllTy, mkSpecForAllTys,
@@ -1058,13 +1059,16 @@ tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
 -- any coreView stuff is already done. Refuses to look through (c => t)
 tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = ty1, ft_res = ty2 })
-  | InvisArg <- af
-  = Nothing  -- See Note [Decomposing fat arrow c=>t]
-  | otherwise
+  | VisArg <- af   -- See Note [Decomposing fat arrow c=>t]
+
+  -- See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType,
+  -- Wrinkle around FunTy
+  , Just rep1 <- getRuntimeRep_maybe ty1
+  , Just rep2 <- getRuntimeRep_maybe ty2
   = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2)
-  where
-    rep1 = getRuntimeRep ty1
-    rep2 = getRuntimeRep ty2
+
+  | otherwise
+  = Nothing
 
 tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
 tcRepSplitAppTy_maybe (TyConApp tc tys)
@@ -1472,30 +1476,39 @@ splitTyConApp_maybe = repSplitTyConApp_maybe . coreFullView
 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 -- Defined here to avoid module loops between Unify and TcType.
 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
-tcSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
-tcSplitTyConApp_maybe (FunTy VisArg w arg res)
-  | Just arg_rep <- getRuntimeRep_maybe arg
-  , Just res_rep <- getRuntimeRep_maybe res
-  = Just (funTyCon, [w, arg_rep, res_rep, arg, res])
-tcSplitTyConApp_maybe _ = Nothing
+                         | otherwise             = tcRepSplitTyConApp_maybe ty
 
 -------------------
 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 -- ^ Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
 -- assumes the synonyms have already been dealt with.
+repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
+repSplitTyConApp_maybe (FunTy _ w arg res)
+  -- NB: we're in Core, so no check for VisArg
+  = Just (funTyCon, [w, arg_rep, res_rep, arg, res])
+  where
+    arg_rep = getRuntimeRep arg
+    res_rep = getRuntimeRep res
+repSplitTyConApp_maybe _ = Nothing
+
+tcRepSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
+-- ^ Like 'tcSplitTyConApp_maybe', but doesn't look through synonyms. This
+-- assumes the synonyms have already been dealt with.
 --
 -- Moreover, for a FunTy, it only succeeds if the argument types
 -- have enough info to extract the runtime-rep arguments that
 -- the funTyCon requires.  This will usually be true;
 -- but may be temporarily false during canonicalization:
 --     see Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical
---
-repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-repSplitTyConApp_maybe (FunTy _ w arg res)
+--     and Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType,
+--         Wrinkle around FunTy
+tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
+tcRepSplitTyConApp_maybe (FunTy VisArg w arg res)
+  -- NB: VisArg. See Note [Decomposing fat arrow c=>t]
   | Just arg_rep <- getRuntimeRep_maybe arg
   , Just res_rep <- getRuntimeRep_maybe res
   = Just (funTyCon, [w, arg_rep, res_rep, arg, res])
-repSplitTyConApp_maybe _ = Nothing
+tcRepSplitTyConApp_maybe _ = Nothing
 
 -------------------
 -- | Attempts to tease a list type apart and gives the type of the elements if
@@ -2540,6 +2553,17 @@ ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
 nonDetCmpTypeX.
 See Note [Unique Determinism] for more details.
+
+Note [Computing equality on types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are several places within GHC that depend on the precise choice of
+definitional equality used. If we change that definition, all these places
+must be updated. This Note merely serves as a place for all these places
+to refer to, so searching for references to this Note will find every place
+that needs to be updated.
+
+See also Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.
+
 -}
 
 nonDetCmpType :: Type -> Type -> Ordering
@@ -2569,6 +2593,7 @@ data TypeOrdering = TLT  -- ^ @t1 < t2@
 
 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
     -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
+    -- See Note [Computing equality on types]
 nonDetCmpTypeX env orig_t1 orig_t2 =
     case go env orig_t1 orig_t2 of
       -- If there are casts then we also need to do a comparison of the kinds of
@@ -2623,7 +2648,10 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
       | Just (s1, t1) <- repSplitAppTy_maybe ty1
       = go env s1 s2 `thenCmpTy` go env t1 t2
     go env (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
-      = go env s1 s2 `thenCmpTy` go env t1 t2 `thenCmpTy` go env w1 w2
+        -- NB: nonDepCmpTypeX does the kind check requested by
+        -- Note [Equality on FunTys] in GHC.Core.TyCo.Rep
+      = liftOrdering (nonDetCmpTypeX env s1 s2 `thenCmp` nonDetCmpTypeX env t1 t2)
+          `thenCmpTy` go env w1 w2
         -- Comparing multiplicities last because the test is usually true
     go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index bd54ecee39..2e6b89f355 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -800,14 +800,14 @@ see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
 
 Unlike the "impure unifiers" in the typechecker (the eager unifier in
 GHC.Tc.Utils.Unify, and the constraint solver itself in GHC.Tc.Solver.Canonical), the pure
-unifier It does /not/ work up to ~.
+unifier does /not/ work up to ~.
 
 The algorithm implemented here is rather delicate, and we depend on it
 to uphold certain properties. This is a summary of these required
 properties.
 
 Notation:
- θ,φ    substitutions
+ θ,φ  substitutions
  ξ    type-function-free types
  τ,σ  other types
  τ♭   type τ, flattened
@@ -1067,7 +1067,7 @@ unify_ty :: UMEnv
          -> UM ()
 -- See Note [Specification of unification]
 -- Respects newtypes, PredTypes
-
+-- See Note [Computing equality on types] in GHC.Core.Type
 unify_ty env ty1 ty2 kco
   -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
   | TyConApp tc1 [] <- ty1