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:
```haskell
{-# 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
issue