diff options
Diffstat (limited to 'compiler/GHC/HsToCore/Expr.hs')
| -rw-r--r-- | compiler/GHC/HsToCore/Expr.hs | 115 |
1 files changed, 87 insertions, 28 deletions
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index 5f1aa24035..694b394c1c 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -45,6 +45,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Utils.Monad import GHC.Core.Type import GHC.Core.Multiplicity +import GHC.Core.Coercion( Coercion ) import GHC.Core import GHC.Core.Utils import GHC.Core.Make @@ -53,6 +54,7 @@ import GHC.Driver.Session import GHC.Types.CostCentre import GHC.Types.Id import GHC.Types.Id.Make +import GHC.Types.Var.Env import GHC.Unit.Module import GHC.Core.ConLike import GHC.Core.DataCon @@ -61,14 +63,12 @@ import GHC.Builtin.Types import GHC.Builtin.Names import GHC.Types.Basic import GHC.Data.Maybe -import GHC.Types.Var.Env import GHC.Types.SrcLoc import GHC.Utils.Misc import GHC.Data.Bag import GHC.Utils.Outputable as Outputable import GHC.Utils.Panic import GHC.Core.PatSyn - import Control.Monad {- @@ -618,13 +618,70 @@ Note [Update for GADTs] ~~~~~~~~~~~~~~~~~~~~~~~ Consider data T a b where - T1 :: { f1 :: a } -> T a Int + MkT :: { foo :: a } -> T a Int + + upd :: T s t -> s -> T s t + upd z y = z { foo = y} + +We need to get this: + $WMkT :: a -> T a Int + MkT :: (b ~# Int) => a -> T a b + + upd = /\s t. \(z::T s t) (y::s) -> + case z of + MkT (co :: t ~# Int) _ -> $WMkT @s y |> T (Refl s) (Sym co) -Then the wrapper function for T1 has type - $WT1 :: a -> T a Int -But if x::T a b, then - x { f1 = v } :: T a b (not T a Int!) -So we need to cast (T a Int) to (T a b). Sigh. +Note the final cast + T (Refl s) (Sym co) :: T s Int ~ T s t +which uses co, bound by the GADT match. This is the wrap_co coercion +in wrapped_rhs. How do we produce it? + +* Start with raw materials + tc, the tycon: T + univ_tvs, the universally quantified tyvars of MkT: a,b + NB: these are in 1-1 correspondence with the tyvars of tc + +* Form univ_cos, a coercion for each of tc's args: (Refl s) (Sym co) + We replaced + a by (Refl s) since 's' instantiates 'a' + b by (Sym co) since 'b' is in the data-con's EqSpec + +* Then form the coercion T (Refl s) (Sym co) + +It gets more complicated when data families are involved (#18809). +Consider + data family F x + data instance F (a,b) where + MkF :: { foo :: Int } -> F (Int,b) + + bar :: F (s,t) -> Int -> F (s,t) + bar z y = z { foo = y} + +We have + data R:FPair a b where + MkF :: { foo :: Int } -> R:FPair Int b + + $WMkF :: Int -> F (Int,b) + MkF :: forall a b. (a ~# Int) => Int -> R:FPair a b + + bar :: F (s,t) -> Int -> F (s,t) + bar = /\s t. \(z::F (s,t)) \(y::Int) -> + case z |> co1 of + MkF (co2::s ~# Int) _ -> $WMkF @t y |> co3 + +(Side note: here (z |> co1) is built by typechecking the scrutinee, so +we ignore it here. In general the scrutinee is an aribtrary expression.) + +The question is: what is co3, the cast for the RHS? + co3 :: F (Int,t) ~ F (s,t) +Again, we can construct it using co2, bound by the GADT match. +We do /exactly/ the same as the non-family case up to building +univ_cos. But that gives us + rep_tc: R:FPair + univ_cos: (Sym co2) (Refl t) +But then we use mkTcFamilyTyConAppCo to "lift" this to the coercion +we want, namely + F (Sym co2, Refl t) :: F (Int,t) ~ F (s,t) -} @@ -711,8 +768,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields dict_req_wrap <.> mkWpTyApps [ lookupTyVar out_subst tv `orElse` mkTyVarTy tv - | tv <- user_tvs - , not (tv `elemVarEnv` wrap_subst) ] + | tv <- user_tvs ] -- Be sure to use user_tvs (which may be ordered -- differently than `univ_tvs ++ ex_tvs) above. -- See Note [DataCon user type variable binders] @@ -723,27 +779,30 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields -- Note [Update for GADTs] wrapped_rhs = case con of - RealDataCon data_con -> - let - wrap_co = - mkTcTyConAppCo Nominal - (dataConTyCon data_con) - [ lookup tv ty - | (tv,ty) <- univ_tvs `zip` out_inst_tys ] - lookup univ_tv ty = - case lookupVarEnv wrap_subst univ_tv of - Just co' -> co' - Nothing -> mkTcReflCo Nominal ty - in if null eq_spec - then rhs - else mkLHsWrap (mkWpCastN wrap_co) rhs + RealDataCon data_con + | null eq_spec -> rhs + | otherwise -> mkLHsWrap (mkWpCastN wrap_co) rhs + -- This wrap is the punchline: Note [Update for GADTs] + where + rep_tc = dataConTyCon data_con + wrap_co = mkTcFamilyTyConAppCo rep_tc univ_cos + univ_cos = zipWithEqual "dsExpr:upd" mk_univ_co univ_tvs out_inst_tys + + mk_univ_co :: TyVar -- Universal tyvar from the DataCon + -> Type -- Corresponding instantiating type + -> Coercion + mk_univ_co univ_tv inst_ty + = case lookupVarEnv eq_spec_env univ_tv of + Just co -> co + Nothing -> mkTcNomReflCo inst_ty + + eq_spec_env :: VarEnv Coercion + eq_spec_env = mkVarEnv [ (eqSpecTyVar spec, mkTcSymCo (mkTcCoVarCo eqs_var)) + | (spec,eqs_var) <- zipEqual "dsExpr:upd2" eq_spec eqs_vars ] + -- eq_spec is always null for a PatSynCon PatSynCon _ -> rhs - wrap_subst = - mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var)) - | (spec, eq_var) <- eq_spec `zip` eqs_vars - , let tv = eqSpecTyVar spec ] req_wrap = dict_req_wrap <.> mkWpTyApps in_inst_tys |