Make typeToLHsType produce kind signatures for tycon applications
authorRyan Scott <ryan.gl.scott@gmail.com>
Thu, 4 Jan 2018 01:11:31 +0000 (20:11 -0500)
committerBen Gamari <ben@smart-cactus.org>
Fri, 12 Jan 2018 20:19:25 +0000 (15:19 -0500)
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

(cherry picked from commit 649e777211fe08432900093002547d7358f92d82)

compiler/hsSyn/HsUtils.hs
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/deriving/should_compile/T14579.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/all.T

index db4507b..0d14478 100644 (file)
@@ -123,6 +123,7 @@ import Util
 import Bag
 import Outputable
 import Constants
+import TyCon
 
 import Data.Either
 import Data.Function
@@ -642,9 +643,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)
 
@@ -655,6 +662,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.
+-}
 
 {- *********************************************************************
 *                                                                      *
index e4230ad..63375ae 100644 (file)
@@ -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
diff --git a/testsuite/tests/deriving/should_compile/T14579.hs b/testsuite/tests/deriving/should_compile/T14579.hs
new file mode 100644 (file)
index 0000000..1945244
--- /dev/null
@@ -0,0 +1,12 @@
+{-# 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
index af9a577..8752bbd 100644 (file)
@@ -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, [''])