GitLab

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!