#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"b4dfe04aa77bb2d0ce2c7d82cab5e4425e0b738c/ghc" b4dfe04/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b4dfe04aa77bb2d0ce2c7d82cab5e4425e0b738c" Fix kind generalisation for pattern synonyms We were failing to zonk, after quantifyTyVars, and that left un-zonked type variables in the final PatSyn. This fixes the patsyn/ problems in Trac #11648, but not the polykinds/ ones. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => merge * milestone: => 8.0.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's a smaller test case for the polykinds error {{{ class Monoidy (to :: k0 -> k1 -> *) (m :: k1) where type MComp to m :: k1 -> k1 -> k0 mjoin :: MComp to m m m `to` m }}} The problem is this: * `TcTyClsDecls.getFamDeclInitialKind` thinks that `MComp` has a CUSK. * When it quantifies over it, it gives it the kind: {{{ MComp :: forall k1_aLj[sk] (k0_aLi[sk] :: TYPE t_aSB[tau:1]). (k0_aLi[sk] -> k1_aLj[sk] -> *) -> k1_aLj[sk] -> k1_aLj[sk] -> k1_aLj[sk] -> k0_aLi[sk] }}} This is wrong: the `t_aSB` should be instantiated to `Lifted`. It's terrible for a meta-tyvar to end up in the kind of a `TyCon`. * So I'm worried about where this defaulting happens in `TcHsType.kcHsTyVarBndrs` with `cusk` = True. Indeed, by adding tracing to this program I've confirmed that `Monoidy` also gets a kind (at least during kind-checking) looking like {{{ forall (k1{tv aLi} [sk] :: *) ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q} (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334})) :: TYPE{(w) tc 32Q} (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334})). ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q} (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334})) -> (k1{tv aLi} [sk] :: *) -> *{(w) tc 330}) -> (k1{tv aLi} [sk] :: *) -> Constraint{(w) tc 32Y} }}} Notice that `t_aSB`. But even if we fix that I'm worried about doing this CUSK stuff for associated types. I think it's probably wrong. We are crawling over the class decl to find constraints on the kind variables so we can infer the class decl's kind. We start that process with `getInitialKinds`; and we can't at that moment quantify over the kind variables we are about to gather constraints for! At very least we must elaborate `Note [Complete user-supplied kind signatures]` to cover associated types. An associate type should have a CUSK iff (a) its parent class does, and (b) any private tyvars have kind sigs. I'm a bit puzzled about why we call `kcTyClDecl` and `generaliseTCD` ''at all'' for decls with a CUSK. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've been wondering if this dragon would bite. And now it has. Consider {{{ data T (a :: Proxy k) }}} Does that have a CUSK? According to the CUSK rules for datatypes, it does indeed: all of the type variables have a kind signature. But there's a problem in that we don't know `k`'s type! So this kind signature isn't complete. Instead, we should need to say, e.g., {{{ data T :: forall (k :: *). Proxy k -> * }}} Note the explicit `:: *` on `k`'s binder, which is necessary for us to have completely specify the kind. However, in looking more closely at this case, I don't actually think this is the problem. A mistake in detecting CUSKness should affect type inference and whether or not we have principal kinds, etc., but it shouldn't produce the drastic failure that we're seeing above. Somehow, it seems that `quantifyTyVars` is making a mistake. I don't have the ability to test this at the moment (I'm in an intermediate state) but should get to this later this week. I propose to fix the immediate problem (which should be straightforward) and then to delay the debate about CUSKs for another time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But `quantifyTyVars` is called from `kindGeneralize` within `kcTyClGroup.generalise`, no? I agree that, if our CUSK check were totally accurate, we should skip `kcTyClDecl` and `generaliseTCD`, but we currently don't. So `quantifyTyVars` should get called. Or am I horribly confused? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Ah -- so the meta-tyvars aren't making it to the real `TyCon`, only the `TcTyCon`? It's quite normal for `TcTyCon`s to have meta-tyvars. (Indeed, that's what they're for.) But I'm missing some context. The ASSERT that's breaking is the check during substitutions. But which substitution? I don't see an obvious substitution in `getFamDeclInitialKind`. To be clear, I think there are two related problems going on: 1. The CUSK check is inaccurate in the presence of `TypeInType`, because implicitly-bound kind variables (like `k` in `data Proxy (a :: k)`) can have non-trivial types. 2. The code in !TcTyClsDecls is tripping over CUSK types that aren't actually CUSKs. I propose to fully defer (1). It can be triggered only with `TypeInType` enabled and has some thorny design issues. And when it goes wrong, it won't be catastrophic (i.e., no panicking, segfaulting, or launching rockets, just an unexpected -- but still sound -- result of type inference). (2) is the real issue at hand. And, currently without the ability to test, I don't fully understand what's going wrong. I hope to be out of my intermediate state today or tomorrow. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is making yet more sense. And it seems that you are proposing: * INVARIANT: The kind of a quantified type variable has no meta-tyvars. We already had that the quantified type variable itself must not be a meta-tyvar. But this invariant goes one step further, in that the set of variables reachable from a quantified tyvar must be devoid of meta-tyvars. Do you agree with this invariant? And, as for design, it seems you are proposing (forgetting about associated types for the moment): * Keep the syntactic definition of CUSK as it is (Note [Complete user- supplied kind signatures] in HsDecls). * When a declaration has a CUSK, default any remaining meta-tyvars after `getInitialKind`. * If a meta-tyvar is not defaultable, the program is erroneous. I'm quite dubious of this design for several reasons. First, this seems strange to users. For example: {{{ data T1 (a :: Proxy k) data T2 (a :: Proxy k) b }}} `T1` has a CUSK, according to our definition. Thus its `k` will be defaulted to kind `*`. `T2`, though, does not have a CUSK, and so `k` is not defaulted and has kind `k2`. Second, the design seems hard to implement without annoying users. For example: {{{ data T3 (x :: * -> *) data T4 (a :: T3 k) }}} `T4` has a CUSK, and `k` should clearly have kind `* -> *`. But we can't discover that until `kcTyClDecl`, which is too late. According to the last bullet above, we'll fail at defaulting `T4`'s `k`'s kind and issue an error, even though it's quite obvious what we should do. So, I must ask: why is it so necessary to have the INVARIANT at the top? I understand this requires expanding the in-scope set for the substitution at hand, but why is that problematic? I don't see what's so bad about a meta-tyvar in a quantified variable's kind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:17 simonpj]:

