Commit 649e7772 authored by Ryan Scott's avatar Ryan Scott
Browse files

Make typeToLHsType produce kind signatures for tycon applications

Summary:
`GeneralizedNewtypeDeriving` generates calls to `coerce`
which take visible type arguments. These types must be produced by
way of `typeToLHsType`, which converts a `Type` to an `LHsType`.
However, `typeToLHsType` was leaving off important kind information
when a `Type` contained a poly-kinded tycon application, leading to
incorrectly generated code in #14579.

This fixes the issue by tweaking `typeToLHsType` to generate
explicit kind signatures for tycon applications. This makes the
generated code noisier, but at least the program from #14579 now
works correctly.

Test Plan: make test TEST=T14579

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14579

Differential Revision: https://phabricator.haskell.org/D4264
parent 7a25659e
......@@ -122,6 +122,7 @@ import Util
import Bag
import Outputable
import Constants
import TyCon
import Data.Either
import Data.Function
......@@ -641,9 +642,15 @@ typeToLHsType ty
go (AppTy t1 t2) = nlHsAppTy (go t1) (go t2)
go (LitTy (NumTyLit n)) = noLoc $ HsTyLit (HsNumTy noSourceText n)
go (LitTy (StrTyLit s)) = noLoc $ HsTyLit (HsStrTy noSourceText s)
go (TyConApp tc args) = nlHsTyConApp (getRdrName tc) (map go args')
go ty@(TyConApp tc args)
| any isInvisibleTyConBinder (tyConBinders tc)
-- We must produce an explicit kind signature here to make certain
-- programs kind-check. See Note [Kind signatures in typeToLHsType].
= noLoc $ HsKindSig lhs_ty (go (typeKind ty))
| otherwise = lhs_ty
where
args' = filterOutInvisibleTypes tc args
lhs_ty = nlHsTyConApp (getRdrName tc) (map go args')
args' = filterOutInvisibleTypes tc args
go (CastTy ty _) = go ty
go (CoercionTy co) = pprPanic "toLHsSigWcType" (ppr co)
......@@ -654,6 +661,55 @@ typeToLHsType ty
go_tv tv = noLoc $ KindedTyVar (noLoc (getRdrName tv))
(go (tyVarKind tv))
{-
Note [Kind signatures in typeToLHsType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are types that typeToLHsType can produce which require explicit kind
signatures in order to kind-check. Here is an example from Trac #14579:
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq
newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a)) deriving Eq
The derived Eq instance for Glurp (without any kind signatures) would be:
instance Eq a => Eq (Glurp a) where
(==) = coerce @(Wat 'Proxy -> Wat 'Proxy -> Bool)
@(Glurp a -> Glurp a -> Bool)
(==)
(Where the visible type applications use types produced by typeToLHsType.)
The type 'Proxy has an underspecified kind, so we must ensure that
typeToLHsType ascribes it with its kind: ('Proxy :: Proxy a).
We must be careful not to produce too many kind signatures, or else
typeToLHsType can produce noisy types like
('Proxy :: Proxy (a :: (Type :: Type))). In pursuit of this goal, we adopt the
following criterion for choosing when to annotate types with kinds:
* If there is a tycon application with any invisible arguments, annotate
the tycon application with its kind.
Why is this the right criterion? The problem we encountered earlier was the
result of an invisible argument (the `a` in ('Proxy :: Proxy a)) being
underspecified, so producing a kind signature for 'Proxy will catch this.
If there are no invisible arguments, then there is nothing to do, so we can
avoid polluting the result type with redundant noise.
What about a more complicated tycon, such as this?
T :: forall {j} (a :: j). a -> Type
Unlike in the previous 'Proxy example, annotating an application of `T` to an
argument (e.g., annotating T ty to obtain (T ty :: Type)) will not fix
its invisible argument `j`. But because we apply this strategy recursively,
`j` will be fixed because the kind of `ty` will be fixed! That is to say,
something to the effect of (T (ty :: j) :: Type) will be produced.
This strategy certainly isn't foolproof, as tycons that contain type families
in their kind might break down. But we'd likely need visible kind application
to make those work.
-}
{- *********************************************************************
* *
......
......@@ -73,15 +73,20 @@ Derived class instances:
GHC.Base.Semigroup (T14578.Wat f g a) where
(GHC.Base.<>)
= GHC.Prim.coerce
@(T14578.App (Data.Functor.Compose.Compose f g) a
-> T14578.App (Data.Functor.Compose.Compose f g) a
-> T14578.App (Data.Functor.Compose.Compose f g) a)
@(T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a
-> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a
-> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a)
@(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
(GHC.Base.<>)
GHC.Base.sconcat
= GHC.Prim.coerce
@(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g) a)
-> T14578.App (Data.Functor.Compose.Compose f g) a)
@(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a)
-> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a)
@(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
GHC.Base.sconcat
GHC.Base.stimes
......@@ -89,8 +94,10 @@ Derived class instances:
@(forall (b :: TYPE GHC.Types.LiftedRep).
GHC.Real.Integral b =>
b
-> T14578.App (Data.Functor.Compose.Compose f g) a
-> T14578.App (Data.Functor.Compose.Compose f g) a)
-> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a
-> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
-> TYPE GHC.Types.LiftedRep) a)
@(forall (b :: TYPE GHC.Types.LiftedRep).
GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a)
GHC.Base.stimes
......
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
module T14579 where
import Data.Kind
import Data.Proxy
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
deriving Eq
newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))
deriving Eq
......@@ -99,3 +99,4 @@ test('T14094', normal, compile, [''])
test('T14339', normal, compile, [''])
test('T14331', normal, compile, [''])
test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
test('T14579', normal, compile, [''])
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