Commit bfdccac6 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

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.
parent dfaef1ca
......@@ -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
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
......
......@@ -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]
}
......
......@@ -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
......
......@@ -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
......
{-# 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}
......@@ -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'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment