Desugar RecordUpd in `tcExpr`wip/T18802

This patch typechecks record updates by desugaring them inside
the typechecker using the HsExpansion mechanism, and then typechecking
this desugared result.

Example:

    data T p q = T1 { x :: Int, y :: Bool, z :: Char }
               | T2 { v :: Char }
               | T3 { x :: Int }
               | T4 { p :: Float, y :: Bool, x :: Int }
               | T5

The record update `e { x=e1, y=e2 }` desugars as follows

  e { x=e1, y=e2 }
    ===>
  let { x' = e1; y' = e2 } in
  case e of
     T1 _ _ z -> T1 x' y' z
     T4 p _ _ -> T4 p y' x'

The desugared expression is put into an HsExpansion, and we typecheck
that.

The full details are given in Note [Record Updates] in GHC.Tc.Gen.Expr.

Fixes #2595 #3632 #10808 #10856 #16501 #18311 #18802 #21158 #21289

Updates haddock submodule

5 files changed, 571 insertions, 404 deletions

diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 182818616a..e1679d82d0 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -82,7 +82,7 @@ import GHC.Types.Error
 import GHC.Types.Hint (UntickedPromotedThing(..))
 import GHC.Types.FieldLabel (FieldLabelString)
 import GHC.Types.ForeignCall (CLabelString)
-import GHC.Types.Name (Name, OccName, getSrcLoc)
+import GHC.Types.Name (Name, OccName, getSrcLoc, getSrcSpan)
 import GHC.Types.Name.Reader
 import GHC.Types.SrcLoc
 import GHC.Types.TyThing (TyThing)
@@ -2950,14 +2950,15 @@ pprRelevantBindings :: RelevantBindings -> SDoc
 -- This function should be in "GHC.Tc.Errors.Ppr",
 -- but's it's here for the moment as it's needed in "GHC.Tc.Errors".
 pprRelevantBindings (RelevantBindings bds ran_out_of_fuel) =
-  ppUnless (null bds) $
+  ppUnless (null rel_bds) $
     hang (text "Relevant bindings include")
-       2 (vcat (map ppr_binding bds) $$ ppWhen ran_out_of_fuel discardMsg)
+       2 (vcat (map ppr_binding rel_bds) $$ ppWhen ran_out_of_fuel discardMsg)
   where
     ppr_binding (nm, tidy_ty) =
       sep [ pprPrefixOcc nm <+> dcolon <+> ppr tidy_ty
           , nest 2 (parens (text "bound at"
                <+> ppr (getSrcLoc nm)))]
+    rel_bds = filter (not . isGeneratedSrcSpan . getSrcSpan . fst) bds
 
 discardMsg :: SDoc
 discardMsg = text "(Some bindings suppressed;" <+>
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 492c46c7df..45c3dabbe5 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -23,7 +23,7 @@ module GHC.Tc.Gen.Expr
          tcPolyExpr, tcExpr,
          tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
          tcCheckId,
-         getFixedTyVars ) where
+         ) where
 
 import GHC.Prelude
 
@@ -37,16 +37,18 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Types.Basic
 import GHC.Types.Error
+import GHC.Types.Unique.Map ( UniqMap, listToUniqMap, lookupUniqMap )
 import GHC.Core.Multiplicity
 import GHC.Core.UsageEnv
 import GHC.Tc.Errors.Types
-import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic, hasFixedRuntimeRep )
 import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Gen.App
 import GHC.Tc.Gen.Head
 import GHC.Tc.Gen.Bind        ( tcLocalBinds )
 import GHC.Tc.Instance.Family ( tcGetFamInstEnvs )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
+import GHC.Rename.Expr        ( mkExpandedExpr )
 import GHC.Rename.Env         ( addUsedGRE )
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.Arrow
@@ -67,9 +69,9 @@ import GHC.Types.Name.Reader
 import GHC.Core.TyCon
 import GHC.Core.Type
 import GHC.Tc.Types.Evidence
-import GHC.Types.Var.Set
 import GHC.Builtin.Types
 import GHC.Builtin.Names
+import GHC.Builtin.Uniques ( mkBuiltinUnique )
 import GHC.Driver.Session
 import GHC.Types.SrcLoc
 import GHC.Utils.Misc
