+        isAlgType, isDataFamilyApp, isSatTyFamApp,

+-- | Check whether a type is a data family type

+isDataFamilyApp :: Type -> Bool

+isDataFamilyApp ty = case tyConAppTyCon_maybe ty of

+                           Just tc -> isDataFamilyTyCon tc

+                           _       -> False

+

+isSatTyFamApp :: Type -> Maybe (TyCon, [Type])

+-- Return the argument if we have a saturated type family application

+-- Why saturated?  See (ATF4) in Note [Apartness and type families]

+isSatTyFamApp (TyConApp tc tys)

+  |  isTypeFamilyTyCon tc

+  && not (tys `lengthExceeds` tyConArity tc)  -- Not over-saturated

+  = Just (tc, tys)

+isSatTyFamApp _ = Nothing

+

+    mb_sat_fam_app1 = isSatTyFamApp ty1

+    mb_sat_fam_app2 = isSatTyFamApp ty2

+      | Just (tc2, tys2) <- isSatTyFamApp ty2

+    is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyApp ty

+  = case ctOrigin ct of

+      AssocFamPatOrigin         -> True  -- See (CIG1)

+      _                         -> False

+       ; let (suppressed_items, reportable_items) = partition suppressItem tidy_items

+       ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 reportable_items

+       ; (_, leftovers) <- tryReporters ctxt2 report2 items1

+         -- If there are no other errors to report, report suppressed errors.

+         -- See Note [Suppressing confusing errors].  NB: with -fdefer-type-errors

+         -- we might have reported warnings only from `reportable_items`, but we

+         -- still want to suppress the `suppressed_items`.

+       ; when (null reportable_items) $

