TyEq:N assertion: only for saturated applications

The assertion that checked TyEq:N in canEqCanLHSFinish incorrectly
triggered in the case of an unsaturated newtype TyCon heading the RHS,
even though we can't unwrap such an application. Now, we only trigger
an assertion failure in case of a saturated application of a newtype
TyCon.

Fixes #22310

4 files changed, 41 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 6622c67a4b..332d59244a 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -2032,6 +2032,14 @@ and the Id newtype is unwrapped. This is assured by requiring only rewritten
 types in canEqCanLHS *and* having the newtype-unwrapping check above
 the tyvar check in can_eq_nc.
 
+Note that this only applies to saturated applications of newtype TyCons, as
+we can't rewrite an unsaturated application. See for example T22310, where
+we ended up with:
+
+  newtype Compose f g a = ...
+
+  [W] t[tau] ~# Compose Foo Bar
+
 Note [Put touchable variables on the left]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Ticket #10009, a very nasty example:
@@ -2401,15 +2409,17 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 
     lhs_ty = canEqLHSType lhs
 
-    -- This is about (TyEq:N): check that we don't have a newtype
-    -- whose constructor is in scope at the top-level of the RHS.
+    -- This is about (TyEq:N): check that we don't have a saturated application
+    -- of a newtype TyCon at the top level of the RHS, if the constructor
+    -- of the newtype is in scope.
     ty_eq_N_OK :: TcS Bool
     ty_eq_N_OK
       | ReprEq <- eq_rel
-      , Just tc <- tyConAppTyCon_maybe rhs
+      , Just (tc, tc_args) <- splitTyConApp_maybe rhs
       , Just con <- newTyConDataCon_maybe tc
-      -- #21010: only a problem if the newtype constructor is in scope
-      -- yet we didn't rewrite it away.
+      -- #22310: only a problem if the newtype TyCon is saturated.
+      , tc_args `lengthAtLeast` tyConArity tc
+      -- #21010: only a problem if the newtype constructor is in scope.
       = do { rdr_env <- getGlobalRdrEnvTcS
            ; let con_in_scope = isJust $ lookupGRE_Name rdr_env (dataConName con)
            ; return $ not con_in_scope }
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 586a6a68aa..ea2a5f7189 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -235,7 +235,8 @@ data Ct
        --   * (TyEq:F) rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
        --   * (TyEq:K) tcTypeKind lhs `tcEqKind` tcTypeKind rhs; Note [Ct kind invariant]
-       --   * (TyEq:N) If the equality is representational, rhs has no top-level newtype
+       --   * (TyEq:N) If the equality is representational, rhs is not headed by a saturated
+       --     application of a newtype TyCon.
        --     See Note [No top-level newtypes on RHS of representational equalities]
        --     in GHC.Tc.Solver.Canonical. (Applies only when constructor of newtype is
        --     in scope.)
diff --git a/testsuite/tests/typecheck/should_compile/T22310.hs b/testsuite/tests/typecheck/should_compile/T22310.hs
new file mode 100644
index 0000000000..9605a674be
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22310.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE GADTs, ScopedTypeVariables, StandaloneKindSignatures #-}
+
+module T22310 where
+
+import Data.Coerce ( coerce )
+import Data.Kind   ( Type )
+
+type Some :: (Type -> Type) -> Type
+data Some t where
+  Some :: t ex -> Some t
+
+type NT :: Type -> Type
+newtype NT f = MkNT ()
+
+oops :: Some NT -> Some NT
+oops = coerce (\(Some @NT x) -> Some x)
+  -- After canonicalisation of Wanted constraints,
+  -- we end up with:
+  --
+  -- [W] t[tau:0] ~R# NT
+  --
+  -- Note the newtype TyCon on the RHS.
+  -- Does not violate TyEq:N, because it is unsaturated!
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 802eb9097d..c1b10ff6c8 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -856,3 +856,4 @@ test('DeepSubsumption09', normal, compile, [''])
 test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21550', normal, compile, [''])
+test('T22310', normal, compile, [''])