Update core spec to reflect changes to Core.

Key changes:
 * Adds a new rule for forall-coercions over coercion variables, which
was implemented but conspicuously missing from the spec.
 * Adds treatment for FunCo.
 * Adds treatment for ForAllTy over coercion variables.
 * Improves commentary (including restoring a Note lost in
03d4852658e1b7407abb4da84b1b03bfa6f6db3b) in the source.

No changes to running code.

5 files changed, 65 insertions, 12 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 317ca00906..06dfa2e02b 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1371,7 +1371,7 @@ promoteCoercion co = case co of
     ForAllCo _ _ _
       -> ASSERT( False )
          mkNomReflCo liftedTypeKind
-      -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+      -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
     FunCo _ _ _
       -> ASSERT( False )
@@ -1420,7 +1420,7 @@ promoteCoercion co = case co of
       | otherwise
       -> ASSERT( False)
          mkNomReflCo liftedTypeKind
-           -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+           -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
     KindCo _
       -> ASSERT( False )
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 5777940ba5..b7813eb667 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1467,7 +1467,6 @@ lintType t@(ForAllTy (Bndr cv _vis) ty)
        ; checkValueKind k (text "the body of forall:" <+> ppr t)
        ; return liftedTypeKind
            -- We don't check variable escape here. Namely, k could refer to cv'
-           -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
     }}
 
 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
@@ -1826,7 +1825,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
        ; (k3, k4, t1, t2, r) <- lintCoercion co
        ; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
        ; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
-           -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+           -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
        ; in_scope <- getInScope
        ; let tyl   = mkTyCoInvForAllTy cv1 t1
              r2    = coVarRole cv1
@@ -1845,7 +1844,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
              tyr = mkTyCoInvForAllTy cv2 $
                    substTy subst t2
        ; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
-                   -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+                   -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
 lintCoercion co@(FunCo r co1 co2)
   = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
@@ -2019,7 +2018,7 @@ lintCoercion (InstCo co arg)
              , CoercionTy s2' <- s2
              -> do { return $
                        (liftedTypeKind, liftedTypeKind
-                          -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+                          -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
                        , substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
                        , substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
                        , r) }
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index c1ca32fc3c..1f2fd6cf19 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -206,6 +206,9 @@ data Type
   | ForAllTy
         {-# UNPACK #-} !TyCoVarBinder
         Type            -- ^ A Π type.
+             -- INVARIANT: If the binder is a coercion variable, it must
+             -- be mentioned in the Type. See
+             -- Note [Unused coercion variable in ForAllTy]
 
   | FunTy      -- ^ t1 -> t2   Very common, so an important special case
                 -- See Note [Function types]
@@ -218,9 +221,10 @@ data Type
   | CastTy
         Type
         KindCoercion  -- ^ A kind cast. The coercion is always nominal.
-                      -- INVARIANT: The cast is never refl.
+                      -- INVARIANT: The cast is never reflexive
                       -- INVARIANT: The Type is not a CastTy (use TransCo instead)
-                      -- See Note [Respecting definitional equality] (EQ2) and (EQ3)
+                      -- INVARIANT: The Type is not a ForAllTy over a type variable
+                      -- See Note [Respecting definitional equality] (EQ2), (EQ3), (EQ4)
 
   | CoercionTy
         Coercion    -- ^ Injection of a Coercion into a type
@@ -567,10 +571,19 @@ be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
 `eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
 our (EQ) property.
 
-Lastly, in order to detect reflexive casts reliably, we must make sure not
+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)).
 
-In sum, in order to uphold (EQ), we need the following three invariants:
+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,
+
+  ForAllTy tv (ty |> co)     and     (ForAllTy tv ty) |> co
+
+are `eqType`. But only the first can be split by splitForAllTy. So we forbid
+the second form, instead pushing the coercion inside to get the first form.
+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
@@ -578,7 +591,7 @@ In sum, in order to uphold (EQ), we need the following three invariants:
   (EQ2) No reflexive casts in CastTy.
   (EQ3) No nested CastTys.
   (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
-        See Note [Weird typing rule for ForAllTy] in GHC.Core.Type.
+        See Note [Weird typing rule for ForAllTy]
 
 These invariants are all documented above, in the declaration for Type.
 
@@ -607,6 +620,45 @@ There are cases we want to skip the check. For example, the check is
 unnecessary when it is known from the context that the input variable
 is a type variable.  In those cases, we use mkForAllTy.
 
+Note [Weird typing rule for ForAllTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is the (truncated) typing rule for the dependent ForAllTy:
+
+  inner : TYPE r
+  tyvar is not free in r
+  ----------------------------------------
+  ForAllTy (Bndr tyvar vis) inner : TYPE r
+
+Note that the kind of `inner` is the kind of the overall ForAllTy. This is
+necessary because every ForAllTy over a type variable is erased at runtime.
+Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in
+the kind) must be the same as the representation of the body. We must check
+for skolem-escape, though. The skolem-escape would prevent a definition like
+
+  undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a
+
+because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real
+type of undefined is
+
+  undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a
+
+and that HasCallStack constraint neatly sidesteps the potential skolem-escape
+problem.
+
+If the bound variable is a coercion variable:
+
+  inner : TYPE r
+  covar is free in inner
+  ------------------------------------
+  ForAllTy (Bndr covar vis) inner : Type
+
+Here, the kind of the ForAllTy is just Type, because coercion abstractions
+are *not* erased. The "covar is free in inner" premise is solely to maintain
+the representation invariant documented in
+Note [Unused coercion variable in ForAllTy]. Though there is surface similarity
+between this free-var check and the one in the tyvar rule, these two restrictions
+are truly unrelated.
+
 -}
 
 -- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
@@ -1003,6 +1055,7 @@ data Coercion
                -- The TyCon is never a synonym;
                -- we expand synonyms eagerly
                -- But it can be a type function
+               -- TyCon is never a saturated (->); use FunCo instead
 
   | AppCo Coercion CoercionN             -- lift AppTy
           -- AppCo :: e -> N -> e
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 3af971c101..3e86e86cf4 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1382,6 +1382,7 @@ mkCastTy (CastTy ty co1) co2
 
 mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co
   -- (EQ4) from the Note
+  -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.
   | isTyVar tv
   , let fvs = tyCoVarsOfCo co
   = -- have to make sure that pushing the co in doesn't capture the bound var!
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 8719746f67..10b1a85342 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -1507,7 +1507,7 @@ ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
 --        subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
 --      Question: How do we get kcoi?
 --   2. Given:
---        lkco :: <*>    -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+--        lkco :: <*>    -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 --        rkco :: <*>
 --      Wanted:
 --        ty_co_match menv' subst2 ty1 co2 lkco' rkco'