...

So, I must ask: why is it so necessary to have the INVARIANT at the top?

What if `f :: forall k. forall (a :: kappa). blah`, where `kappa` is a kind meta-var. What if `kappa` was later instantiated to `k`? Now the type looks quite different.

I'm not sure what you mean by "quite different". Yes, if we get `kappa := k`, then the type has more dependency, but what's so bad about that?

Indeed `kcHsTyVarBndrs` goes to some trouble to avoid this {{{ -- in the CUSK case, we want to default any un-kinded

tyvars

-- See Note [Complete user-supplied kind signatures] in

HsDecls

; case hs_tvb of UserTyVar {} | cusk , not scoped -- don't default class tyvars -> discardResult $ unifyKind (Just (mkTyVarTy tv)) liftedTypeKind (tyVarKind tv) }}}

This code is intended to deal with open data/type family declarations, which always have a CUSK, by fiat. It shouldn't trigger in any other case, because all other declaration forms require `KindedTyVar`s to make a CUSK.

For your T1/T2 example I'm not too bothered. CUSKs mean that the user has ''specified the complete kind''. If you want `k` to have some other kind than `*` you can specify that too (I hope).

OK.

For T3/T4, note that `kdHsTyVarBndrs` calls `TcHsTyVarBndr_Scoped` which

in turn calls `unifyKind` so I think you'll be fine. (BUt there is clearly a missing `solveEqualities` here! Yes, I suppose that's true. But I don't spot a missing `solveEqualities` anywhere. Did you miss the call toward the top of `kcTyClGroup`? Bottom line here: I'm unconvinced about INVARIANT. But it does seem easy enough to implement "all declarations with CUSKs default all meta-tyvars", which solves the main problem here. And then we just punt on INVARIANT. In other words, I wish to address (1) from comment:14, which will then solve (2) on the way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"55577a9130738932d022d442d0773ffd79d0945d/ghc" 55577a9/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="55577a9130738932d022d442d0773ffd79d0945d" Fix #11648. We now check that a CUSK is really a CUSK and issue an error if it isn't. This also involves more solving and zonking in kcHsTyVarBndrs, which was the outright bug reported in #11648. Test cases: polykinds/T11648{,b} This updates the haddock submodule. [skip ci] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T11648{,b} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): A few comments for posterity on the commit above: A lot of the changes are due to moving decisions out from kcHsTyVarBndrs, and thus the need to store information in the AST: - It turned out to be more convenient to decide if a data decl has a CUSK in the renamed than on the fly. (It could be done on the fly, but it would have been a bit hairy and duplicated code in the renamer.) See the new bit in the manual for a description of what's going on here. - There also needed to be a decision about whether to use `Anon` or `Named` when building the `TcTyBinder`s of a tycon's kind. Previous to this patch, this was done in `kcHsTyVarBndrs`, but -- as Simon pointed out to me -- this was bogus (it looked at the free variables of a not-yet- solved-or-zonked type). So it's now done via a simple syntactic check in the renamer. But then the result of the check must be put in the AST, causing knock-on changes. See `Note [Dependent LHsQTyVars]` in !TcHsType and also a new bit in the manual. - One of this issues brought up in the ticket is the handling of CUSKs for associated type families. An associated type/data family's CUSKness must be inherited from the enclosing class. Previously, all associated families had CUSKs, but this was wrong. So the CUSK check is a bit more intricate to allow for this relationship. - Along the way, I made `(->)`, when used in a kind, have type `* -> * -> *`, instead of being polymorphic in `RuntimeRep`s. We don't have type- level representation polymorphism. - Also incidental to this patch, I made kind variables have kind `*` when `-XTypeInType` is not in effect. Not doing this earlier was an oversight. The check isn't perfect, as it's sometimes hard to tell what's a kind variable and what isn't; currently, only variables used in kinds in tycon `LHsQTyVars` are affected, and these are surely kind variables. (This is `mk_kv_kinds` in `kcHsTyVarBndrs`.) - There is a new function `anonymiseTyBinders`. This was necessary in an earlier version of this patch but is now redundant (and harmless). I will remove. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T11648{,b} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Don't forget to merge both 55577a9 (the main patch) and 19be5385. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler