Fix newtype eta-reduction

The eta-reduction we do for newype axioms was generating
an inhomogeneous axiom: see #19739.

This patch fixes it in a simple way; see GHC.Tc.TyCl.Build
Note [Newtype eta and homogeneous axioms]

3 files changed, 82 insertions, 18 deletions

diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 56fe29cb7e..d972752e9a 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -1337,17 +1337,22 @@ Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider
         newtype Parser a = MkParser (IO a) deriving Monad
-Are these two types equal (that is, does a coercion exist between them)?
+Are these two types equal? That is, does a coercion exist between them?
         Monad Parser
         Monad IO
-which we need to make the derived instance for Monad Parser.
+(We need this coercion to make the derived instance for Monad Parser.)
 
 Well, yes.  But to see that easily we eta-reduce the RHS type of
-Parser, in this case to IO, so that even unsaturated applications
-of Parser will work right.  This eta reduction is done when the type
-constructor is built, and cached in NewTyCon.
+Parser, in this case to IO, so that even unsaturated applications of
+Parser will work right.  So instead of
+   axParser :: forall a. Parser a ~ IO a
+we generate an eta-reduced axiom
+   axParser :: Parser ~ IO
 
-Here's an example that I think showed up in practice
+This eta reduction is done when the type constructor is built, in
+GHC.Tc.TyCl.Build.mkNewTyConRhs, and cached in NewTyCon.
+
+Here's an example that I think showed up in practice.
 Source code:
         newtype T a = MkT [a]
         newtype Foo m = MkFoo (forall a. m a -> Int)
@@ -1359,14 +1364,15 @@ Source code:
         w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
 
 After desugaring, and discarding the data constructors for the newtypes,
-we get:
-        w2 = w1 `cast` Foo CoT
-so the coercion tycon CoT must have
-        kind:    T ~ []
- and    arity:   0
+we would like to get:
+        w2 = w1 `cast` Foo axT
 
-This eta-reduction is implemented in GHC.Tc.TyCl.Build.mkNewTyConRhs.
+so that w2 and w1 share the same code. To do this, the coercion axiom
+axT must have
+        kind:    axT :: T ~ []
+ and    arity:   0
 
+See also Note [Newtype eta and homogeneous axioms] in GHC.Tc.TyCl.Build.
 
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs
index 588f209377..1dba4093f1 100644
--- a/compiler/GHC/Tc/TyCl/Build.hs
+++ b/compiler/GHC/Tc/TyCl/Build.hs
@@ -79,6 +79,8 @@ mkNewTyConRhs tycon_name tycon con
         -- has a single argument (Foo a) that is a *type class*, so
         -- dataConInstOrigArgTys returns [].
 
+    -- Eta-reduce the newtype
+    -- See Note [Newtype eta] in GHC.Core.TyCon
     etad_tvs   :: [TyVar]  -- Matched lazily, so that mkNewTypeCo can
     etad_roles :: [Role]   -- return a TyCon without pulling on rhs_ty
     etad_rhs   :: Type     -- See Note [Tricky iface loop] in GHC.Iface.Load
@@ -89,12 +91,51 @@ mkNewTyConRhs tycon_name tycon con
                -> Type          -- Rhs type
                -> ([TyVar], [Role], Type)  -- Eta-reduced version
                                            -- (tyvars in normal order)
-    eta_reduce (a:as) (_:rs) ty | Just (fun, arg) <- splitAppTy_maybe ty,
-                                  Just tv <- getTyVar_maybe arg,
-                                  tv == a,
-                                  not (a `elemVarSet` tyCoVarsOfType fun)
-                                = eta_reduce as rs fun
-    eta_reduce tvs rs ty = (reverse tvs, reverse rs, ty)
+    eta_reduce (a:as) (_:rs) ty
+      | Just (fun, arg) <- splitAppTy_maybe ty
+      , Just tv <- getTyVar_maybe arg
+      , tv == a
+      , not (a `elemVarSet` tyCoVarsOfType fun)
+      , typeKind fun `eqType` typeKind (mkTyConApp tycon (mkTyVarTys $ reverse as))
+        -- Why this kind-check?  See Note [Newtype eta and homogeneous axioms]
+      = eta_reduce as rs fun
+    eta_reduce as rs ty = (reverse as, reverse rs, ty)
+
+{- Note [Newtype eta and homogeneous axioms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When eta-reducing a newtype, we must be careful to make sure the axiom
+is homogeneous.  (That is, the two types related by the axiom must
+have the same kind.)  All known proofs of type safety for Core rely on
+the homogeneity of axioms, so let's not monkey with that.
+
+It is easy to mistakenly make an inhomogeneous axiom (#19739):
+  type T :: forall (a :: Type) -> Type
+  newtype T a = MkT (Proxy a)
+
+Can we eta-reduce, thus?
+  axT :: T ~ Proxy
+
+No!  Because
+   T     :: forall a -> Type
+   Proxy :: Type     -> Type
+
+This is inhomogeneous. Hence, we have an extra kind-check in eta_reduce,
+to make sure the reducts have the same kind. This is simple, although
+perhaps quadratic in complexity, if we eta-reduce many arguments (which
+seems vanishingly unlikely in practice).  But NB that the free-variable
+check, which immediately precedes the kind check, is also potentially
+quadratic.
+
+There are other ways we could do the check (discussion on #19739):
+
+* We could look at the sequence of binders on the newtype and on the
+  head of the representation type, and make sure the visibilities on
+  the binders match up. This is quite a bit more code, and the reasoning
+  is subtler.
+
+* We could, say, do the kind-check at the end and then backtrack until the
+  kinds match up. Hard to know whether that's more performant or not.
+-}
 
 ------------------------------------------------------
 buildDataCon :: FamInstEnvs
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index fb83e99583..c5be699e13 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1054,6 +1054,23 @@ however, so this Note aims to describe these subtleties:
   themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
   does.
 
+* Happily, we don't need to worry about the possibility of
+  building an inhomogeneous axiom, described in GHC.Tc.TyCl.Build
+  Note [Newtype eta and homogeneous axioms].   For example
+     type F :: Type -> forall (b :: Type) -> Type
+     data family F a b
+     newtype instance F Int b = MkF (Proxy b)
+  we get a newtype, and a eta-reduced axiom connecting the data family
+  with the newtype:
+     type R:FIntb :: forall (b :: Type) -> Type
+     newtype R:FIntb b = MkF (Proxy b)
+     axiom Foo.D:R:FIntb0 :: F Int = Foo.R:FIntb
+  Now the subtleties of Note [Newtype eta and homogeneous axioms] are
+  dealt with by the newtype (via mkNewTyConRhs called in tcDataFamInstDecl)
+  while the axiom connecting F Int ~ R:FIntb is eta-reduced, but the
+  quantifer 'b' is derived from the original data family F, and so the
+  kinds will always match.
+
 Note [Kind inference for data family instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this GADT-style data type declaration, where I have used