Fix unifier bug: failing to decompose over-saturated type familywip/T22647

This simple patch fixes #22647

3 files changed, 37 insertions, 13 deletions

diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index e0594cb811..0ac530d8bd 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -1054,20 +1054,11 @@ unify_ty env ty1 ty2 _kco
             ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
               don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
 
-  | Just (tc1, _) <- mb_tc_app1
-  , not (isGenerativeTyCon tc1 Nominal)
-    -- E.g.   unify_ty (F ty1) b  =  MaybeApart
-    --        because the (F ty1) behaves like a variable
-    --        NB: if unifying, we have already dealt
-    --            with the 'ty2 = variable' case
-  = maybeApart MARTypeFamily
+  | isTyFamApp mb_tc_app1     -- A (not-over-saturated) type-family application
+  = maybeApart MARTypeFamily  -- behaves like a type variable; might match
 
-  | Just (tc2, _) <- mb_tc_app2
-  , not (isGenerativeTyCon tc2 Nominal)
-  , um_unif env
-    -- E.g.   unify_ty [a] (F ty2) =  MaybeApart, when unifying (only)
-    --        because the (F ty2) behaves like a variable
-    --        NB: we have already dealt with the 'ty1 = variable' case
+  | isTyFamApp mb_tc_app2     -- A (not-over-saturated) type-family application
+  , um_unif env               -- behaves like a type variable; might unify
   = maybeApart MARTypeFamily
 
   -- TYPE and CONSTRAINT are not Apart
@@ -1169,6 +1160,17 @@ unify_tys env orig_xs orig_ys
       -- Possibly different saturations of a polykinded tycon
       -- See Note [Polykinded tycon applications]
 
+isTyFamApp :: Maybe (TyCon, [Type]) -> Bool
+-- True if we have a saturated or under-saturated type family application
+-- If it is /over/ saturated then we return False.  E.g.
+--     unify_ty (F a b) (c d)    where F has arity 1
+-- we definitely want to decompose that type application! (#22647)
+isTyFamApp (Just (tc, tys))
+  =  not (isGenerativeTyCon tc Nominal)       -- Type family-ish
+  && not (tys `lengthExceeds` tyConArity tc)  -- Not over-saturated
+isTyFamApp Nothing
+  = False
+
 ---------------------------------
 uVar :: UMEnv
      -> InTyVar         -- Variable to be unified
diff --git a/testsuite/tests/typecheck/should_compile/T22647.hs b/testsuite/tests/typecheck/should_compile/T22647.hs
new file mode 100644
index 0000000000..10cf5a98e8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22647.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeApplications, KindSignatures, DataKinds, TypeFamilies, FlexibleInstances #-}
+
+module T22647 where
+
+import Data.Kind
+
+data D = D
+type family F :: D -> Type
+
+class C f where
+  meth :: f
+
+instance C (f (p :: D)) where   -- f :: D -> Type
+  meth = error "urk1"
+
+instance C (g (q :: Type)) where -- g :: Type -> Type
+  meth = error "urk2"
+
+x = meth :: F 'D
+
+y = meth :: [Type]
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 1f1e7d8d1f..577ce86d65 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -853,3 +853,4 @@ test('T21550', normal, compile, [''])
 test('T22310', normal, compile, [''])
 test('T22331', normal, compile, [''])
 test('T22516', normal, compile, [''])
+test('T22647', normal, compile, [''])