summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/hsSyn/HsUtils.hs87
-rw-r--r--compiler/typecheck/TcSplice.hs120
-rw-r--r--compiler/types/TyCoRep.hs305
-rw-r--r--testsuite/tests/deriving/should_compile/T14578.stderr30
-rw-r--r--testsuite/tests/deriving/should_compile/T14579.stderr39
-rw-r--r--testsuite/tests/deriving/should_compile/T14579b.hs21
-rw-r--r--testsuite/tests/deriving/should_compile/all.T3
-rw-r--r--testsuite/tests/deriving/should_fail/T15073.stderr21
m---------utils/haddock0
9 files changed, 421 insertions, 205 deletions
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index febd5ac64f..dfb0ebf0db 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -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.
-}
{- *********************************************************************
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 1bb844a77f..548dc7201e 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -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
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 075d270095..f7c21b7626 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -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
diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index 78861f69e0..0c0fb641f7 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -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
index 0000000000..133ba6fb2f
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14579.stderr
@@ -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
index 0000000000..c73844a1db
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14579b.hs
@@ -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
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 656cc0de4b..5aa102b871 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -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, [''])
diff --git a/testsuite/tests/deriving/should_fail/T15073.stderr b/testsuite/tests/deriving/should_fail/T15073.stderr
index 2cc3f90482..1235b01c68 100644
--- a/testsuite/tests/deriving/should_fail/T15073.stderr
+++ b/testsuite/tests/deriving/should_fail/T15073.stderr
@@ -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
diff --git a/utils/haddock b/utils/haddock
-Subproject 21e4f3fa6f73a9b25f3deed80da0e56024238ea
+Subproject cfd682c5fd03b099a3d78c44f9279faf56a0ac7
View Lorry Controller Status