Don't panic in ltPatersonSize

The function GHC.Tc.Utils.TcType.ltPatersonSize would panic when it
encountered a type family on the RHS, as usually these are not allowed
(type families are not allowed on the RHS of class instances or of
quantified constraints). However, it is possible to still encounter
type families on the RHS after doing a bit of constraint solving, as
seen in test case T23171. This could trigger the panic in the call to
ltPatersonSize in GHC.Tc.Solver.Canonical.mk_strict_superclasses, which
is involved in avoiding loopy superclass constraints.

This patch simply changes ltPatersonSize to return "I don't know, because
there's a type family involved" in these cases.

Fixes #23171

3 files changed, 79 insertions, 20 deletions

diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index db546edfd4..845e954b83 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -2394,22 +2394,32 @@ has a separate call to isStuckTypeFamily, so the `F` above will still be accepte
 -}
 
 
+-- | Why was the LHS 'PatersonSize' not strictly smaller than the RHS 'PatersonSize'?
+--
+-- See Note [Paterson conditions] in GHC.Tc.Validity.
 data PatersonSizeFailure
-  = PSF_TyFam TyCon     -- Type family
-  | PSF_Size            -- Too many type constructors/variables
-  | PSF_TyVar [TyVar]   -- These type variables appear more often than in instance head;
-                        --   no duplicates in this list
+  -- | Either side contains a type family.
+  = PSF_TyFam TyCon
+  -- | The size of the LHS is not strictly less than the size of the RHS.
+  | PSF_Size
+  -- | These type variables appear more often in the LHS than in the RHS.
+  | PSF_TyVar [TyVar] -- ^  no duplicates in this list
 
 --------------------------------------
 
-data PatersonSize    -- See Note [Paterson conditions] in GHC.Tc.Validity
-  = PS_TyFam TyCon   -- Mentions a type family; infinite size
-
-  | PS_Vanilla { ps_tvs :: [TyVar]  -- Free tyvars, including repetitions;
-               , ps_size :: Int     -- Number of type constructors and variables
+-- | The Paterson size of a given type, in the sense of
+-- Note [Paterson conditions] in GHC.Tc.Validity
+--
+--   - after expanding synonyms,
+--   - ignoring coercions (as they are not user written).
+data PatersonSize
+  -- | The type mentions a type family, so the size could be anything.
+  = PS_TyFam TyCon
+
+  -- | The type does not mention a type family.
+  | PS_Vanilla { ps_tvs :: [TyVar]  -- ^ free tyvars, including repetitions;
+               , ps_size :: Int     -- ^ number of type constructors and variables
     }
-  -- Always after expanding synonyms
-  -- Always ignore coercions (not user written)
   -- ToDo: ignore invisible arguments?  See Note [Invisible arguments and termination]
 
 instance Outputable PatersonSize where
@@ -2422,21 +2432,26 @@ pSizeZero, pSizeOne :: PatersonSize
 pSizeZero = PS_Vanilla { ps_tvs = [], ps_size = 0 }
 pSizeOne  = PS_Vanilla { ps_tvs = [], ps_size = 1 }
 
-ltPatersonSize :: PatersonSize    -- Size of constraint
-               -> PatersonSize    -- Size of instance head; never PS_TyFam
+-- | @ltPatersonSize ps1 ps2@ returns:
+--
+--  - @Nothing@ iff @ps1@ is definitely strictly smaller than @ps2@,
+--  - @Just ps_fail@ otherwise; @ps_fail@ says what went wrong.
+ltPatersonSize :: PatersonSize
+               -> PatersonSize
                -> Maybe PatersonSizeFailure
--- (ps1 `ltPatersonSize` ps2) returns
---     Nothing iff ps1 is strictly smaller than p2
---     Just ps_fail says what went wrong
-ltPatersonSize (PS_TyFam tc) _ = Just (PSF_TyFam tc)
 ltPatersonSize (PS_Vanilla { ps_tvs = tvs1, ps_size = s1 })
                (PS_Vanilla { ps_tvs = tvs2, ps_size = s2 })
   | s1 >= s2                                = Just PSF_Size
   | bad_tvs@(_:_) <- noMoreTyVars tvs1 tvs2 = Just (PSF_TyVar bad_tvs)
   | otherwise                               = Nothing -- OK!
-ltPatersonSize (PS_Vanilla {}) (PS_TyFam tc)
-  = pprPanic "ltPSize" (ppr tc)
-    -- Impossible because we never have a type family in an instance head
+ltPatersonSize (PS_TyFam tc) _ = Just (PSF_TyFam tc)
+ltPatersonSize _ (PS_TyFam tc) = Just (PSF_TyFam tc)
+  -- NB: this last equation is never taken when checking instances, because
+  -- type families are disallowed in instance heads.
+  --
+  -- However, this function is also used in the logic for solving superclass
+  -- constraints (see Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance),
+  -- in which case we might well hit this case (see e.g. T23171).
 
 noMoreTyVars :: [TyVar]  -- Free vars (with repetitions) of the constraint C
              -> [TyVar]  -- Free vars (with repetitions) of the head H
diff --git a/testsuite/tests/typecheck/should_compile/T23171.hs b/testsuite/tests/typecheck/should_compile/T23171.hs
new file mode 100644
index 0000000000..93a217d0fe
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T23171.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T23171 where
+
+import Data.Kind
+
+type C1 :: Type -> Type -> Constraint
+class C1 t m where
+
+type C2 :: Type -> Constraint
+class C2 a where
+
+type C3 :: Type -> Constraint
+class C2 a => C3 a where
+
+type D :: Type -> Constraint
+class D t where
+instance (forall m. C3 m => C1 t m) => D t where
+
+type T :: Type -> Type
+type family T a where
+
+try :: forall (e :: Type). D (T e) => e -> ()
+try _ = ()
+
+type C1T :: Type -> Type -> Constraint
+class C1 (T e) m => C1T e m
+
+tried :: forall (e :: Type). (forall m. C1T e m) => e -> ()
+tried = try @e
+
+-- From the call to "try", we get [W] D (T e).
+-- After using the instance for D, we get the QC [G] C3 m ==> [W] C1 (T e) m.
+--
+-- The Given "[G] C3 m" thus arises from superclass expansion
+-- from "D (T e)", which contains a type family application, T.
+-- So the logic in 'mkStrictSuperClasses' better be able to handle that when
+-- expanding the superclasses of C3 (in this case, C2); in particular
+-- ltPatersonSize needs to handle a type family in its second argument.
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 4ffb6f6a5c..7ef8cc4fa6 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -871,5 +871,6 @@ test('T22194', normal, compile, [''])
 test('QualifiedRecordUpdate',
     [ extra_files(['QualifiedRecordUpdate_aux.hs']) ]
     , multimod_compile, ['QualifiedRecordUpdate', '-v0'])
+test('T23171', normal, compile, [''])
 test('T23192', normal, compile, [''])
 test('T23199', normal, compile, [''])