#14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T14579{a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4264, | Phab:D5229, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/261 -------------------------------------+------------------------------------- Comment (by simonpj): I've read the patch, but I'm commenting here because Trac has greater longevity than code reviews. You have written a commendably detailed Note -- thank you. Still, it took me a solid hour of head-scratching to really understand it. Here are some thoughts that may (or may not) help to make it clearer. First, it took me ages reslise that `tyConAppNeedsKindSig` can be done without knowing the actual arguments to `T`. Only once I'd realised that did I discover that, sure enough, it doesn't rely on `args`, only on `length args`! So I ''strongly'' suggest {{{ tyConAppNeedsKindSig :: Bool -- ^ Should specified binders count towards injective positions in -- the kind of the TyCon? -> TyCon -> Int -- Number of args -> Bool -- Does (T t1 .. tn) need a signature tyConAppNeedsKindSig spec_inj_pos tc n_args = ... }}} That is, pass the ''number'' of args, not the actual args. That makes it clear that the function could, in principle, live in `TyCon`. It could even be cached in the TyCon, as a list of `Bools` or, because of the Inferred/Specified thing, two lists of `Bools`. But the caching is probably not worth it. Ok then, my thought process went like this. Given a application `T t1 .. tn`, does it need a kind signature? Why might it need a kind signature? So that we can fill in any of T's omitted arguments. By an "omitted argument" I mean one that we do not reify expicitly in the `HsType`. Sometimes the omitted ones are Inferred ones (in `typeToHsType`); sometimes both Inferred and Specified (in `TcSplice`); but the key thing is that they don't appear in the `HsType`. What do we mean by "fill in"? Suppose {{{ T :: forall {k}. Type -> (k->*) -> k }}} and we have the application `T {j} Int aty`. When we convert to `HsType` we are going to omit the inferred arg `{j}`. Is it fixed by the other non-inferred args? Yes: if we know the kind of `aty :: blah`, we'll generate an equality constraint `(kappa->*) ~ blah` and, assuming we can solve it, that will fix `kappa`. (Here `kappa` is the unification variable that we instantiate `k` with.) So the question becomes this. * Consider the first `n` args of T: do the kinds of the non-omitted arguments determine the omitted arguments? We'll only handle the case were the omitted arguments are `NamedTCB`, so we need to determine a variable. When does a kind "determine" a variable? This is what `injectiveVarsOfType` computes. {{{ -- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation -- of what an injective position is.) injectiveVarsOfType :: Type -> FV }}} Rather than speak of "injective positions" I think of it like this: if `a` is in `injectiveVarsOfType ty` then knowing `ty` fixes, or determines, `a`. 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, if `F` is a non-injective type family, then {{{ injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c} }}} (This part about `injectiveVarsOfType` is not new -- but I'd suggest adding it as comments to the function.) So we can refine the question: * Consider the first `n` args of T, and each omitted argument `i <= n`: is argument `i` a `NamedTCB` binder `b`, and does `b` appear in `injectiveVarsOfTtype (k(i+1) .. k(n))`? Where `kj` is the kind of the j'th argument of T. Much of this is as you have it, except that I'm not lookin at `result_kind` (in your `tyConAppNeedsKindSig`. If I can't fill in all omitted arguments, I'll add a kind signature. So for a silly thing like {{{ T :: forall k. Type -> Type }}} and the type `(T {j} Int)`, I'll add a kind signature, which actually does no good since `k` is unused. But it's a silly example. And you'll add one for a different silly example. {{{ T :: forall k. Type -> F k }}} which equally does no good. Nothing here is radically different from what you have. But I find the chain of thought here easier to follow. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14579#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler