Consider ``` type family F a type instance F Int = Int type instance F Bool = Int data T a = MkT { x :: F a, y :: a } foo1 :: T Int -> T Bool foo1 (MkT { x = x }) = MkT { x = x, y = True} foo2 :: T Int -> T Bool foo2 t = t { y = True } ``` `foo1` typechecks fine, but `foo2` complains ``` Foo.hs:16:10: error: • Couldn't match type ‘Int’ with ‘Bool’ Expected type: T Bool Actual type: T Int • In the expression: t {y = True} In an equation for ‘foo2’: foo2 t = t {y = True} ``` This is bogus. `foo2` should be fine -- precisely because `foo1` is. The offending code is in the `RecordUpd` case of `GHc.Tc.Gen.Expr.tcExpr`. See this comment ``` -- 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 ``` With the advent of type families "appearing in" a type is not the same as being fixed by it. Not hard to fix; might even lead to less code!