- check_fields arg_tys
- = do { rbinds' <- tcRecordBinds data_con arg_tys rbinds
- ; mapM unBox arg_tys
- ; return rbinds' }
- -- The unBox ensures that all the boxes in arg_tys are indeed
- -- filled, which is the invariant expected by tcIdApp
-
- ; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty
-
- ; returnM (RecordCon (L loc (dataConWrapId data_con)) con_expr rbinds') }
-
--- The main complication with RecordUpd is that we need to explicitly
--- handle the *non-updated* fields. Consider:
---
--- 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
---
--- All this is done in STEP 4 below.
---
--- Note about GADTs
--- ~~~~~~~~~~~~~~~~
--- For record update we require that every constructor involved in the
--- update (i.e. that has all the specified fields) is "vanilla". I
--- don't know how to do the update otherwise.
-
-
-tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty
- = -- STEP 0
+ (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity
+ con_id = dataConWrapId data_con
+
+ ; co_res <- unifyType actual_res_ty res_ty
+ ; rbinds' <- tcRecordBinds data_con arg_tys rbinds
+ ; return $ mkHsWrapCoI co_res $
+ RecordCon (L loc con_id) con_expr rbinds' }
+\end{code}
+
+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'), becuase '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 Trac #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 [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
+
+NB: this is not (quite) the same as being a "naughty" record selector
+(See Note [Naughty record selectors]) in TcTyClsDecls), 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]
+
+\begin{code}
+tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
+ = ASSERT( notNull upd_fld_names )
+ do {
+ -- STEP 0