diff options
Diffstat (limited to 'compiler/GHC/Tc/TyCl/Build.hs')
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Build.hs | 53 |
1 files changed, 47 insertions, 6 deletions
diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index 588f209377..1dba4093f1 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -79,6 +79,8 @@ mkNewTyConRhs tycon_name tycon con -- has a single argument (Foo a) that is a *type class*, so -- dataConInstOrigArgTys returns []. + -- Eta-reduce the newtype + -- See Note [Newtype eta] in GHC.Core.TyCon etad_tvs :: [TyVar] -- Matched lazily, so that mkNewTypeCo can etad_roles :: [Role] -- return a TyCon without pulling on rhs_ty etad_rhs :: Type -- See Note [Tricky iface loop] in GHC.Iface.Load @@ -89,12 +91,51 @@ mkNewTyConRhs tycon_name tycon con -> Type -- Rhs type -> ([TyVar], [Role], Type) -- Eta-reduced version -- (tyvars in normal order) - eta_reduce (a:as) (_:rs) ty | Just (fun, arg) <- splitAppTy_maybe ty, - Just tv <- getTyVar_maybe arg, - tv == a, - not (a `elemVarSet` tyCoVarsOfType fun) - = eta_reduce as rs fun - eta_reduce tvs rs ty = (reverse tvs, reverse rs, ty) + eta_reduce (a:as) (_:rs) ty + | Just (fun, arg) <- splitAppTy_maybe ty + , Just tv <- getTyVar_maybe arg + , tv == a + , not (a `elemVarSet` tyCoVarsOfType fun) + , typeKind fun `eqType` typeKind (mkTyConApp tycon (mkTyVarTys $ reverse as)) + -- Why this kind-check? See Note [Newtype eta and homogeneous axioms] + = eta_reduce as rs fun + eta_reduce as rs ty = (reverse as, reverse rs, ty) + +{- Note [Newtype eta and homogeneous axioms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When eta-reducing a newtype, we must be careful to make sure the axiom +is homogeneous. (That is, the two types related by the axiom must +have the same kind.) All known proofs of type safety for Core rely on +the homogeneity of axioms, so let's not monkey with that. + +It is easy to mistakenly make an inhomogeneous axiom (#19739): + type T :: forall (a :: Type) -> Type + newtype T a = MkT (Proxy a) + +Can we eta-reduce, thus? + axT :: T ~ Proxy + +No! Because + T :: forall a -> Type + Proxy :: Type -> Type + +This is inhomogeneous. Hence, we have an extra kind-check in eta_reduce, +to make sure the reducts have the same kind. This is simple, although +perhaps quadratic in complexity, if we eta-reduce many arguments (which +seems vanishingly unlikely in practice). But NB that the free-variable +check, which immediately precedes the kind check, is also potentially +quadratic. + +There are other ways we could do the check (discussion on #19739): + +* We could look at the sequence of binders on the newtype and on the + head of the representation type, and make sure the visibilities on + the binders match up. This is quite a bit more code, and the reasoning + is subtler. + +* We could, say, do the kind-check at the end and then backtrack until the + kinds match up. Hard to know whether that's more performant or not. +-} ------------------------------------------------------ buildDataCon :: FamInstEnvs |