+         do { (_, more_leftovers) <- tryReporters ctxt_for_insols (report1++report2)

+                                                  suppressed_items

+                 -- ctxt_for_insols: the suppressed errors can be Int~Bool, which

+                 -- will have made the incoming `ctxt` be True; don't make that

+                 -- suppress the Int~Bool error!

+    report1 = [ -- We put implicit lifting errors first, because are solid errors

+                -- See "Implicit lifting" in GHC.Tc.Gen.Splice

+                -- Note [Lifecycle of an untyped splice, and PendingRnSplice]

+                ("implicit lifting", is_implicit_lifting, True, mkImplicitLiftingReporter)

+              -- Next, solid equality errors

+

+              -- Next, custom type errors

+              -- See Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint

+              --

+              -- Put custom type errors /after/ solid equality errors.  In #26255 we

+              -- had a custom error (T <= F alpha) which was suppressing a far more

+              -- informative (K Int ~ [K alpha]). That mismatch between K and [] is

+              -- definitely wrong; and if it was fixed we'd know alpha:=Int, and hence

+              -- perhaps be able to solve T <= F alpha, by reducing F Int.

+              --

+              -- But put custom type errors /before/ "non-tv eq", because if we have

+              --     () ~ TypeError blah

+              -- we want to report it as a custom error, /not/ as a mis-match

+              -- between TypeError and ()!  Also see the Assert example

+              -- in Note [Custom type errors in constraints]

+              , ("custom_error", is_user_type_error, True,  mkUserTypeErrorReporter)

+                 -- (Handles TypeError and Unsatisfiable)

+

+              -- "non-tv-eq": equalities (ty1 ~ ty2) where ty1 is not a tyvar

+

+suppressItem :: ErrorItem -> Bool

+ -- See Note [Suppressing confusing errors]

+suppressItem item

+  | Wanted <- ei_flavour item

+  , let orig = errorItemOrigin item

+  = isWantedSuperclassOrigin orig       -- See (SCE1)

+    || isWantedWantedFunDepOrigin orig  -- See (SCE2)

+  | otherwise

+  = False

+

+Which errors are suppressed?

+

+(SCE1) Superclasses of Wanteds.  These are generated only in case they trigger functional

+   dependencies.  If such a constraint is unsolved, then its "parent" constraint must

+   also be unsolved, and is much more informative to the user.  Example (#26255):

+        class (MinVersion <= F era) => Era era where { ... }

+        f :: forall era. EraFamily era -> IO ()

+        f = ..blah...   -- [W] Era era

+   Here we have simply omitted "Era era =>" from f's type.  But we'll end up with

+   /two/ Wanted constraints:

+        [W] d1 :  Era era

+        [W] d2 : MinVersion <= F era  -- Superclass of d1

+   We definitely want to report d1 and not d2!  Happily it's easy to filter out those

+   superclass-Wanteds, becuase their Origin betrays them.

+

+   See test T18851 for an example of how it is (just, barely) possible for the /only/

+   errors to be superclass-of-Wanted constraints.

+

+(SCE2) Errors which arise from the interaction of two Wanted fun-dep constraints.

+(CIG1) Constraints generated in order to unify associated type instance parameters

+(Note: Aug 25: this seems a rather tricky corner;

+               c.f. Note [Suppressing confusing errors])

+

+-}

+

+{- *********************************************************************

+*                                                                      *

+          Custom type errors: Unsatisfiable and TypeError

+*                                                                      *

+********************************************************************* -}

+

+{- Note [Custom type errors in constraints]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+When GHC reports a type-error about an unsolved-constraint, we check

+to see if the constraint contains any custom-type errors, and if so

+we report them.  Here are some examples of constraints containing type

+errors:

+

+  TypeError msg           -- The actual constraint is a type error

+

+  TypError msg ~ Int      -- Some type was supposed to be Int, but ended up

+                          -- being a type error instead

+

+  Eq (TypeError msg)      -- A class constraint is stuck due to a type error

+

+  F (TypeError msg) ~ a   -- A type function failed to evaluate due to a type err

+

+It is also possible to have constraints where the type error is nested deeper,

+for example see #11990, and also:

+

+  Eq (F (TypeError msg))  -- Here the type error is nested under a type-function

+                          -- call, which failed to evaluate because of it,

+                          -- and so the `Eq` constraint was unsolved.

+                          -- This may happen when one function calls another

+                          -- and the called function produced a custom type error.

+

+A good use-case is described in "Detecting the undetectable"

+   https://blog.csongor.co.uk/report-stuck-families/

+which features

+   type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where

+     Assert _ Dummy _ = Any

+     Assert _ _ k = k

+and an unsolved constraint like

+   Assert (TypeError ...) (F ty1) ty1 ~ ty2

+that reports that (F ty1) remains stuck.

+-}

+

+-- | A constraint is considered to be a custom type error, if it contains

+-- custom type errors anywhere in it.

+-- See Note [Custom type errors in constraints]

+getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType

+getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred

+                                  : map getUserTypeErrorMsg (subTys pred)

+  where

+   -- Richard thinks this function is very broken. What is subTys

+   -- supposed to be doing? Why are exactly-saturated tyconapps special?

+   -- What stops this from accidentally ripping apart a call to TypeError?

+    subTys t = case splitAppTys t of

+                 (t,[]) ->

+                   case splitTyConApp_maybe t of

+                              Nothing     -> []

+                              Just (_,ts) -> ts

+                 (t,ts) -> t : ts

+

+-- | Is this an user error message type, i.e. either the form @TypeError err@ or

+-- @Unsatisfiable err@?

+isTopLevelUserTypeError :: PredType -> Bool

+isTopLevelUserTypeError pred =

+  isJust (userTypeError_maybe pred) || isJust (isUnsatisfiableCt_maybe pred)

+

+-- | Does this constraint contain an user error message?

+--

+-- That is, the type is either of the form @Unsatisfiable err@, or it contains

+-- a type of the form @TypeError msg@, either at the top level or nested inside

+-- the type.

+containsUserTypeError :: PredType -> Bool

+containsUserTypeError pred =

+  isJust (getUserTypeErrorMsg pred) || isJust (isUnsatisfiableCt_maybe pred)

+

+-- | Is this type an unsatisfiable constraint?

+-- If so, return the error message.

+isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType

+isUnsatisfiableCt_maybe t

+  | Just (tc, [msg]) <- splitTyConApp_maybe t

+  , tc `hasKey` unsatisfiableClassNameKey

+  = Just msg

+  | otherwise

+  = Nothing

+

+{-

+  | Just {} <- isLitTy ty                   = True

+

+{-

+[W] Show c, Num int, C int A, C int B, C int c

+Superclasses

+   C_FD int ~ A

+   C_FD int ~ B

+   C_FD int ~ c

+-->

+   C_FD int ~ B

+   B ~ A

+-}

+{-# LANGUAGE DataKinds #-}

+{-# LANGUAGE ScopedTypeVariables #-}

+{-# LANGUAGE TypeFamilyDependencies #-}

+{-# LANGUAGE UndecidableSuperClasses #-}

+

+module T26255a where

+

+import Data.Proxy

+import GHC.TypeLits

+

+type MinVersion = 1

+

+class

+  ( KnownNat (ProtVerLow era)

+  , MinVersion <= ProtVerLow era

+  , KnownSymbol (EraName era)

+  ) =>

+  Era era

+  where

+  type EraName era = (r :: Symbol) | r -> era

+

+  type ProtVerLow era :: Nat

+

+  eraName :: Proxy era -> String

+  eraName _ = symbolVal (Proxy :: Proxy (EraName era))

+

+data FooEra

+

+instance Era FooEra where

+  type EraName FooEra = "Foo"

+  type ProtVerLow FooEra = 1

+

+data BarEra

+

+instance Era BarEra where

+  type EraName BarEra = "Bar"

+  type ProtVerLow BarEra = 2

+

+fromEraName :: (Era era, EraName era ~ name) => Proxy (name :: Symbol) -> Proxy era

+fromEraName _ = Proxy

+

+noCompileErrorMessage :: IO ()

+noCompileErrorMessage = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Bar")

+

+brokenCompileErrorMessage1 :: IO ()

+brokenCompileErrorMessage1 = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Blah")

+

+T26255a.hs:46:51: error: [GHC-18872]

+    • Couldn't match type ‘EraName era0’ with ‘"Blah"’

+        arising from a use of ‘fromEraName’

+      The type variable ‘era0’ is ambiguous

+    • In the second argument of ‘($)’, namely

+        ‘fromEraName (Proxy :: Proxy "Blah")’

+      In the second argument of ‘($)’, namely

+        ‘eraName $ fromEraName (Proxy :: Proxy "Blah")’

+      In the expression:

+        putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Blah")

+{-# LANGUAGE DataKinds #-}

+{-# LANGUAGE ScopedTypeVariables #-}

+{-# LANGUAGE TypeFamilyDependencies #-}

+{-# LANGUAGE UndecidableSuperClasses #-}

+

+module T26255b where

+

+import Data.Proxy

+import GHC.TypeLits

+

+type MinVersion = 1

+

+class

+  ( KnownNat (ProtVerLow era)

+  , MinVersion <= ProtVerLow era

+  , KnownSymbol (EraName era)

+  ) =>

+  Era era

+  where

+  type EraName era = (r :: Symbol) | r -> era

+

+  type ProtVerLow era :: Nat

+

+  eraName :: Proxy era -> String

+  eraName _ = symbolVal (Proxy :: Proxy (EraName era))

+

+data FooEra

+

+instance Era FooEra where

+  type EraName FooEra = "Foo"

+  type ProtVerLow FooEra = 1

+

+data BarEra

+

+instance Era BarEra where

+  type EraName BarEra = "Bar"

+  type ProtVerLow BarEra = 2

+

+fromEraName :: (Era era, EraName era ~ name) => Proxy (name :: Symbol) -> Proxy era

+fromEraName _ = Proxy

+

+noCompileErrorMessage :: IO ()

+noCompileErrorMessage = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Bar")

+

+brokenCompileErrorMessage2 :: IO ()

+brokenCompileErrorMessage2 = putStrLn $ eraName $ head $ fromEraName (Proxy :: Proxy "Bar")

+T26255b.hs:46:58: error: [GHC-83865]

+    • Couldn't match expected type: [Proxy era0]

+                  with actual type: Proxy BarEra

+    • In the second argument of ‘($)’, namely

+        ‘fromEraName (Proxy :: Proxy "Bar")’

+      In the second argument of ‘($)’, namely

+        ‘head $ fromEraName (Proxy :: Proxy "Bar")’

+      In the second argument of ‘($)’, namely

+        ‘eraName $ head $ fromEraName (Proxy :: Proxy "Bar")’

+{-# LANGUAGE DataKinds #-}

+{-# LANGUAGE FlexibleContexts #-}

+{-# LANGUAGE ScopedTypeVariables #-}

+{-# LANGUAGE TypeFamilyDependencies #-}

+{-# LANGUAGE TypeOperators #-}

+{-# LANGUAGE UndecidableSuperClasses #-}

+

+module T26255c where

+

+import Data.Kind

+import Data.Proxy

+import GHC.TypeLits

+

+type MinVersion = 1

+

+class

+  ( KnownNat (ProtVerLow era)

+  , MinVersion <= ProtVerLow era

+  ) =>

+  Era era

+  where

+  type ProtVerLow era :: Nat

+

+newtype EraFamily era = EraFamily Int

+

+class Era era => NewEra era where

+  eraFamilySize :: EraFamily era -> Int

+

+printEraFamilySize :: EraFamily era -> IO ()

+printEraFamilySize = print . eraFamilySize

+T26255c.hs:30:30: error: [GHC-39999]

+    • No instance for ‘NewEra era’

+        arising from a use of ‘eraFamilySize’

+      Possible fix:

+        add (NewEra era) to the context of

+          the type signature for:

+            printEraFamilySize :: forall {k} (era :: k). EraFamily era -> IO ()

+    • In the second argument of ‘(.)’, namely ‘eraFamilySize’

+      In the expression: print . eraFamilySize

+      In an equation for ‘printEraFamilySize’:

+          printEraFamilySize = print . eraFamilySize

+UnliftedNewtypesFamilyKindFail2.hs:12:1: error: [GHC-83865]

+    • Expected a type, but ‘F 5’ has kind ‘5’

+    • In the newtype family instance declaration for ‘F’

+

+test('T26255a', normal, compile_fail, [''])

+test('T26255b', normal, compile_fail, [''])