GHC 9.6.1: equality constraints are apparently not propagated everywhere (specifically in record update syntax)

Summary

Encountered this with GHC 9.6.1. Works fine on GHC 9.4.5, 9.2.7

Steps to reproduce

Here is a reproducer:

{-# OPTIONS_GHC -Werror -Wincomplete-patterns #-}
{-# LANGUAGE TypeFamilies, GADTs, TypeOperators #-}

module Lib where

data GADT where
  GADT :: d ~ () => d -> GADT

data SomeRec = SomeRec { srField :: () }

data FooBar p where
  Foo :: FooBar ()
  Bar :: FooBar Int

getFooBar :: d -> FooBar d
getFooBar = undefined

falsePositive :: GADT -> SomeRec -> SomeRec
falsePositive (GADT di) cd =
  cd
    { srField = case getFooBar di of -- Patterns of type ‘FooBar d’ not matched: Bar
        Foo -> ()
    }

fine :: GADT -> SomeRec -> SomeRec
fine (GADT di) cd = case getFooBar di of
  Foo -> cd { srField = () }

Notice moving case out of the record update fixes this (but it has different strictness characteristics).

Matching on GADT puts d ~ () into scope, so matching on getFooBar di has only one possible alternative. But apparently the constraint is not propagated into the record update?

Expected behavior

To compile without incomplete pattern warning.

Environment

• GHC version used: 9.6.1

Optional:

• Operating System: Linux
• System Architecture: amd64