Level number panic with LinearTypes

The following program

{-# LANGUAGE LinearTypes #-}
module T where

data C a = forall p. C (a %p -> a)

f :: C a -> C a
f b = C (\x -> case b of C g -> g x)

causes a level number assertion failure:

  GHC version 9.3.20220317:
	ASSERT failed!
  2
  1
  p_ax2[tau:1]
  p_ax6[ssk:2]
  Call stack:
      CallStack (from HasCallStack):
        massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1056:10 in ghc:GHC.Tc.Utils.TcMType

If this assertion is skipped, it fails Core Lint, due to an out-of-scope multiplicity variable.

Reproduced on 9.2 and HEAD. Related: #20232 (closed) and #18998 (closed).

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information