+ data T a b = MkT1 { fa :: a, fb :: b }
+ | MkT2 { fa :: a, fc :: Int -> Int }
+ | MkT3 { fd :: a }
+
+ upd :: T a b -> c -> T a c
+ upd t x = t { fb = x}
+
+The type signature on upd is correct (i.e. the result should not be (T a b))
+because upd should be equivalent to:
+
+ upd t x = case t of
+ MkT1 p q -> MkT1 p x
+ MkT2 a b -> MkT2 p b
+ MkT3 d -> error ...
+
+So we need to give a completely fresh type to the result record,
+and then constrain it by the fields that are *not* updated ("p" above).
+
+Note that because MkT3 doesn't contain all the fields being updated,
+its RHS is simply an error, so it doesn't impose any type constraints
+
+Note [Implict type sharing]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We also take into account any "implicit" non-update fields. For example
+ data T a b where { MkT { f::a } :: T a a; ... }
+So the "real" type of MkT is: forall ab. (a~b) => a -> T a b
+
+Then consider
+ upd t x = t { f=x }
+We infer the type
+ upd :: T a b -> a -> T a b
+ upd (t::T a b) (x::a)
+ = case t of { MkT (co:a~b) (_:a) -> MkT co x }
+We can't give it the more general type
+ upd :: T a b -> c -> T c b
+
+Note [Criteria for update]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to allow update for existentials etc, provided the updated
+field isn't part of the existential. For example, this should be ok.
+ data T a where { MkT { f1::a, f2::b->b } :: T a }
+ f :: T a -> b -> T b
+ f t b = t { f1=b }
+The criterion we use is this:
+
+ The types of the updated fields
+ mention only the universally-quantified type variables
+ of the data constructor
+
+In principle one could go further, and allow
+ g :: T a -> T a
+ g t = t { f2 = \x -> x }
+because the expression is polymorphic...but that seems a bridge too far.
+
+Note [Data family example]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+ data instance T (a,b) = MkT { x::a, y::b }
+ --->
+ data :TP a b = MkT { a::a, y::b }
+ coTP a b :: T (a,b) ~ :TP a b
+
+Suppose r :: T (t1,t2), e :: t3
+Then r { x=e } :: T (t3,t1)
+ --->
+ case r |> co1 of
+ MkT x y -> MkT e y |> co2
+ where co1 :: T (t1,t2) ~ :TP t1 t2
+ co2 :: :TP t3 t2 ~ T (t3,t2)
+The wrapping with co2 is done by the constructor wrapper for MkT
+
+Outgoing invariants
+~~~~~~~~~~~~~~~~~~~
+In the outgoing (HsRecordUpd scrut binds cons in_inst_tys out_inst_tys):
+
+ * cons are the data constructors to be updated
+
+ * in_inst_tys, out_inst_tys have same length, and instantiate the
+ *representation* tycon of the data cons. In Note [Data
+ family example], in_inst_tys = [t1,t2], out_inst_tys = [t3,t2]
+
+\begin{code}
+tcExpr expr@(RecordUpd record_expr rbinds _ _ _) res_ty
+ = do {