Record update is over-restrictive
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!