Core Lint error with horde-ad

Compiling the following module with -O fails Core Lint in 9.6 and master:

{-# LANGUAGE BangPatterns, FlexibleInstances, MultiParamTypeClasses #-}

module M where

import Data.Kind (Type)

class Vector v a where
  nothing :: v a
  just :: a -> v a

data Proxy (a :: Type) = P

instance Vector Proxy a where
  nothing = P
  just _ = P

step :: Maybe a
step = Nothing
{-# INLINE[0] step #-}

stream :: Vector v a => v a
stream = case step of
           Nothing -> nothing
           Just !x -> just x
{-# INLINE[1] stream #-}

data Id a = MkId a

f :: (Proxy (Id a), Proxy a)
f = (stream, stream)

$ ./stage1/bin/ghc -O -dcore-lint M
[1 of 1] Compiling M                ( M.hs, M.o )
*** Core Lint errors : in result of Simplifier ***
M.hs:29:1: warning:
    Argument value doesn't match argument type:
    Expected arg type: a_aHI
    Actual arg type: Id a_aHI
    Arg: ipv_sJg
    In the RHS of f_sIP :: forall {a}. Proxy (Id a)
    In the body of lambda with binder a_aHI :: *
    In a case alternative: (Just x_ax7 :: Id a_aHI)
    In a case alternative: (MkId ipv_sJg :: Id a_aHI)
    In the pattern of a case alternative: (MkId ipv_sJg :: Id a_aHI)
    Substitution: <InScope = {a_aHI}
                   IdSubst   = []
                   TvSubst   = [aHI :-> a_aHI]
                   CvSubst   = []>

GHC 9.4.3 and 9.2.5 work fine. Testcase minimized from #22955 (comment 483278).