[Git][ghc/ghc][master] Fix desugaring of record updates on data families
Marge Bot
gitlab at gitlab.haskell.org
Fri Oct 9 12:52:14 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
bfdccac6 by Simon Peyton Jones at 2020-10-09T08:52:07-04:00
Fix desugaring of record updates on data families
This fixes a long-standing bug in the desugaring of record
updates for data families, when the latter involves a GADT. It's
all explained in Note [Update for GADTs] in GHC.HsToCore.Expr.
Building the correct cast is surprisingly tricky, as that Note
explains.
Fixes #18809. The test case (in indexed-types/should_compile/T18809)
contains several examples that exercise the dark corners.
- - - - -
8 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/Tc/Types/Evidence.hs
- + testsuite/tests/indexed-types/should_compile/T18809.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,6 +41,7 @@ module GHC.Core.Coercion (
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo, castCoercionKind, castCoercionKindI,
+ mkFamilyTyConAppCo,
mkHeteroCoercionType,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -1528,6 +1529,27 @@ castCoercionKindI g h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
where (Pair t1 t2, r) = coercionKindRole g
+mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
+-- ^ Given a family instance 'TyCon' and its arg 'Coercion's, return the
+-- corresponding family 'Coercion'. E.g:
+--
+-- > data family T a
+-- > data instance T (Maybe b) = MkT b
+--
+-- Where the instance 'TyCon' is :RTL, so:
+--
+-- > mkFamilyTyConAppCo :RTL (co :: a ~# Int) = T (Maybe a) ~# T (Maybe Int)
+--
+-- cf. 'mkFamilyTyConApp'
+mkFamilyTyConAppCo tc cos
+ | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
+ , let tvs = tyConTyVars tc
+ fam_cos = ASSERT2( tvs `equalLength` cos, ppr tc <+> ppr cos )
+ map (liftCoSubstWith Nominal tvs cos) fam_tys
+ = mkTyConAppCo Nominal fam_tc fam_cos
+ | otherwise
+ = mkTyConAppCo Nominal tc cos
+
-- See note [Newtype coercions] in GHC.Core.TyCon
mkPiCos :: Role -> [Var] -> Coercion -> Coercion
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -581,6 +581,7 @@ variables:
purposes of TypeApplications, and as a consequence, they do not come equipped
with visibilities (that is, they are TyVars/TyCoVars instead of
TyCoVarBinders).
+
* dcUserTyVarBinders, for the type variables binders in the order in which they
originally arose in the user-written type signature. Their order *does* matter
for TypeApplications, so they are full TyVarBinders, complete with
@@ -601,10 +602,10 @@ dcExTyCoVars. That is, the tyvars in dcUserTyVarBinders are a permutation of
ordering, they in fact share the same type variables (with the same Uniques). We
sometimes refer to this as "the dcUserTyVarBinders invariant".
-dcUserTyVarBinders, as the name suggests, is the one that users will see most of
-the time. It's used when computing the type signature of a data constructor (see
-dataConWrapperType), and as a result, it's what matters from a TypeApplications
-perspective.
+dcUserTyVarBinders, as the name suggests, is the one that users will
+see most of the time. It's used when computing the type signature of a
+data constructor wrapper (see dataConWrapperType), and as a result,
+it's what matters from a TypeApplications perspective.
Note [The dcEqSpec domain invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -436,8 +436,8 @@ mkTvSubstPrs prs =
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv tyvars tys
| debugIsOn
- , not (all isTyVar tyvars)
- = pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys)
+ , not (all isTyVar tyvars && (tyvars `equalLength` tys))
+ = pprPanic "zipTyEnv" (ppr tyvars $$ ppr tys)
| otherwise
= ASSERT( all (not . isCoercionTy) tys )
zipToUFM tyvars tys
=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -577,8 +577,9 @@ data RecordUpdTc = RecordUpdTc
, rupd_in_tys :: [Type] -- Argument types of *input* record type
, rupd_out_tys :: [Type] -- and *output* record type
- -- The original type can be reconstructed
- -- with conLikeResTy
+ -- For a data family, these are the type args of the
+ -- /representation/ type constructor
+
, rupd_wrap :: HsWrapper -- See note [Record Update HsWrapper]
}
=====================================
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
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -48,6 +48,7 @@ module GHC.Tc.Types.Evidence (
mkTcKindCo,
tcCoercionKind,
mkTcCoVarCo,
+ mkTcFamilyTyConAppCo,
isTcReflCo, isTcReflexiveCo,
tcCoercionRole,
unwrapIP, wrapIP,
@@ -141,6 +142,7 @@ 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
@@ -174,6 +176,7 @@ mkTcCoherenceRightCo = mkCoherenceRightCo
mkTcPhantomCo = mkPhantomCo
mkTcKindCo = mkKindCo
mkTcCoVarCo = mkCoVarCo
+mkTcFamilyTyConAppCo = mkFamilyTyConAppCo
tcCoercionKind = coercionKind
tcCoercionRole = coercionRole
=====================================
testsuite/tests/indexed-types/should_compile/T18809.hs
=====================================
@@ -0,0 +1,33 @@
+{-# LANGUAGE GADTs, TypeFamilies #-}
+
+module T18809 where
+
+-- Ordinary
+data F2 s where
+ MkF2 :: { foo2 :: Int } -> F2 s
+
+bar2 :: F2 s -> Int -> F2 s
+bar2 z y = z { foo2 = y }
+
+-- GADT
+data F1 s where
+ MkF1 :: { foo1 :: Int } -> F1 Int
+
+bar1 :: F1 s -> Int -> F1 s
+bar1 z y = z { foo1 = y }
+
+-- Orinary data family
+data family F3 a
+data instance F3 (s,t) where
+ MkF2b :: { foo3 :: Int } -> F3 (s,t)
+
+bar3 :: F3 (s,t) -> Int -> F3 (s,t)
+bar3 z y = z {foo3 = y}
+
+-- GADT + data family
+data family F4 a
+data instance F4 (s,t) where
+ MkF2a :: { foo4 :: Int } -> F4 (Int,t)
+
+bar4 :: F4 (s,t) -> Int -> F4 (s,t)
+bar4 z y = z { foo4 = y}
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -296,3 +296,4 @@ test('T17056', normal, compile, [''])
test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
test('T17923', normal, compile, [''])
test('T18065', normal, compile, ['-O'])
+test('T18809', normal, compile, ['-O'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bfdccac6acce84e15292a454d12f4e0d87ef6f10
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bfdccac6acce84e15292a454d12f4e0d87ef6f10
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201009/eec6920f/attachment-0001.html>
More information about the ghc-commits
mailing list