GHC 9.0.1+ panics (No skolem info), GHC 8.10.4 produces error message

If you compile the following program with GHC 9.0.1 or later, it will panic:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

type Sing :: k -> Type
type family Sing

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type D :: Type -> Type
data D a = MkD a

type SD :: D a -> Type
data SD z where
  SMkD :: Sing x -> SD (MkD x)
type instance Sing @(D a) = SD

elimD :: forall a (p :: D a ~> Type) (d :: D a).
         Sing d
      -> (forall (x :: a). Sing x -> Apply p (MkD x))
      -> Apply p d
elimD sd k = go sd
  where
    go :: forall a' (d' :: D a').
          Sing d' -> Apply p d'
    go (SMkD sx) = k sx

$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:43:30: error:ghc: panic! (the 'impossible' happened)
  (GHC version 9.0.1:
        No skolem info:
  [a_axS[sk:1]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
        pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors

On the other hand, GHC 8.10.4 will produce a proper error message:

$ /opt/ghc/8.10.4/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:43:30: error:
    • Expected kind ‘D a1’, but ‘d'’ has kind ‘D a'1’
    • In the second argument of ‘Apply’, namely ‘d'’
      In the type signature:
        go :: forall a' (d' :: D a'). Sing d' -> Apply p d'
      In an equation for ‘elimD’:
          elimD sd k
            = go sd
            where
                go :: forall a' (d' :: D a'). Sing d' -> Apply p d'
                go (SMkD sx) = k sx
    • Relevant bindings include
        k :: forall (x :: a1). Sing x -> Apply p ('MkD x)
          (bound at Bug.hs:40:10)
        sd :: Sing d (bound at Bug.hs:40:7)
        elimD :: Sing d
                 -> (forall (x :: a1). Sing x -> Apply p ('MkD x)) -> Apply p d
          (bound at Bug.hs:40:1)
   |
43 |           Sing d' -> Apply p d'
   |                              ^^

Bug.hs:44:22: error:
    • Could not deduce: x ~~ x0
      from the context: d' ~ 'MkD x
        bound by a pattern with constructor:
                   SMkD :: forall a (x :: a). Sing x -> SD ('MkD x),
                 in an equation for ‘go’
        at Bug.hs:44:9-15
      ‘x’ is a rigid type variable bound by
        a pattern with constructor:
          SMkD :: forall a (x :: a). Sing x -> SD ('MkD x),
        in an equation for ‘go’
        at Bug.hs:44:9-15
      Expected type: Sing x0
        Actual type: Sing x
    • In the first argument of ‘k’, namely ‘sx’
      In the expression: k sx
      In an equation for ‘go’: go (SMkD sx) = k sx
    • Relevant bindings include
        sx :: Sing x (bound at Bug.hs:44:14)
        go :: Sing d' -> Apply p d' (bound at Bug.hs:44:5)
        k :: forall (x :: a1). Sing x -> Apply p ('MkD x)
          (bound at Bug.hs:40:10)
        sd :: Sing d (bound at Bug.hs:40:7)
        elimD :: Sing d
                 -> (forall (x :: a1). Sing x -> Apply p ('MkD x)) -> Apply p d
          (bound at Bug.hs:40:1)
   |
44 |     go (SMkD sx) = k sx
   |                      ^^