Note [Unifying result types in tcRecordUpd]
After expanding and typechecking a record update in the way described in Note [Record Updates], we must take care to unify the result types. Example: type family F (a :: Type) :: Type where {} data D a = MkD { fld :: F a } f :: F Int -> D Bool -> D Int f i r = r { fld = i } This record update expands to: let x :: F alpha -- metavariable x = i in case r of MkD _ -> MkD x Because the type family F is not injective, our only hope for unifying the metavariable alpha is through the result type of the record update, which tells us that we should unify alpha := Int. Test case: T10808. Wrinkle [GADT result type in tcRecordUpd] When dealing with a GADT, we want to be careful about which result type we use. Example: data G a b where MkG :: { bar :: F a } -> G a Int g :: F Int -> G Float b -> G Int b g i r = r { bar = i } We **do not** want to use the result type from the constructor MkG, which would leave us with a result type "G alpha Int". Instead, we should use the result type from the GADT header, instantiating as above, to get "G alpha beta" which will get unified withy "G Int b". Test cases: T18809, HardRecordUpdate.
References 1
- Record Updates GHC.Tc.Gen.Expr
Referenced by 1
- GHC.Tc.Gen.Expr call site