Fix #14579 by defining tyConAppNeedsKindSig, and using it
authorRyan Scott <ryan.gl.scott@gmail.com>
Wed, 6 Feb 2019 00:57:29 +0000 (19:57 -0500)
committerRyan Scott <ryan.gl.scott@gmail.com>
Wed, 6 Feb 2019 00:57:29 +0000 (19:57 -0500)
compiler/hsSyn/HsUtils.hs
compiler/typecheck/TcSplice.hs
compiler/types/TyCoRep.hs
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/deriving/should_compile/T14579.stderr [new file with mode: 0644]
testsuite/tests/deriving/should_compile/T14579b.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/all.T
testsuite/tests/deriving/should_fail/T15073.stderr
utils/haddock

index febd5ac..dfb0ebf 100644 (file)
@@ -57,7 +57,7 @@ module HsUtils(
   -- Types
   mkHsAppTy, mkHsAppKindTy, userHsTyVarBndrs, userHsLTyVarBndrs,
   mkLHsSigType, mkLHsSigWcType, mkClassOpSigs, mkHsSigEnv,
-  nlHsAppTy, nlHsTyVar, nlHsFunTy, nlHsParTy, nlHsTyConApp,
+  nlHsAppTy, nlHsAppKindTy, nlHsTyVar, nlHsFunTy, nlHsParTy, nlHsTyConApp,
 
   -- Stmts
   mkTransformStmt, mkTransformByStmt, mkBodyStmt, mkBindStmt, mkTcBindStmt,
@@ -105,14 +105,14 @@ import TcEvidence
 import RdrName
 import Var
 import TyCoRep
-import Type   ( filterOutInvisibleTypes )
+import Type   ( tyConArgFlags )
 import TysWiredIn ( unitTy )
 import TcType
 import DataCon
 import ConLike
 import Id
 import Name
-import NameSet
+import NameSet hiding ( unitFV )
 import NameEnv
 import BasicTypes
 import SrcLoc
@@ -121,7 +121,6 @@ import Util
 import Bag
 import Outputable
 import Constants
-import TyCon
 
 import Data.Either
 import Data.Function
@@ -501,6 +500,10 @@ nlHsParTy t   = noLoc (HsParTy noExt t)
 nlHsTyConApp :: IdP (GhcPass p) -> [LHsType (GhcPass p)] -> LHsType (GhcPass p)
 nlHsTyConApp tycon tys  = foldl' nlHsAppTy (nlHsTyVar tycon) tys
 
+nlHsAppKindTy ::
+  LHsType (GhcPass p) -> LHsKind (GhcPass p) -> LHsType (GhcPass p)
+nlHsAppKindTy f k = noLoc (HsAppKindTy noExt f (parenthesizeHsType appPrec k))
+
 {-
 Tuples.  All these functions are *pre-typechecker* because they lack
 types on the tuple.
@@ -660,14 +663,24 @@ typeToLHsType ty
     go (LitTy (StrTyLit s))
       = noLoc $ HsTyLit NoExt (HsStrTy NoSourceText s)
     go ty@(TyConApp tc args)
-      | any isInvisibleTyConBinder (tyConBinders tc)
+      | tyConAppNeedsKindSig True tc (length args)
         -- We must produce an explicit kind signature here to make certain
         -- programs kind-check. See Note [Kind signatures in typeToLHsType].
       = nlHsParTy $ noLoc $ HsKindSig NoExt lhs_ty (go (typeKind ty))
       | otherwise = lhs_ty
        where
-        lhs_ty = nlHsTyConApp (getRdrName tc) (map go args')
-        args'  = filterOutInvisibleTypes tc args
+        arg_flags :: [ArgFlag]
+        arg_flags = tyConArgFlags tc args
+
+        lhs_ty :: LHsType GhcPs
+        lhs_ty = foldl' (\f (arg, flag) ->
+                          let arg' = go arg in
+                          case flag of
+                            Inferred  -> f
+                            Specified -> f `nlHsAppKindTy` arg'
+                            Required  -> f `nlHsAppTy`     arg')
+                        (nlHsTyVar (getRdrName tc))
+                        (zip args arg_flags)
     go (CastTy ty _)        = go ty
     go (CoercionTy co)      = pprPanic "toLHsSigWcType" (ppr co)
 
@@ -684,48 +697,40 @@ 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
+  -- type P :: forall {k} {t :: k}. Proxy t
+  type P = 'Proxy
+
+  -- type Wat :: forall a. Proxy a -> *
+  newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
+    deriving Eq
+
+  -- type Wat2 :: forall {a}. Proxy a -> *
+  type Wat2 = Wat
+
+  -- type Glurp :: * -> *
+  newtype Glurp a = MkGlurp (Wat2 (P :: 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)
+    (==) = coerce @(Wat2 P  -> Wat2 P  -> Bool)
+                  @(Glurp a -> Glurp a -> 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.
+The type P (in Wat2 P) has an underspecified kind, so we must ensure that
+typeToLHsType ascribes it with its kind: Wat2 (P :: Proxy a). To accomplish
+this, whenever we see an application of a tycon to some arguments, we use
+the tyConAppNeedsKindSig function to determine if it requires an explicit kind
+signature to resolve some ambiguity. (See Note
+Note [When does a tycon application need an explicit kind signature?] for a
+more detailed explanation of how this works.)
+
+Note that we pass True to tyConAppNeedsKindSig since we are generated code with
+visible kind applications, so even specified arguments count towards injective
+positions in the kind of the tycon.
 -}
 
 {- *********************************************************************
index 1bb844a..548dc72 100644 (file)
@@ -57,7 +57,6 @@ import GHCi
 import HscMain
         -- These imports are the reason that TcSplice
         -- is very high up the module hierarchy
-import FV
 import RnSplice( traceSplice, SpliceInfo(..))
 import RdrName
 import HscTypes
@@ -1890,109 +1889,12 @@ reifyTyVarsToMaybe :: [TyVar] -> TcM (Maybe [TH.TyVarBndr])
 reifyTyVarsToMaybe []  = pure Nothing
 reifyTyVarsToMaybe tys = Just <$> reifyTyVars tys
 
-{-
-Note [Kind annotations on TyConApps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A poly-kinded tycon sometimes needs a kind annotation to be unambiguous.
-For example:
-
-   type family F a :: k
-   type instance F Int  = (Proxy :: * -> *)
-   type instance F Bool = (Proxy :: (* -> *) -> *)
-
-It's hard to figure out where these annotations should appear, so we do this:
-Suppose we have a tycon application (T ty1 ... tyn). Assuming that T is not
-oversatured (more on this later), we can assume T's declaration is of the form
-T (tvb1 :: s1) ... (tvbn :: sn) :: p. If any kind variable that
-is free in p is not free in an injective position in tvb1 ... tvbn,
-then we put on a kind annotation, since we would not otherwise be able to infer
-the kind of the whole tycon application.
-
-The injective positions in a tyvar binder are the injective positions in the
-kind of its tyvar, provided the tyvar binder is either:
-
-* Anonymous. For example, in the promoted data constructor '(:):
-
-    '(:) :: forall a. a -> [a] -> [a]
-
-  The second and third tyvar binders (of kinds `a` and `[a]`) are both
-  anonymous, so if we had '(:) 'True '[], then the inferred kinds of 'True and
-  '[] would contribute to the inferred kind of '(:) 'True '[].
-* Has required visibility. For example, in the type family:
-
-    type family Wurble k (a :: k) :: k
-    Wurble :: forall k -> k -> k
-
-  The first tyvar binder (of kind `forall k`) has required visibility, so if
-  we had Wurble (Maybe a) Nothing, then the inferred kind of Maybe a would
-  contribute to the inferred kind of Wurble (Maybe a) Nothing.
-
-An injective position in a type is one that does not occur as an argument to
-a non-injective type constructor (e.g., non-injective type families). See
-injectiveVarsOfType.
-
-How can be sure that this is correct? That is, how can we be sure that in the
-event that we leave off a kind annotation, that one could infer the kind of the
-tycon application from its arguments? It's essentially a proof by induction: if
-we can infer the kinds of every subtree of a type, then the whole tycon
-application will have an inferrable kind--unless, of course, the remainder of
-the tycon application's kind has uninstantiated kind variables.
-
-An earlier implementation of this algorithm only checked if p contained any
-free variables. But this was unsatisfactory, since a datatype like this:
-
-  data Foo = Foo (Proxy '[False, True])
-
-Would be reified like this:
-
-  data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool])
-                                     :: [Bool]) :: [Bool]))
-
-Which has a rather excessive amount of kind annotations. With the current
-algorithm, we instead reify Foo to this:
-
-  data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool]))))
-
-Since in the case of '[], the kind p is [a], and there are no arguments in the
-kind of '[]. On the other hand, in the case of '(:) True '[], the kind p is
-(forall a. [a]), but a occurs free in the first and second arguments of the
-full kind of '(:), which is (forall a. a -> [a] -> [a]). (See Trac #14060.)
-
-What happens if T is oversaturated? That is, if T's kind has fewer than n
-arguments, in the case that the concrete application instantiates a result
-kind variable with an arrow kind? If we run out of arguments, we do not attach
-a kind annotation. This should be a rare case, indeed. Here is an example:
-
-   data T1 :: k1 -> k2 -> *
-   data T2 :: k1 -> k2 -> *
-
-   type family G (a :: k) :: k
-   type instance G T1 = T2
-
-   type instance F Char = (G T1 Bool :: (* -> *) -> *)   -- F from above
-
-Here G's kind is (forall k. k -> k), and the desugared RHS of that last
-instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to
-the algorithm above, there are 3 arguments to G so we should peel off 3
-arguments in G's kind. But G's kind has only two arguments. This is the
-rare special case, and we choose not to annotate the application of G with
-a kind signature. After all, we needn't do this, since that instance would
-be reified as:
-
-   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
-
-So the kind of G isn't ambiguous anymore due to the explicit kind annotation
-on its argument. See #8953 and test th/T8953.
--}
-
 reify_tc_app :: TyCon -> [Type.Type] -> TcM TH.Type
 reify_tc_app tc tys
   = do { tys' <- reifyTypes (filterOutInvisibleTypes tc tys)
        ; maybe_sig_t (mkThAppTs r_tc tys') }
   where
     arity       = tyConArity tc
-    tc_binders  = tyConBinders tc
-    tc_res_kind = tyConResKind tc
 
     r_tc | isUnboxedSumTyCon tc           = TH.UnboxedSumT (arity `div` 2)
          | isUnboxedTupleTyCon tc         = TH.UnboxedTupleT (arity `div` 2)
@@ -2013,28 +1915,20 @@ reify_tc_app tc tys
          | isPromotedDataCon tc           = TH.PromotedT (reifyName tc)
          | otherwise                      = TH.ConT (reifyName tc)
 
-    -- See Note [Kind annotations on TyConApps]
+    -- See Note [When does a tycon application need an explicit kind
+    -- signature?] in TyCoRep
     maybe_sig_t th_type
-      | needs_kind_sig
+      | tyConAppNeedsKindSig
+          False -- We don't reify types using visible kind applications, so
+                -- don't count specified binders as contributing towards
+                -- injective positions in the kind of the tycon.
+          tc (length tys)
       = do { let full_kind = tcTypeKind (mkTyConApp tc tys)
            ; th_full_kind <- reifyKind full_kind
            ; return (TH.SigT th_type th_full_kind) }
       | otherwise
       = return th_type
 
-    needs_kind_sig
-      | GT <- compareLength tys tc_binders
-      = False
-      | otherwise
-      = let (dropped_binders, remaining_binders)
-              = splitAtList  tys tc_binders
-            result_kind  = mkTyConKind remaining_binders tc_res_kind
-            result_vars  = tyCoVarsOfType result_kind
-            dropped_vars = fvVarSet $
-                           mapUnionFV injectiveVarsOfBinder dropped_binders
-
-        in not (subVarSet result_vars dropped_vars)
-
 ------------------------------
 reifyName :: NamedThing n => n -> TH.Name
 reifyName thing
index 075d270..f7c21b7 100644 (file)
@@ -90,7 +90,7 @@ module TyCoRep (
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList, tyCoVarsOfProv,
         almostDevoidCoVarOfCo,
-        injectiveVarsOfBinder, injectiveVarsOfType,
+        injectiveVarsOfType, tyConAppNeedsKindSig,
 
         noFreeVarsOfType, noFreeVarsOfCo,
 
@@ -2103,20 +2103,21 @@ almost_devoid_co_var_of_types (ty:tys) cv
 
 ------------- Injective free vars -----------------
 
--- | Returns the free variables of a 'TyConBinder' that are in injective
--- positions. (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an
--- explanation of what an injective position is.)
-injectiveVarsOfBinder :: TyConBinder -> FV
-injectiveVarsOfBinder (Bndr tv vis) =
-  case vis of
-    AnonTCB           -> injectiveVarsOfType (varType tv)
-    NamedTCB Required -> unitFV tv `unionFV`
-                         injectiveVarsOfType (varType tv)
-    NamedTCB _        -> emptyFV
-
 -- | Returns the free variables of a 'Type' that are in injective positions.
--- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation
--- of what an injective position is.)
+-- For example, if @F@ is a non-injective type family, then:
+--
+-- @
+-- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
+-- @
+--
+-- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
+-- More formally, if
+-- @a@ is in @'injectiveVarsOfType' ty@
+-- and  @S1(ty) ~ S2(ty)@,
+-- then @S1(a)  ~ S2(a)@,
+-- where @S1@ and @S2@ are arbitrary substitutions.
+--
+-- See @Note [When does a tycon application need an explicit kind signature?]@.
 injectiveVarsOfType :: Type -> FV
 injectiveVarsOfType = go
   where
@@ -2132,12 +2133,284 @@ injectiveVarsOfType = go
                          filterByList (inj ++ repeat True) tys
                          -- Oversaturated arguments to a tycon are
                          -- always injective, hence the repeat True
-    go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go (binderType tvb)
-                                             `unionFV` go ty
+    go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty
     go LitTy{}           = emptyFV
     go (CastTy ty _)     = go ty
     go CoercionTy{}      = emptyFV
 
+-- | Does a 'TyCon' (that is applied to some number of arguments) need to be
+-- ascribed with an explicit kind signature to resolve ambiguity if rendered as
+-- a source-syntax type?
+-- (See @Note [When does a tycon application need an explicit kind signature?]@
+-- for a full explanation of what this function checks for.)
+
+-- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but
+-- accomplishing this requires a fair deal of futzing aruond with .hs-boot
+-- files.
+tyConAppNeedsKindSig
+  :: Bool  -- ^ Should specified binders count towards injective positions in
+           --   the kind of the TyCon?
+  -> TyCon
+  -> Int   -- ^ The number of args the 'TyCon' is applied to.
+  -> Bool  -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
+           --   number of arguments)
+tyConAppNeedsKindSig spec_inj_pos tc n_args
+  | LT <- listLengthCmp tc_binders n_args
+  = False
+  | otherwise
+  = let (dropped_binders, remaining_binders)
+          = splitAt n_args tc_binders
+        result_kind  = mkTyConKind remaining_binders tc_res_kind
+        result_vars  = tyCoVarsOfType result_kind
+        dropped_vars = fvVarSet $
+                       mapUnionFV (injective_vars_of_binder spec_inj_pos)
+                                  dropped_binders
+
+    in not (subVarSet result_vars dropped_vars)
+  where
+    tc_binders  = tyConBinders tc
+    tc_res_kind = tyConResKind tc
+
+    -- Returns the variables that would be fixed by knowing a TyConBinder. See
+    -- Note [When does a tycon application need an explicit kind signature?]
+    -- for a more detailed explanation of what this function does.
+    injective_vars_of_binder
+      :: Bool -- Should specified binders count towards injective positions?
+              -- (If you're using visible kind applications, then you want True
+              -- here.)
+      -> TyConBinder -> FV
+    injective_vars_of_binder spec_inj_pos (Bndr tv vis) =
+      case vis of
+        AnonTCB -> injectiveVarsOfType (varType tv)
+        NamedTCB argf
+          |     (argf == Required)
+             || (spec_inj_pos && (argf == Specified))
+          -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
+          |  otherwise
+          -> emptyFV
+
+{-
+Note [When does a tycon application need an explicit kind signature?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are a couple of places in GHC where we convert Core Types into forms that
+more closely resemble user-written syntax. These include:
+
+1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app)
+2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock)
+
+This conversion presents a challenge: how do we ensure that the resulting type
+has enough kind information so as not to be ambiguous? To better motivate this
+question, consider the following Core type:
+
+  -- Foo :: Type -> Type
+  type Foo = Proxy Type
+
+There is nothing ambiguous about the RHS of Foo in Core. But if we were to,
+say, reify it into a TH Type, then it's tempting to just drop the invisible
+Type argument and simply return `Proxy`. But now we've lost crucial kind
+information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool`
+or `Proxy Int` or something else! We've inadvertently introduced ambiguity.
+
+Unlike in other situations in GHC, we can't just turn on
+-fprint-explicit-kinds, as we need to produce something which has the same
+structure as a source-syntax type. Moreover, we can't rely on visible kind
+application, since the first kind argument to Proxy is inferred, not specified.
+Our solution is to annotate certain tycons with their kinds whenever they
+appear in applied form in order to resolve the ambiguity. For instance, we
+would reify the RHS of Foo like so:
+
+  type Foo = (Proxy :: Type -> Type)
+
+We need to devise an algorithm that determines precisely which tycons need
+these explicit kind signatures. We certainly don't want to annotate _every_
+tycon with a kind signature, or else we might end up with horribly bloated
+types like the following:
+
+  (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type)
+
+We only want to annotate tycons that absolutely require kind signatures in
+order to resolve some sort of ambiguity, and nothing more.
+
+Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type
+require a kind signature? It might require it when we need to fill in any of
+T's omitted arguments. By "omitted argument", we mean one that is dropped when
+reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
+specified arguments (e.g., TH reification in TcSplice), and sometimes the
+omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType,
+which reifies specified arguments through visible kind application).
+Regardless, the key idea is that _some_ arguments are going to be omitted after
+reification, and the only mechanism we have at our disposal for filling them in
+is through explicit kind signatures.
+
+What do we mean by "fill in"? Let's consider this small example:
+
+  T :: forall {k}. Type -> (k -> Type) -> k
+
+Moreover, we have this application of T:
+
+  T @{j} Int aty
+
+When we reify this type, we omit the inferred argument @{j}. Is it fixed by the
+other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then
+we'll generate an equality constraint (kappa -> Type) and, assuming we can
+solve it, that will fix `kappa`. (Here, `kappa` is the unification variable
+that we instantiate `k` with.)
+
+Therefore, for any application of a tycon T to some arguments, the Question We
+Must Answer is:
+
+* Given the first n arguments of T, do the kinds of the non-omitted arguments
+  fill in the omitted arguments?
+
+(This is still a bit hand-wavey, but we'll refine this question incrementally
+as we explain more of the machinery underlying this process.)
+
+Answering this question is precisely the role that the `injectiveVarsOfType`
+and `injective_vars_of_binder` functions exist to serve. If an omitted argument
+`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing
+`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a
+bit.)
+
+More formally, if
+`a` is in `injectiveVarsOfType ty`
+and  S1(ty) ~ S2(ty),
+then S1(a)  ~ S2(a),
+where S1 and S2 are arbitrary substitutions.
+
+For example, is `F` is a non-injective type family, then
+
+  injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c}
+
+Now that we know what this function does, here is a second attempt at the
+Question We Must Answer:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. Do the injective
+  variables of these binders fill in the remainder of T's kind?
+
+Alright, we're getting closer. Next, we need to clarify what the injective
+variables of a tycon binder are. This the role that the
+`injective_vars_of_binder` function serves. Here is what this function does for
+each form of tycon binder:
+
+* Anonymous binders are injective positions. For example, in the promoted data
+  constructor '(:):
+
+    '(:) :: forall a. a -> [a] -> [a]
+
+  The second and third tyvar binders (of kinds `a` and `[a]`) are both
+  anonymous, so if we had '(:) 'True '[], then the kinds of 'True and
+  '[] would contribute to the kind of '(:) 'True '[]. Therefore,
+  injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}.
+  (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.)
+* Named binders:
+  - Inferred binders are never injective positions. For example, in this data
+    type:
+
+      data Proxy a
+      Proxy :: forall {k}. k -> Type
+
+    If we had Proxy 'True, then the kind of 'True would not contribute to the
+    kind of Proxy 'True. Therefore,
+    injective_vars_of_binder(forall {k}. ...) = {}.
+  - Required binders are injective positions. For example, in this data type:
+
+      data Wurble k (a :: k) :: k
+      Wurble :: forall k -> k -> k
+
+  The first tyvar binder (of kind `forall k`) has required visibility, so if
+  we had Wurble (Maybe a) Nothing, then the kind of Maybe a would
+  contribute to the kind of Wurble (Maybe a) Nothing. Hence,
+  injective_vars_of_binder(forall a -> ...) = {a}.
+  - Specified binders /might/ be injective positions, depending on how you
+    approach things. Continuing the '(:) example:
+
+      '(:) :: forall a. a -> [a] -> [a]
+
+    Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind
+    of '(:) 'True '[], since it's not explicitly instantiated by the user. But
+    if visible kind application is enabled, then this is possible, since the
+    user can write '(:) @Bool 'True '[]. (In that case,
+    injective_vars_of_binder(forall a. ...) = {a}.)
+
+    There are some situations where using visible kind application is appropriate
+    (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH
+    reification), so the `injective_vars_of_binder` function is parametrized by
+    a Bool which decides if specified binders should be counted towards
+    injective positions or not.
+
+Now that we've defined injective_vars_of_binder, we can refine the Question We
+Must Answer once more:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. For each such binder
+  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
+  superset of the free variables of the remainder of T's kind?
+
+If the answer to this question is "no", then (T ty_1 ... ty_n) needs an
+explicit kind signature, since T's kind has kind variables leftover that
+aren't fixed by the non-omitted arguments.
+
+One last sticking point: what does "the remainder of T's kind" mean? You might
+be tempted to think that it corresponds to all of the arguments in the kind of
+T that would normally be instantiated by omitted arguments. But this isn't
+quite right, strictly speaking. Consider the following (silly) example:
+
+  S :: forall {k}. Type -> Type
+
+And suppose we have this application of S:
+
+  S Int Bool
+
+The Int argument would be omitted, and
+injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which
+might suggest that (S Bool) needs an explicit kind signature. But
+(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature
+only affects the /result/ of the application, not all of the individual
+arguments. So adding a kind signature here won't make a difference. Therefore,
+the fourth (and final) iteration of the Question We Must Answer is:
+
+* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
+  of T that are instantiated by non-omitted arguments. For each such binder
+  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
+  superset of the free variables of the kind of (T ty_1 ... ty_n)?
+
+Phew, that was a lot of work!
+
+How can be sure that this is correct? That is, how can we be sure that in the
+event that we leave off a kind annotation, that one could infer the kind of the
+tycon application from its arguments? It's essentially a proof by induction: if
+we can infer the kinds of every subtree of a type, then the whole tycon
+application will have an inferrable kind--unless, of course, the remainder of
+the tycon application's kind has uninstantiated kind variables.
+
+What happens if T is oversaturated? That is, if T's kind has fewer than n
+arguments, in the case that the concrete application instantiates a result
+kind variable with an arrow kind? If we run out of arguments, we do not attach
+a kind annotation. This should be a rare case, indeed. Here is an example:
+
+   data T1 :: k1 -> k2 -> *
+   data T2 :: k1 -> k2 -> *
+
+   type family G (a :: k) :: k
+   type instance G T1 = T2
+
+   type instance F Char = (G T1 Bool :: (* -> *) -> *)   -- F from above
+
+Here G's kind is (forall k. k -> k), and the desugared RHS of that last
+instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to
+the algorithm above, there are 3 arguments to G so we should peel off 3
+arguments in G's kind. But G's kind has only two arguments. This is the
+rare special case, and we choose not to annotate the application of G with
+a kind signature. After all, we needn't do this, since that instance would
+be reified as:
+
+   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
+
+So the kind of G isn't ambiguous anymore due to the explicit kind annotation
+on its argument. See #8953 and test th/T8953.
+-}
+
 ------------- No free vars -----------------
 
 -- | Returns True if this type has no free variables. Should be the same as
index 78861f6..0c0fb64 100644 (file)
@@ -66,39 +66,29 @@ 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 :: 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.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.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
           ((GHC.Base.<>)
-             @(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) a)) ::
           T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a
     GHC.Base.sconcat
       = GHC.Prim.coerce
-          @(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.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
           (GHC.Base.sconcat
-             @(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) a)) ::
           GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes
       = GHC.Prim.coerce
           @(b
-            -> 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) a
+               -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(b -> T14578.Wat f g a -> T14578.Wat f g a)
           (GHC.Base.stimes
-             @(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) a)) ::
           forall (b :: TYPE GHC.Types.LiftedRep).
           GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
   
diff --git a/testsuite/tests/deriving/should_compile/T14579.stderr b/testsuite/tests/deriving/should_compile/T14579.stderr
new file mode 100644 (file)
index 0000000..133ba6f
--- /dev/null
@@ -0,0 +1,39 @@
+
+==================== Derived instances ====================
+Derived class instances:
+  instance forall a (x :: Data.Proxy.Proxy a).
+           GHC.Classes.Eq a =>
+           GHC.Classes.Eq (T14579.Wat x) where
+    (GHC.Classes.==)
+      = GHC.Prim.coerce
+          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
+          @(T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool)
+          ((GHC.Classes.==) @(GHC.Maybe.Maybe a)) ::
+          T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool
+    (GHC.Classes./=)
+      = GHC.Prim.coerce
+          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
+          @(T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool)
+          ((GHC.Classes./=) @(GHC.Maybe.Maybe a)) ::
+          T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool
+  
+  instance GHC.Classes.Eq a => GHC.Classes.Eq (T14579.Glurp a) where
+    (GHC.Classes.==)
+      = GHC.Prim.coerce
+          @(T14579.Wat @a (Data.Proxy.Proxy @a)
+            -> T14579.Wat @a (Data.Proxy.Proxy @a) -> GHC.Types.Bool)
+          @(T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool)
+          ((GHC.Classes.==) @(T14579.Wat @a (Data.Proxy.Proxy @a))) ::
+          T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool
+    (GHC.Classes./=)
+      = GHC.Prim.coerce
+          @(T14579.Wat @a (Data.Proxy.Proxy @a)
+            -> T14579.Wat @a (Data.Proxy.Proxy @a) -> GHC.Types.Bool)
+          @(T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool)
+          ((GHC.Classes./=) @(T14579.Wat @a (Data.Proxy.Proxy @a))) ::
+          T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool
+  
+
+Derived type family instances:
+
+
diff --git a/testsuite/tests/deriving/should_compile/T14579b.hs b/testsuite/tests/deriving/should_compile/T14579b.hs
new file mode 100644 (file)
index 0000000..c73844a
--- /dev/null
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PolyKinds #-}
+module T14579b where
+
+import Data.Kind
+import Data.Proxy
+
+-- type P :: forall {k} {t :: k}. Proxy t
+type P = 'Proxy
+
+-- type Wat :: forall a. Proxy a -> *
+newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
+  deriving Eq
+
+-- type Wat2 :: forall {a}. Proxy a -> *
+type Wat2 = Wat
+
+-- type Glurp :: * -> *
+newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a))
+  deriving Eq
index 656cc0d..5aa102b 100644 (file)
@@ -103,8 +103,9 @@ test('T14094', normal, compile, [''])
 test('T14339', normal, compile, [''])
 test('T14331', normal, compile, [''])
 test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
-test('T14579', normal, compile, [''])
+test('T14579', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14579a', normal, compile, [''])
+test('T14579b', normal, compile, [''])
 test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14883', normal, compile, [''])
 test('T14932', normal, compile, [''])
index 2cc3f90..1235b01 100644 (file)
@@ -3,26 +3,19 @@ T15073.hs:8:12: error:
     • Illegal unboxed tuple type as function argument: (# Foo a #)
       Perhaps you intended to use UnboxedTuples
     • In an expression type signature:
-        Foo a
-        -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
+        Foo a -> Unit# @GHC.Types.LiftedRep (Foo a)
       In the expression:
           GHC.Prim.coerce
-            @(a
-              -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-            @(Foo a
-              -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
+            @(a -> Unit# @GHC.Types.LiftedRep a)
+            @(Foo a -> Unit# @GHC.Types.LiftedRep (Foo a))
             (p @a) ::
-            Foo a
-            -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
+            Foo a -> Unit# @GHC.Types.LiftedRep (Foo a)
       In an equation for ‘p’:
           p = GHC.Prim.coerce
-                @(a
-                  -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-                @(Foo a
-                  -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
+                @(a -> Unit# @GHC.Types.LiftedRep a)
+                @(Foo a -> Unit# @GHC.Types.LiftedRep (Foo a))
                 (p @a) ::
-                Foo a
-                -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
+                Foo a -> Unit# @GHC.Types.LiftedRep (Foo a)
       When typechecking the code for ‘p’
         in a derived instance for ‘P (Foo a)’:
         To see the code I am typechecking, use -ddump-deriv
index 21e4f3f..cfd682c 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 21e4f3fa6f73a9b25f3deed80da0e56024238ea5
+Subproject commit cfd682c5fd03b099a3d78c44f9279faf56a0ac70