Wrinkles

 (W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and

      aBSENT_CONSTRAINT_ERROR_ID for types of kind Constraint.

      of type TYPE rr. See (CPR2) in Note [Which types are unboxed?] in

      GHC.Core.Opt.WorkWrap.Utils.

 Type and Constraint are not equal (eqType) but they are not /apart/

 either. Reason (c.f. #7451):

      So in GHC.Tc.Instance.Class.matchTypeable, Type and Constraint are

      treated as separate TyCons; i.e. given no special treatment.

 Note [RuntimeRep polymorphism]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 Generally speaking, you can't be polymorphic in `RuntimeRep`.  E.g

 -- | Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)`

 -- produce a coercion `rep_co :: r1 ~ r2`

 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion

 mkRuntimeRepCo co

   = assert (isTYPEorCONSTRAINT k1 && isTYPEorCONSTRAINT k2) $

     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2

     Pair k1 k2 = coercionKind kind_co

 isReflCoVar_maybe :: Var -> Maybe Coercion

 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)

 -- Works on all kinds of Vars, not just CoVars

        , Just (tc2, tys2) <- splitTyConApp_maybe ty2

        , let { len1 = length tys1

              ; len2 = length tys2 }

        && len1 == len2

        && n < len1

        && r == tyConRole (coercionRole co) tc1 n

          hang (text "Inhomogeneous axiom")

             2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$

                text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }

          -- Type and Constraint are not Apart, so this test allows

          -- the newtype axiom for a single-method class.  Indeed the

          -- whole reason Type and Constraint are not Apart is to allow

 import GHC.Utils.Outputable

 import GHC.Types.Name

 import GHC.Types.Name.Env

 import Control.Monad (join)

 import Data.Data (Data)

 roughMatchTyConName :: TyCon -> Name

 roughMatchTyConName tc

 -- | Trie of @[RoughMatchTc]@

 --

                       Nothing  -> pprPanic "piResultTy" (ppr ty $$ ppr arg)

 piResultTy_maybe :: Type -> Type -> Maybe Type

 piResultTy_maybe ty arg = case coreFullView ty of

   FunTy { ft_res = res } -> Just res

 import GHC.Types.Var

 import GHC.Types.Var.Env

 import GHC.Types.Var.Set

 import GHC.Core.Type     hiding ( getTvSubstEnv )

 import GHC.Core.Coercion hiding ( getCvSubstEnv )

 import GHC.Core.Predicate( scopedSort )

          See Note [Apartness and type families]

     * MARInfinite (occurs check):

          See Note [Infinitary substitutions]

     * MARCast (obscure):

          See (KCU2) in Note [Kind coercions in Unify]

 -- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence:

 -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv

 data MaybeApartReason

   = MARTypeFamily   -- ^ matching e.g. F Int ~? Bool

   | MARInfinite     -- ^ matching e.g. a ~? Maybe a

   | MARCast         -- ^ Very obscure.

     -- See (KCU2) in Note [Kind coercions in Unify]

 -- See (UR1) in Note [Unification result] for why MARInfinite wins

 combineMAR MARInfinite         _ = MARInfinite   -- MARInfinite wins

 combineMAR MARTypeFamily       r = r             -- Otherwise it doesn't really matter

 combineMAR MARCast             r = r

 instance Outputable MaybeApartReason where

   ppr MARTypeFamily       = text "MARTypeFamily"

   ppr MARInfinite         = text "MARInfinite"

   ppr MARCast             = text "MARCast"

 instance Semigroup MaybeApartReason where

        ; unify_tc_app env tc1 tys1 tys2

        }

   where

     mb_tc_app1 = splitTyConApp_maybe ty1

     mb_tc_app2 = splitTyConApp_maybe ty2

   | k `eqType` naturalTy      = doTyLit knownNatClassName         t

   | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName      t

   | k `eqType` charTy         = doTyLit knownCharClassName        t

   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]

   , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks

 type family G a where

   G (a b) = a

 foo :: (F (G Constraint)) -> Bool

 foo x = x

   H a a = Int

   H a b = Bool

 bar1 x = x

 bar2 x = x

 test('T24090a', normal, compile_fail, [''])

 test('T24090b', normal, compile, ['']) # scheduled to become an actual error in GHC 9.16

 test('T24298', normal, compile_fail, [''])

 test('T24318', normal, compile_fail, [''])

 # all the various do expansion fail messages