Record update typing is wrong

Consider this

type family F a

data T b = MkT { x :: [Int], y :: [F b] }

emptyT :: T b
emptyT = MkT [] []

foo1 :: [Int] -> T b
foo1  newx = emptyT { x = newx }

foo2 :: [Int] -> T b
foo2  newx = case emptyT of MkT x y -> MkT newx y

According to the Haskell report, foo1 and foo2 should behave the same. But they don't: foo2 is rejected with

Foo.hs:29:49: error:
    • Couldn't match type: F b0
                     with: F b
      Expected: [F b]
        Actual: [F b0]
      NB: ‘F’ is a non-injective type family
      The type variable ‘b0’ is ambiguous
    • In the second argument of ‘MkT’, namely ‘y’
      In the expression: MkT newx y
      In a case alternative: MkT x y -> MkT newx y
    • Relevant bindings include
        y :: [F b0] (bound at Foo.hs:29:35)
        foo2 :: [Int] -> T b (bound at Foo.hs:29:1)
   |
29 | foo2  newx = case emptyT of MkT x y -> MkT newx y
   |                                                 ^

And indeed that makes sense: becuase F is a type family, we have no way to know at what type to instantiate emptyT.

So why does foo1 work? It's because of this code in GHC.Tc.Gen.Expr, in the RecordUpd case of tcExpr:

        -- STEP 4  Note [Type of a record update]
        -- Figure out types for the scrutinee and result
        -- Both are of form (T a b c), with fresh type variables, but with
        -- common variables where the scrutinee and result must have the same type
        -- These are variables that appear in *any* arg of *any* of the
        -- relevant constructors *except* in the updated fields
        --
        ; let fixed_tvs = getFixedTyVars upd_fld_occs con1_tvs relevant_cons
              is_fixed_tv tv = tv `elemVarSet` fixed_tvs

Those "fixed" tyvars are the ones that GHC thinks are going to be the same in "before" and "after" -- and it used all the free vars of unaffected fields (in this case the field y). So b is treated as "fixed".

But that is not what the report says; and it would be reasonably complicated to specify. The simplest thing is to regard this a bug, which leads GHC to accept too many programs. It is not hard to fix foo2:

foo2 :: forall b. [Int] -> T b
foo2  newx = case (emptyT :: T b) of MkT x y -> MkT newx y

This came up during @CarrieMY's work on !7320 (closed)/#18802 (closed). It turns out that GHC itself uses this idiom in GHC.Hs.Utils:

mkRecStmt anns stmts  = (emptyRecStmt' anns) { recS_stmts = stmts }

When we desugar record update in the renamer, this rejected for the reasons above.