"No skolem info" panic when matching on too few fields of a GADT constructor

Summary

When matching on too few fields of a constructor, instead of "Constructor Foo should have 2 arguments, but has been given 1" I get a compiler panic.

Steps to reproduce

This program typechecks just fine:

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Bug where

data Foo a b where
  Foo :: Bar a b c -> Foo as c -> Foo (a,as) b

data Bar a b c where

data HList xs where
  Nil :: HList ()
  Cons :: x -> HList xs -> HList (x,xs)

data EqualLists xs ys where
  Refl :: EqualLists () ()
  ConsRefl :: EqualLists xs ys -> EqualLists (x,xs) (x,ys)

-- matching on ConsRefl provides the proof that the head of the two lists are the same type
-- we bring the types of the tails in scope in the pattern matches and use those in the type of k
foo :: EqualLists xs ys -> HList xs -> HList ys -> Foo xs b -> Foo ys b
foo (ConsRefl equal) (Cons _ (xs :: HList xs)) (Cons _ (ys :: HList ys)) f =
  let k :: forall d. Foo xs d -> Foo ys d
      k = foo equal xs ys
  in case f of
    Foo bar foo -> Foo bar $ k foo

But, if we forget to match on bar in the final line:

Foo foo -> Foo bar $ k foo

We instead get a panic:

ghc: panic! (the 'impossible' happened)
  (GHC version 9.0.1:
        No skolem info:
  [xs_acMw[ssk:3]]
  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

I tried to minimise the example to only require a few extensions and no imports, but it was difficult to simplify further without knowing what goes wrong.

Expected behavior

"Constructor Foo should have 2 arguments, but has been given 1"

Environment

• GHC version used: 9.0.1