@@ -85,6 +87,8 @@ import GHC.Types.Unique.Set ( UniqSet, mkUniqSet, elementOfUniqSet, nonDetEltsUn
 import Data.Function
 import Data.List (partition, sortBy, groupBy, intersect)
 
+import GHC.Data.Bag ( unitBag )
+
 {-
 ************************************************************************
 *                                                                      *
@@ -502,319 +506,30 @@ tcExpr expr@(RecordCon { rcon_con = L loc con_name
   where
     orig = OccurrenceOf con_name
 
-{-
-Note [Type of a record update]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The main complication with RecordUpd is that we need to explicitly
-handle the *non-updated* fields.  Consider:
-
-        data T a b c = MkT1 { fa :: a, fb :: (b,c) }
-                     | MkT2 { fa :: a, fb :: (b,c), fc :: c -> c }
-                     | MkT3 { fd :: a }
-
-        upd :: T a b c -> (b',c) -> T a b' c
-        upd t x = t { fb = x}
-
-The result type should be (T a b' c)
-not (T a b c),   because 'b' *is not* mentioned in a non-updated field
-not (T a b' c'), because 'c' *is*     mentioned in a non-updated field
-NB that it's not good enough to look at just one constructor; we must
-look at them all; cf #3219
-
-After all, 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).
-We call these the "fixed" type variables, and compute them in getFixedTyVars.
-
-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.
-Hence the use of 'relevant_cont'.
-
-Note [Implicit 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
-
-NB: this is not (quite) the same as being a "naughty" record selector
-(See Note [Naughty record selectors]) in GHC.Tc.TyCl), at least
-in the case of GADTs. Consider
-   data T a where { MkT :: { f :: a } :: T [a] }
-Then f is not "naughty" because it has a well-typed record selector.
-But we don't allow updates for 'f'.  (One could consider trying to
-allow this, but it makes my head hurt.  Badly.  And no one has asked
-for it.)
-
-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]
-
-Note [Mixed Record Field Updates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following pattern synonym.
-
-  data MyRec = MyRec { foo :: Int, qux :: String }
-
-  pattern HisRec{f1, f2} = MyRec{foo = f1, qux=f2}
-
-This allows updates such as the following
-
-  updater :: MyRec -> MyRec
-  updater a = a {f1 = 1 }
-
-It would also make sense to allow the following update (which we reject).
-
-  updater a = a {f1 = 1, qux = "two" } ==? MyRec 1 "two"
-
-This leads to confusing behaviour when the selectors in fact refer the same
-field.
-
-  updater a = a {f1 = 1, foo = 2} ==? ???
-
-For this reason, we reject a mixture of pattern synonym and normal record
-selectors in the same update block. Although of course we still allow the
-following.
-
-  updater a = (a {f1 = 1}) {foo = 2}
-
-  > updater (MyRec 0 "str")
-  MyRec 2 "str"
-
--}
-
 -- Record updates via dot syntax are replaced by desugared expressions
 -- in the renamer. See Note [Overview of record dot syntax] in
 -- GHC.Hs.Expr. This is why we match on 'rupd_flds = Left rbnds' here
 -- and panic otherwise.
 tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = Left rbnds }) res_ty
   = assert (notNull rbnds) $
-    do  { -- STEP -2: typecheck the record_expr, the record to be updated
-          (record_expr', record_rho) <- tcScalingUsage Many $ tcInferRho record_expr
-            -- Record update drops some of the content of the record (namely the
-            -- content of the field being updated). As a consequence, unless the
-            -- field being updated is unrestricted in the record, or we need an
-            -- unrestricted record. Currently, we simply always require an
-            -- unrestricted record.
-            --
-            -- Consider the following example:
-            --
-            -- data R a = R { self :: a }
-            -- bad :: a ⊸ ()
-            -- bad x = let r = R x in case r { self = () } of { R x' -> x' }
+    do  { -- Desugar the record update. See Note [Record Updates].
+        ; (ds_expr, ds_res_ty, err_ctxt) <- desugarRecordUpd record_expr rbnds res_ty
+
+          -- Typecheck the desugared expression.
+        ; expr' <- addErrCtxt err_ctxt $
+                   tcExpr (mkExpandedExpr expr ds_expr) (Check ds_res_ty)
+            -- NB: it's important to use ds_res_ty and not res_ty here.
+            -- Test case: T18802b.
+
+        ; addErrCtxt err_ctxt $ tcWrapResultMono expr expr' ds_res_ty res_ty
+            -- We need to unify the result type of the desugared
+            -- expression with the expected result type.
             --
-            -- This should definitely *not* typecheck.
-
-        -- STEP -1  See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
-        -- After this we know that rbinds is unambiguous
-        ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty
-        ; let upd_flds = map (unLoc . hfbLHS . unLoc) rbinds
-              upd_fld_occs = map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc) upd_flds
-              sel_ids      = map selectorAmbiguousFieldOcc upd_flds
-        -- STEP 0
-        -- Check that the field names are really field names
-        -- and they are all field names for proper records or
-        -- all field names for pattern synonyms.
-        ; let bad_guys = [ setSrcSpan loc $ addErrTc (notSelector fld_name)
-                         | fld <- rbinds,
-                           -- Excludes class ops
-                           let L loc sel_id = hsRecUpdFieldId (unLoc fld),
-                           not (isRecordSelector sel_id),
-                           let fld_name = idName sel_id ]
-        ; unless (null bad_guys) (sequence bad_guys >> failM)
-        -- See Note [Mixed Record Field Updates]
-        ; let (data_sels, pat_syn_sels) =
-                partition isDataConRecordSelector sel_ids
-        ; massert (all isPatSynRecordSelector pat_syn_sels)
-        ; checkTc ( null data_sels || null pat_syn_sels )
-                  ( mixedSelectors data_sels pat_syn_sels )
-
-        -- STEP 1
-        -- Figure out the tycon and data cons from the first field name
-        ; let   -- It's OK to use the non-tc splitters here (for a selector)
-              sel_id : _  = sel_ids
-
-              mtycon :: Maybe TyCon
-              mtycon = case idDetails sel_id of
-                          RecSelId (RecSelData tycon) _ -> Just tycon
-                          _ -> Nothing
-
-              con_likes :: [ConLike]
-              con_likes = case idDetails sel_id of
-                             RecSelId (RecSelData tc) _
-                                -> map RealDataCon (tyConDataCons tc)
-                             RecSelId (RecSelPatSyn ps) _
-                                -> [PatSynCon ps]
-                             _  -> panic "tcRecordUpd"
-                -- NB: for a data type family, the tycon is the instance tycon
-
-              relevant_cons = conLikesWithFields con_likes upd_fld_occs
-                -- A constructor is only relevant to this process if
-                -- it contains *all* the fields that are being updated
-                -- Other ones will cause a runtime error if they occur
-
-        -- Step 2
-        -- Check that at least one constructor has all the named fields
-        -- i.e. has an empty set of bad fields returned by badFields
-        ; checkTc (not (null relevant_cons)) (badFieldsUpd rbinds con_likes)
-
-        -- Take apart a representative constructor
-        ; let con1 = assert (not (null relevant_cons) ) head relevant_cons
-              (con1_tvs, _, _, _prov_theta, req_theta, scaled_con1_arg_tys, _)
-                 = conLikeFullSig con1
-              con1_arg_tys = map scaledThing scaled_con1_arg_tys
-                -- We can safely drop the fields' multiplicities because
-                -- they are currently always 1: there is no syntax for record
-                -- fields with other multiplicities yet. This way we don't need
-                -- to handle it in the rest of the function
-              con1_flds   = map flLabel $ conLikeFieldLabels con1
-              con1_tv_tys = mkTyVarTys con1_tvs
-              con1_res_ty = case mtycon of
-                              Just tc -> mkFamilyTyConApp tc con1_tv_tys
-                              Nothing -> conLikeResTy con1 con1_tv_tys
-
-        -- Check that we're not dealing with a unidirectional pattern
-        -- synonym
-        ; checkTc (conLikeHasBuilder con1) $
-          nonBidirectionalErr (conLikeName con1)
-
-        -- STEP 3    Note [Criteria for update]
-        -- Check that each updated field is polymorphic; that is, its type
-        -- mentions only the universally-quantified variables of the data con
-        ; let flds1_w_tys  = zipEqual "tcExpr:RecConUpd" con1_flds con1_arg_tys
-              bad_upd_flds = filter bad_fld flds1_w_tys
-              con1_tv_set  = mkVarSet con1_tvs
-              bad_fld (fld, ty) = fld `elem` upd_fld_occs &&
-                                      not (tyCoVarsOfType ty `subVarSet` con1_tv_set)
-        ; checkTc (null bad_upd_flds) (TcRnFieldUpdateInvalidType bad_upd_flds)
-
-        -- 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
-        --
-        ; let fixed_tvs = getFixedTyVars upd_fld_occs con1_tvs relevant_cons
-              is_fixed_tv tv = tv `elemVarSet` fixed_tvs
-
-              mk_inst_ty :: TCvSubst -> (TyVar, TcType) -> TcM (TCvSubst, TcType)
-              -- Deals with instantiation of kind variables
-              --   c.f. GHC.Tc.Utils.TcMType.newMetaTyVars
-              mk_inst_ty subst (tv, result_inst_ty)
-                | is_fixed_tv tv   -- Same as result type
-                = return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
-                | otherwise        -- Fresh type, of correct kind
-                = do { (subst', new_tv) <- newMetaTyVarX subst tv
-                     ; return (subst', mkTyVarTy new_tv) }
-
-        ; (result_subst, con1_tvs') <- newMetaTyVars con1_tvs
-        ; let result_inst_tys = mkTyVarTys con1_tvs'
-              init_subst = mkEmptyTCvSubst (getTCvInScope result_subst)
-
-        ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty init_subst
-                                                      (con1_tvs `zip` result_inst_tys)
-
-        ; let rec_res_ty    = TcType.substTy result_subst con1_res_ty
-              scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
-              con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
-
-        ; co_scrut <- unifyType (Just . HsExprRnThing $ unLoc record_expr) record_rho scrut_ty
-                -- NB: normal unification is OK here (as opposed to subsumption),
-                -- because for this to work out, both record_rho and scrut_ty have
-                -- to be normal datatypes -- no contravariant stuff can go on
-
-        -- STEP 5
-        -- Typecheck the bindings
-        ; rbinds'      <- tcRecordUpd con1 con1_arg_tys' rbinds
-
-        -- STEP 6: Deal with the stupid theta.
-        -- See Note [The stupid context] in GHC.Core.DataCon.
-        ; let theta' = substThetaUnchecked scrut_subst (conLikeStupidTheta con1)
-        ; instStupidTheta RecordUpdOrigin theta'
-
-        -- Step 7: make a cast for the scrutinee, in the
-        --         case that it's from a data family
-        ; let fam_co :: HsWrapper   -- RepT t1 .. tn ~R scrut_ty
-              fam_co | Just tycon <- mtycon
-                     , Just co_con <- tyConFamilyCoercion_maybe tycon
-                     = mkWpCastR (mkTcUnbranchedAxInstCo co_con scrut_inst_tys [])
-                     | otherwise
-                     = idHsWrapper
-
-        -- Step 8: Check that the req constraints are satisfied
-        -- For normal data constructors req_theta is empty but we must do
-        -- this check for pattern synonyms.
-        ; let req_theta' = substThetaUnchecked scrut_subst req_theta
-        ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta'
-
-        -- Phew!
-        ; let upd_tc = RecordUpdTc { rupd_cons = relevant_cons
-                                   , rupd_in_tys = scrut_inst_tys
-                                   , rupd_out_tys = result_inst_tys
-                                   , rupd_wrap = req_wrap }
-              expr' = RecordUpd { rupd_expr = mkLHsWrap fam_co $
-                                                mkLHsWrapCo co_scrut record_expr'
-                                , rupd_flds = Left rbinds'
-                                , rupd_ext = upd_tc }
-
-        ; tcWrapResult expr expr' rec_res_ty res_ty }
-tcExpr (RecordUpd {}) _ = panic "GHC.Tc.Gen.Expr: tcExpr: The impossible happened!"
+            -- See Note [Unifying result types in tcRecordUpd].
+            -- Test case: T10808.
+        }
 
+tcExpr (RecordUpd {}) _ = panic "tcExpr: unexpected overloaded-dot RecordUpd"
 
 {-
 ************************************************************************
@@ -1163,33 +878,544 @@ in the other order, the extra signature in f2 is reqd.
 
 {- *********************************************************************
 *                                                                      *
-                 Record bindings
+                 Desugaring record update
 *                                                                      *
 ********************************************************************* -}
 
-getFixedTyVars :: [FieldLabelString] -> [TyVar] -> [ConLike] -> TyVarSet
--- These tyvars must not change across the updates
-getFixedTyVars upd_fld_occs univ_tvs cons
-      = mkVarSet [tv1 | con <- cons
-                      , let (u_tvs, _, eqspec, prov_theta
-                             , req_theta, arg_tys, _)
-                              = conLikeFullSig con
-                            theta = eqSpecPreds eqspec
-                                     ++ prov_theta
-                                     ++ req_theta
-                            flds = conLikeFieldLabels con
-                            fixed_tvs = exactTyCoVarsOfTypes (map scaledThing fixed_tys)
-                                    -- fixed_tys: See Note [Type of a record update]
-                                        `unionVarSet` tyCoVarsOfTypes theta
-                                    -- Universally-quantified tyvars that
-                                    -- appear in any of the *implicit*
-                                    -- arguments to the constructor are fixed
-                                    -- See Note [Implicit type sharing]
-
-                            fixed_tys = [ty | (fl, ty) <- zip flds arg_tys
-                                            , not (flLabel fl `elem` upd_fld_occs)]
-                      , (tv1,tv) <- univ_tvs `zip` u_tvs
-                      , tv `elemVarSet` fixed_tvs ]
+{-
+Note [Type of a record update]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The main complication with RecordUpd is that we need to explicitly
+handle the *non-updated* fields.  Consider:
+
+        data T a b c = MkT1 { fa :: a, fb :: (b,c) }
+                     | MkT2 { fa :: a, fb :: (b,c), fc :: c -> c }
+                     | MkT3 { fd :: a }
+
+        upd :: T a b c -> (b',c) -> T a b' c
+        upd t x = t { fb = x}
+
+The result type should be (T a b' c)
+not (T a b c),   because 'b' *is not* mentioned in a non-updated field
+not (T a b' c'), because 'c' *is*     mentioned in a non-updated field
+NB that it's not good enough to look at just one constructor; we must
+look at them all; cf #3219
+
+After all, 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).
+We call these the "fixed" type variables, and compute them in getFixedTyVars.
+
+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.
+Hence the use of 'relevant_cont'.
+
+Note [Implicit 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
+
+NB: this is not (quite) the same as being a "naughty" record selector
+(See Note [Naughty record selectors]) in GHC.Tc.TyCl), at least
+in the case of GADTs. Consider
+   data T a where { MkT :: { f :: a } :: T [a] }
+Then f is not "naughty" because it has a well-typed record selector.
+But we don't allow updates for 'f'.  (One could consider trying to
+allow this, but it makes my head hurt.  Badly.  And no one has asked
+for it.)
+
+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]
+
+Note [Mixed Record Field Updates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following pattern synonym.
+
+  data MyRec = MyRec { foo :: Int, qux :: String }
+
+  pattern HisRec{f1, f2} = MyRec{foo = f1, qux=f2}
+
+This allows updates such as the following
+
+  updater :: MyRec -> MyRec
+  updater a = a {f1 = 1 }
+
+It would also make sense to allow the following update (which we reject).
+
+  updater a = a {f1 = 1, qux = "two" } ==? MyRec 1 "two"
+
+This leads to confusing behaviour when the selectors in fact refer the same
+field.
+
+  updater a = a {f1 = 1, foo = 2} ==? ???
+
+For this reason, we reject a mixture of pattern synonym and normal record
+selectors in the same update block. Although of course we still allow the
+following.
+
+  updater a = (a {f1 = 1}) {foo = 2}
+
+  > updater (MyRec 0 "str")
+  MyRec 2 "str"
+
+Note [Record Updates]
+~~~~~~~~~~~~~~~~~~~~~
+To typecheck a record update, we desugar it first.  Suppose we have
+    data T p q = T1 { x :: Int, y :: Bool, z :: Char }
+               | T2 { v :: Char }
+               | T3 { x :: Int }
+               | T4 { p :: Float, y :: Bool, x :: Int }
+               | T5
+Then the record update `e { x=e1, y=e2 }` desugars as follows
+
+       e { x=e1, y=e2 }
+    ===>
+       let { x' = e1; y' = e2 } in
+       case e of
+          T1 _ _ z -> T1 x' y' z
+          T4 p _ _ -> T4 p y' x'
+T2, T3 and T5 should not occur, so we omit them from the match.
+The critical part of desugaring is to identify T and then T1/T4.
+
+Wrinkle [Disambiguating fields]
+As outlined above, to typecheck a record update via desugaring, we first need
+to identify the parent record `TyCon` (`T` above). This can be tricky when several
+record types share the same field (with `-XDuplicateRecordFields`).
+
+Currently, we use the inferred type of the record to help disambiguate the record
+fields. For example, in
+
+  ( mempty :: T a b ) { x = 3 }
+
+the type signature on `mempty` allows us to disambiguate the record `TyCon` to `T`,
+when there might be other datatypes with field `x :: Int`.
+This complexity is scheduled for removal via the implementation of GHC proposal #366
+https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0366-no-ambiguous-field-access.rst
+
+However, for the time being, we still need to disambiguate record fields using the
+inferred types. This means that, when typechecking a record update via desugaring,
+we need to do the following:
+
+  D1. Perform a first typechecking pass on the record expression (`e` in the example above),
+      to infer the type of the record being updated.
+  D2. Desugar the record update as described above, using an HsExpansion.
+  D3. Typecheck the desugared code.
+
+In (D1), we call inferRho to infer the type of the record being updated. This returns the
+inferred type of the record, together with a typechecked expression (of type HsExpr GhcTc)
+and a collection of residual constraints.
+We have no need for the latter two, because we will typecheck again in (D3). So, for
+the time being (and until GHC proposal #366 is implemented), we simply drop them.
+
+Wrinkle [Using IdSig]
+As noted above, we want to let-bind the updated fields to avoid code duplication:
+
+  let { x' = e1; y' = e2 } in
+  case e of
+     T1 _ _ z -> T1 x' y' z
+     T4 p _ _ -> T4 p y' x'
+
+However, doing so in a naive way would cause difficulties for type inference.
+For example:
+
+  data R b = MkR { f :: (forall a. a -> a) -> (Int,b), c :: Int }
+  foo r = r { f = \ k -> (k 3, k 'x') }
+
+If we desugar to:
+
+  ds_foo r =
+    let f' = \ k -> (k 3, k 'x')
+    in case r of
+      MkR _ b -> MkR f' b
+
+then we are unable to infer an appropriately polymorphic type for f', because we
+never infer higher-rank types. To circumvent this problem, we proceed as follows:
+
+  1. Obtain general field types by instantiating any of the constructors
+     that contain all the necessary fields. (Note that the field type must be
+     identical across different constructors of a given data constructor).
+  2. Let-bind an 'IdSig' with this type. This amounts to giving the let-bound
+     'Id's a partial type signature.
+
+In the above example, it's as if we wrote:
+
+  ds_foo r =
+    let f' :: (forall a. a -> a) -> (Int, _b)
+        f' = \ k -> (k 3, k 'x')
+    in case r of
+      MkR _ b -> MkR f' b
+
+This allows us to compute the right type for f', and thus accept this record update.
+
+Note [Unifying result types in tcRecordUpd]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+After desugaring 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 desugars 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.
+
+-}
+
+-- | Desugars a record update @record_expr { fld1 = e1, fld2 = e2}@ into a case expression
+-- that matches on the constructors of the record @r@, as described in
+-- Note [Record Updates].
+--
+-- Returns a renamed but not-yet-typechecked expression, together with the
+-- result type of this desugared record update.
+desugarRecordUpd :: LHsExpr GhcRn
+                      -- ^ @record_expr@: expression to which the record update is applied
+                 -> [LHsRecUpdField GhcRn]
+                      -- ^ the record update fields
+                 -> ExpRhoType
+                      -- ^ the expected result type of the record update
+                 -> TcM ( HsExpr GhcRn
+                           -- desugared record update expression
+                        , TcType
+                           -- result type of desugared record update
+                        , SDoc
+                           -- error context to push when typechecking
+                           -- the desugared code
+                        )
+desugarRecordUpd record_expr rbnds res_ty
+  = do {  -- STEP -2: typecheck the record_expr, the record to be updated
+          -- Until GHC proposal #366 is implemented, we still use the type of
+          -- the record to disambiguate its fields, so we must infer the record
+          -- type here before we can desugar. See Wrinkle [Disambiguating fields]
+          -- in Note [Record Updates].
+       ; ((_, record_rho), _lie) <- captureConstraints $  -- see (1) below
+                                    tcScalingUsage Many $ -- see (2) below
+                                    tcInferRho record_expr
+
+            -- (1)
+            -- Note that we capture, and then discard, the constraints.
+            -- This `tcInferRho` is used *only* to identify the data type,
+            -- so we can deal with field disambiguation.
+            -- Then we are going to generate a desugared record update, including `record_expr`,
+            -- and typecheck it from scratch.  We don't want to generate the constraints twice!
+
+            -- (2)
+            -- Record update drops some of the content of the record (namely the
+            -- content of the field being updated). As a consequence, unless the
+            -- field being updated is unrestricted in the record, we need an
+            -- unrestricted record. Currently, we simply always require an
+            -- unrestricted record.
+            --
+            -- Consider the following example:
+            --
+            -- data R a = R { self :: a }
+            -- bad :: a ⊸ ()
+            -- bad x = let r = R x in case r { self = () } of { R x' -> x' }
+            --
+            -- This should definitely *not* typecheck.
+
+       -- STEP -1  See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
+       -- After this we know that rbinds is unambiguous
+       ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty
+       ; let upd_flds = map (unLoc . hfbLHS . unLoc) rbinds
+             upd_fld_occs = map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc) upd_flds
+             sel_ids      = map selectorAmbiguousFieldOcc upd_flds
+             upd_fld_names = map idName sel_ids
+
+       -- STEP 0
+       -- Check that the field names are really field names
+       -- and they are all field names for proper records or
+       -- all field names for pattern synonyms.
+       ; let bad_guys = [ setSrcSpan loc $ addErrTc (notSelector fld_name)
+                        | fld <- rbinds,
+                          -- Excludes class ops
+                          let L loc sel_id = hsRecUpdFieldId (unLoc fld),
+                          not (isRecordSelector sel_id),
+                          let fld_name = idName sel_id ]
+       ; unless (null bad_guys) (sequence bad_guys >> failM)
+       -- See Note [Mixed Record Field Updates]
+       ; let (data_sels, pat_syn_sels) =
+               partition isDataConRecordSelector sel_ids
+       ; massert (all isPatSynRecordSelector pat_syn_sels)
+       ; checkTc ( null data_sels || null pat_syn_sels )
+                 ( mixedSelectors data_sels pat_syn_sels )
+
+       -- STEP 1
+       -- Figure out the tycon and data cons from the first field name
+       ; let   -- It's OK to use the non-tc splitters here (for a selector)
+             sel_id : _  = sel_ids
+             con_likes :: [ConLike]
+             con_likes = case idDetails sel_id of
+                            RecSelId (RecSelData tc) _
+                               -> map RealDataCon (tyConDataCons tc)
+                            RecSelId (RecSelPatSyn ps) _
+                               -> [PatSynCon ps]
+                            _  -> panic "tcRecordUpd"
+               -- NB: for a data type family, the tycon is the instance tycon
+             relevant_cons = conLikesWithFields con_likes upd_fld_occs
+               -- A constructor is only relevant to this process if
+               -- it contains *all* the fields that are being updated
+               -- Other ones will cause a runtime error if they occur
+
+       -- STEP 2
+       -- Check that at least one constructor has all the named fields
+       -- i.e. has an empty set of bad fields returned by badFields
+       ; case relevant_cons of
+         { [] -> failWithTc (badFieldsUpd rbinds con_likes)
+         ; relevant_con : _ ->
+
+      -- STEP 3
+      -- Create new variables for the fields we are updating,
+      -- so that we can share them across constructors.
+      --
+      -- Example:
+      --
+      --   e { x=e1, y=e2 }
+      --
+      -- We want to let-bind variables to `e1` and `e2`:
+      --
+      --   let x' :: Int
+      --       x' = e1
+      --       y' :: Bool
+      --       y' = e2
+      --   in ...
+
+    do { -- Instantiate the type variables of any relevant constuctor
+         -- with metavariables to obtain a type for each 'Id'.
+         -- This will allow us to have 'Id's with polymorphic types
+         -- by using 'IdSig'. See Wrinkle [Using IdSig] in Note [Record Updates].
+       ; let (univ_tvs, ex_tvs, eq_spec, _, _, arg_tys, con_res_ty) = conLikeFullSig relevant_con
+       ; (subst, tc_tvs) <- newMetaTyVars (univ_tvs ++ ex_tvs)
+       ; let (actual_univ_tys, _actual_ex_tys) = splitAtList univ_tvs $ map mkTyVarTy tc_tvs
+
+             -- See Wrinkle [GADT result type in tcRecordUpd]
+             -- for an explanation of the following.
+             ds_res_ty = case relevant_con of
+               RealDataCon con
+                 | not (null eq_spec) -- We only need to do this if we have actual GADT equalities.
+                 -> mkFamilyTyConApp (dataConTyCon con) actual_univ_tys
+               _ -> substTy subst con_res_ty
+
+       -- Gather pairs of let-bound Ids and their right-hand sides,
+       -- e.g. (x', e1), (y', e2), ...
+       ; let mk_upd_id :: Name -> LHsFieldBind GhcTc fld (LHsExpr GhcRn) -> TcM (Name, (TcId, LHsExpr GhcRn))
+             mk_upd_id fld_nm (L _ rbind)
+               = do { let Scaled m arg_ty = lookupNameEnv_NF arg_ty_env fld_nm
+                          nm_occ = rdrNameOcc . nameRdrName $ fld_nm
+                          actual_arg_ty = substTy subst arg_ty
+                          rhs = hfbRHS rbind
+                    ; (_co, actual_arg_ty) <- hasFixedRuntimeRep (FRRRecordUpdate fld_nm (unLoc rhs)) actual_arg_ty
+                      -- We get a better error message by doing a (redundant) representation-polymorphism check here,
+                      -- rather than delaying until the typechecker typechecks the let-bindings,
+                      -- because the let-bound Ids have internal names.
+                      -- (As we will typecheck the let-bindings later, we can drop this coercion here.)
+                      -- See RepPolyRecordUpdate test.
+                    ; nm <- newNameAt nm_occ generatedSrcSpan
+                    ; let id = mkLocalId nm m actual_arg_ty
+                      -- NB: create fresh names to avoid any accidental shadowing
+                      -- occuring in the RHS expressions when creating the let bindings:
+                      --
+                      --  let x1 = e1; x2 = e2; ...
+                    ; return (fld_nm, (id, rhs))
+                    }
+             arg_ty_env = mkNameEnv
+                        $ zipWith (\ lbl arg_ty -> (flSelector lbl, arg_ty))
+                            (conLikeFieldLabels relevant_con)
+                            arg_tys
+
+       ; upd_ids <- zipWithM mk_upd_id upd_fld_names rbinds
+       ; let updEnv :: UniqMap Name (Id, LHsExpr GhcRn)
+             updEnv = listToUniqMap $ upd_ids
+
+             make_pat :: ConLike -> LMatch GhcRn (LHsExpr GhcRn)
+             -- As explained in Note [Record Updates], to desugar
+             --
+             --   e { x=e1, y=e2 }
+             --
+             -- we generate a case statement, with an equation for
+             -- each constructor of the record. For example, for
+             -- the constructor
+             --
+             --   T1 :: { x :: Int, y :: Bool, z :: Char } -> T p q
+             --
+             -- we let-bind x' = e1, y' = e2 and generate the equation:
+             --
+             --   T1 _ _ z -> T1 x' y' z
+             make_pat conLike = mkSimpleMatch CaseAlt [pat] rhs
+               where
+                 (lhs_con_pats, rhs_con_args)
+                    = zipWithAndUnzip mk_con_arg [1..] con_fields
+                 pat = genSimpleConPat con lhs_con_pats
+                 rhs = wrapGenSpan $ genHsApps con rhs_con_args
+                 con = conLikeName conLike
+                 con_fields = conLikeFieldLabels conLike
+
+             mk_con_arg :: Int
+                        -> FieldLabel
+                        -> ( LPat GhcRn
+                              -- LHS constructor pattern argument
+                           , LHsExpr GhcRn )
+                              -- RHS constructor argument
+             mk_con_arg i fld_lbl =
+               -- The following generates the pattern matches of the desugared `case` expression.
+               -- For fields being updated (for example `x`, `y` in T1 and T4 in Note [Record Updates]),
+               -- wildcards are used to avoid creating unused variables.
+               case lookupUniqMap updEnv $ flSelector fld_lbl of
+                 -- Field is being updated: LHS = wildcard pattern, RHS = appropriate let-bound Id.
+                 Just (upd_id, _) -> (genWildPat, genLHsVar (idName upd_id))
+                 -- Field is not being updated: LHS = variable pattern, RHS = that same variable.
+                 _  -> let fld_nm = mkInternalName (mkBuiltinUnique i)
+                                      (mkVarOccFS (flLabel fld_lbl))
+                                      generatedSrcSpan
+                       in (genVarPat fld_nm, genLHsVar fld_nm)
+
+       -- STEP 4
+       -- Desugar to HsCase, as per note [Record Updates]
+       ; let ds_expr :: HsExpr GhcRn
+             ds_expr = HsLet noExtField noHsTok let_binds noHsTok (L gen case_expr)
+
+             case_expr :: HsExpr GhcRn
+             case_expr = HsCase noExtField record_expr (mkMatchGroup Generated (wrapGenSpan matches))
+             matches :: [LMatch GhcRn (LHsExpr GhcRn)]
+             matches = map make_pat relevant_cons
+
+             let_binds :: HsLocalBindsLR GhcRn GhcRn
+             let_binds = HsValBinds noAnn $ XValBindsLR
+                       $ NValBinds upd_ids_lhs (map mk_idSig upd_ids)
+             upd_ids_lhs :: [(RecFlag, LHsBindsLR GhcRn GhcRn)]
+             upd_ids_lhs = [ (NonRecursive, unitBag $ genSimpleFunBind (idName id) [] rhs)
+                           | (_, (id, rhs)) <- upd_ids ]
+             mk_idSig :: (Name, (Id, LHsExpr GhcRn)) -> LSig GhcRn
+             mk_idSig (_, (id, _)) = L gen $ IdSig noExtField id
+               -- We let-bind variables using 'IdSig' in order to accept
+               -- record updates involving higher-rank types.
+               -- See Wrinkle [Using IdSig] in Note [Record Updates].
+             gen = noAnnSrcSpan generatedSrcSpan
+
+        ; traceTc "desugarRecordUpd" $
+            vcat [ text "relevant_con:" <+> ppr relevant_con
+                 , text "res_ty:" <+> ppr res_ty
+                 , text "ds_res_ty:" <+> ppr ds_res_ty
+                 ]
+
+        ; let cons = pprQuotedList relevant_cons
+              err_lines =
+                (text "In a record update at field" <> plural upd_fld_names <+> pprQuotedList upd_fld_names :)
+                $ case relevant_con of
+                     RealDataCon con ->
+                        [ text "with type constructor" <+> quotes (ppr (dataConTyCon con))
+                        , text "data constructor" <+> plural relevant_cons <+> cons ]
+                     PatSynCon {} ->
+                        [ text "with pattern synonym" <+> plural relevant_cons <+> cons ]
+                ++ if null ex_tvs
+                   then []
+                   else [ text "existential variable" <> plural ex_tvs <+> pprQuotedList ex_tvs ]
+              err_ctxt = make_lines_msg err_lines
+
+        ; return (ds_expr, ds_res_ty, err_ctxt) } } }
+
+-- | Pretty-print a collection of lines, adding commas at the end of each line,
+-- and adding "and" to the start of the last line.
+make_lines_msg :: [SDoc] -> SDoc
+make_lines_msg []      = empty
+make_lines_msg [last]  = ppr last <> dot
+make_lines_msg [l1,l2] = l1 $$ text "and" <+> l2 <> dot
+make_lines_msg (l:ls)  = l <> comma $$ make_lines_msg ls
+
+{- *********************************************************************
+*                                                                      *
+                 Record bindings
+*                                                                      *
+********************************************************************* -}
 
 -- Disambiguate the fields in a record update.
 -- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
@@ -1350,34 +1576,6 @@ tcRecordBinds con_like arg_tys (HsRecFields rbinds dd)
                                                      , hfbRHS = rhs'
                                                      , hfbPun = hfbPun fld}))) }
 
-tcRecordUpd
-        :: ConLike
-        -> [TcType]     -- Expected type for each field
-        -> [LHsFieldBind GhcTc (LAmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)]
-        -> TcM [LHsRecUpdField GhcTc]
-
-tcRecordUpd con_like arg_tys rbinds = fmap catMaybes $ mapM do_bind rbinds
-  where
-    fields = map flSelector $ conLikeFieldLabels con_like
-    flds_w_tys = zipEqual "tcRecordUpd" fields arg_tys
-
-    do_bind :: LHsFieldBind GhcTc (LAmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)
-            -> TcM (Maybe (LHsRecUpdField GhcTc))
-    do_bind (L l fld@(HsFieldBind { hfbLHS = L loc af
-                                 , hfbRHS = rhs }))
-      = do { let lbl = rdrNameAmbiguousFieldOcc af
-                 sel_id = selectorAmbiguousFieldOcc af
-                 f = L loc (FieldOcc (idName sel_id) (L (l2l loc) lbl))
-           ; mb <- tcRecordField con_like flds_w_tys f rhs
-           ; case mb of
-               Nothing         -> return Nothing
-               Just (f', rhs') ->
-                 return (Just
-                         (L l (fld { hfbLHS
-                                      = L loc (Unambiguous
-                                               (foExt (unLoc f'))
-                                               (L (l2l loc) lbl))
-                                   , hfbRHS = rhs' }))) }
 
 tcRecordField :: ConLike -> Assoc Name Type
               -> LFieldOcc GhcRn -> LHsExpr GhcRn
@@ -1386,7 +1584,7 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs
   | Just field_ty <- assocMaybe flds_w_tys sel_name
       = addErrCtxt (fieldCtxt field_lbl) $
         do { rhs' <- tcCheckPolyExprNC rhs field_ty
-           ; hasFixedRuntimeRep_syntactic (FRRRecordUpdate (unLoc lbl) (unLoc rhs'))
+           ; hasFixedRuntimeRep_syntactic (FRRRecordCon (unLoc lbl) (unLoc rhs'))
                 field_ty
            ; let field_id = mkUserLocal (nameOccName sel_name)
                                         (nameUnique sel_name)
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index dfe332eb08..42704013a7 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -55,7 +55,6 @@ module GHC.Tc.Types.Evidence (
   mkTcKindCo,
   tcCoercionKind,
   mkTcCoVarCo,
-  mkTcFamilyTyConAppCo,
   isTcReflCo, isTcReflexiveCo,
   tcCoercionRole,
   unwrapIP, wrapIP,
@@ -158,7 +157,6 @@ mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
 mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
 mkTcKindCo             :: TcCoercion -> TcCoercionN
 mkTcCoVarCo            :: CoVar -> TcCoercion
-mkTcFamilyTyConAppCo   :: TyCon -> [TcCoercionN] -> TcCoercionN
 
 tcCoercionKind         :: TcCoercion -> Pair TcType
 tcCoercionRole         :: TcCoercion -> Role
@@ -195,7 +193,6 @@ mkTcCoherenceRightCo   = mkCoherenceRightCo
 mkTcPhantomCo          = mkPhantomCo
 mkTcKindCo             = mkKindCo
 mkTcCoVarCo            = mkCoVarCo
-mkTcFamilyTyConAppCo   = mkFamilyTyConAppCo
 
 tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index d088762270..8582d5c549 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -990,10 +990,14 @@ data FixedRuntimeRepOrigin
 -- 'FixedRuntimeRepOrigin' for that.
 data FixedRuntimeRepContext
 
+  -- | Record fields in record construction must have a fixed runtime
+  -- representation.
+  = FRRRecordCon !RdrName !(HsExpr GhcTc)
+
   -- | Record fields in record updates must have a fixed runtime representation.
   --
   -- Test case: RepPolyRecordUpdate.
-  = FRRRecordUpdate !RdrName !(HsExpr GhcTc)
+  | FRRRecordUpdate !Name !(HsExpr GhcRn)
 
   -- | Variable binders must have a fixed runtime representation.
   --
@@ -1090,6 +1094,9 @@ data FixedRuntimeRepContext
 -- which is not fixed. That information is stored in 'FixedRuntimeRepOrigin'
 -- and is reported separately.
 pprFixedRuntimeRepContext :: FixedRuntimeRepContext -> SDoc
+pprFixedRuntimeRepContext (FRRRecordCon lbl _arg)
+  = sep [ text "The field", quotes (ppr lbl)
+        , text "of the record constructor" ]
 pprFixedRuntimeRepContext (FRRRecordUpdate lbl _arg)
   = sep [ text "The record update at field"
         , quotes (ppr lbl) ]
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index eee43e8ed1..6fa47f8b64 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -857,32 +857,6 @@ zonkExpr env expr@(RecordCon { rcon_ext = con_expr, rcon_flds = rbinds })
         ; return (expr { rcon_ext  = new_con_expr
                        , rcon_flds = new_rbinds }) }
 
--- Record updates via dot syntax are replaced by desugared expressions
--- in the renamer. See Note [Rebindable syntax and HsExpansion]. This
--- is why we match on 'rupd_flds = Left rbinds' here and panic otherwise.
-zonkExpr env (RecordUpd { rupd_flds = Left rbinds
-                        , rupd_expr = expr
-                        , rupd_ext = RecordUpdTc {
-                                       rupd_cons = cons
-                                     , rupd_in_tys = in_tys
-                                     , rupd_out_tys = out_tys
-                                     , rupd_wrap = req_wrap }})
-  = do  { new_expr    <- zonkLExpr env expr
-        ; new_in_tys  <- mapM (zonkTcTypeToTypeX env) in_tys
-        ; new_out_tys <- mapM (zonkTcTypeToTypeX env) out_tys
-        ; new_rbinds  <- zonkRecUpdFields env rbinds
-        ; (_, new_recwrap) <- zonkCoFn env req_wrap
-        ; return (
-            RecordUpd {
-                  rupd_expr = new_expr
-                , rupd_flds = Left new_rbinds
-                , rupd_ext = RecordUpdTc {
-                               rupd_cons = cons
-                             , rupd_in_tys = new_in_tys
-                             , rupd_out_tys = new_out_tys
-                             , rupd_wrap = new_recwrap }}) }
-zonkExpr _ (RecordUpd {}) = panic "GHC.Tc.Utils.Zonk: zonkExpr: The impossible happened!"
-
 zonkExpr env (ExprWithTySig _ e ty)
   = do { e' <- zonkLExpr env e
        ; return (ExprWithTySig noExtField e' ty) }
@@ -1309,16 +1283,6 @@ zonkRecFields env (HsRecFields flds dd)
            ; return (L l (fld { hfbLHS = new_id
                               , hfbRHS = new_expr })) }
 
-zonkRecUpdFields :: ZonkEnv -> [LHsRecUpdField GhcTc]
-                 -> TcM [LHsRecUpdField GhcTc]
-zonkRecUpdFields env = mapM zonk_rbind
-  where
-    zonk_rbind (L l fld)
-      = do { new_id   <- wrapLocMA (zonkFieldOcc env) (hsRecUpdFieldOcc fld)
-           ; new_expr <- zonkLExpr env (hfbRHS fld)
-           ; return (L l (fld { hfbLHS = fmap ambiguousFieldOcc new_id
-                              , hfbRHS = new_expr })) }
-
 {-
 ************************************************************************
 *                                                                      *