diff options
| -rw-r--r-- | compiler/GHC/Core/TyCon.hs | 30 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Build.hs | 53 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 17 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T19739a.hs | 11 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T19739b.hs | 10 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T19739c.hs | 11 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T19739d.hs | 12 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/all.T | 4 |
8 files changed, 130 insertions, 18 deletions
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 56fe29cb7e..d972752e9a 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -1337,17 +1337,22 @@ Note [Newtype eta] ~~~~~~~~~~~~~~~~~~ Consider newtype Parser a = MkParser (IO a) deriving Monad -Are these two types equal (that is, does a coercion exist between them)? +Are these two types equal? That is, does a coercion exist between them? Monad Parser Monad IO -which we need to make the derived instance for Monad Parser. +(We need this coercion to make the derived instance for Monad Parser.) Well, yes. But to see that easily we eta-reduce the RHS type of -Parser, in this case to IO, so that even unsaturated applications -of Parser will work right. This eta reduction is done when the type -constructor is built, and cached in NewTyCon. +Parser, in this case to IO, so that even unsaturated applications of +Parser will work right. So instead of + axParser :: forall a. Parser a ~ IO a +we generate an eta-reduced axiom + axParser :: Parser ~ IO -Here's an example that I think showed up in practice +This eta reduction is done when the type constructor is built, in +GHC.Tc.TyCl.Build.mkNewTyConRhs, and cached in NewTyCon. + +Here's an example that I think showed up in practice. Source code: newtype T a = MkT [a] newtype Foo m = MkFoo (forall a. m a -> Int) @@ -1359,14 +1364,15 @@ Source code: w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x) After desugaring, and discarding the data constructors for the newtypes, -we get: - w2 = w1 `cast` Foo CoT -so the coercion tycon CoT must have - kind: T ~ [] - and arity: 0 +we would like to get: + w2 = w1 `cast` Foo axT -This eta-reduction is implemented in GHC.Tc.TyCl.Build.mkNewTyConRhs. +so that w2 and w1 share the same code. To do this, the coercion axiom +axT must have + kind: axT :: T ~ [] + and arity: 0 +See also Note [Newtype eta and homogeneous axioms] in GHC.Tc.TyCl.Build. ************************************************************************ * * 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 diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index fb83e99583..c5be699e13 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -1054,6 +1054,23 @@ however, so this Note aims to describe these subtleties: themselves. Heavy sigh. But not truly hard; that's what tcbVisibilities does. +* Happily, we don't need to worry about the possibility of + building an inhomogeneous axiom, described in GHC.Tc.TyCl.Build + Note [Newtype eta and homogeneous axioms]. For example + type F :: Type -> forall (b :: Type) -> Type + data family F a b + newtype instance F Int b = MkF (Proxy b) + we get a newtype, and a eta-reduced axiom connecting the data family + with the newtype: + type R:FIntb :: forall (b :: Type) -> Type + newtype R:FIntb b = MkF (Proxy b) + axiom Foo.D:R:FIntb0 :: F Int = Foo.R:FIntb + Now the subtleties of Note [Newtype eta and homogeneous axioms] are + dealt with by the newtype (via mkNewTyConRhs called in tcDataFamInstDecl) + while the axiom connecting F Int ~ R:FIntb is eta-reduced, but the + quantifer 'b' is derived from the original data family F, and so the + kinds will always match. + Note [Kind inference for data family instances] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GADT-style data type declaration, where I have used diff --git a/testsuite/tests/polykinds/T19739a.hs b/testsuite/tests/polykinds/T19739a.hs new file mode 100644 index 0000000000..55296b3197 --- /dev/null +++ b/testsuite/tests/polykinds/T19739a.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +type T :: forall (a :: Type) -> Constraint +class T a where + f :: Proxy a diff --git a/testsuite/tests/polykinds/T19739b.hs b/testsuite/tests/polykinds/T19739b.hs new file mode 100644 index 0000000000..e0377383da --- /dev/null +++ b/testsuite/tests/polykinds/T19739b.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +type T :: forall (a :: Type) -> Type +newtype T a = Mk (Proxy a) diff --git a/testsuite/tests/polykinds/T19739c.hs b/testsuite/tests/polykinds/T19739c.hs new file mode 100644 index 0000000000..331d1f74fd --- /dev/null +++ b/testsuite/tests/polykinds/T19739c.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +type T :: (forall (x :: Type) -> x) -> forall (a :: Type) -> Type +newtype T f a = MkT (f (Type -> Type) a) diff --git a/testsuite/tests/polykinds/T19739d.hs b/testsuite/tests/polykinds/T19739d.hs new file mode 100644 index 0000000000..e316abf620 --- /dev/null +++ b/testsuite/tests/polykinds/T19739d.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +module Foo where + +import Data.Kind +import Data.Proxy + +type F :: Type -> forall (a :: Type) -> Type +data family F a b +newtype instance F Int b = MkF (Proxy b) diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 581b065fa9..275281f527 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -236,3 +236,7 @@ test('T19093', normal, compile, ['']) test('T19094', normal, compile, ['']) test('T19250', normal, compile, ['']) test('T19522', normal, compile, ['']) +test('T19739a', normal, compile, ['']) +test('T19739b', normal, compile, ['']) +test('T19739c', normal, compile, ['']) +test('T19739d', normal, compile, ['']) |