#14880: GHC panic: updateRole -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: Roles => TypeInType * owner: (none) => goldfire Comment: The trouble is that the type of `MkBar` should really be {{{ MkBar :: forall (x:Type) (arg:Type) {a:arg}. Proxy @(Proxy @arg a -> Type) (Foo arg @a) -> Bar x }}} where I have put in all the kind applications. The trouble is that `MkBar` has an ''implicit'' forall's variable `a`, whose kind mentions an ''explicit'' type variable `arg`. So the implicit argument must appear later in the telescope. But `tcConDecl` (the `ConDeclGADT` case) doesn't allow that: {{{ tkv_bndrs = mkTyVarBinders Inferred tkvs' user_tv_bndrs = mkTyVarBinders Specified user_tvs' all_user_bndrs = tkv_bndrs ++ user_tv_bndrs }}} Notice that the inferred ones always come first. But here they can't! Solution: do a topo-sort of the tyvars that is allowed to interleave the `Inferred` and `Specified` ones. But is that the only place? If we try something like this with a function type signature thus {{{ f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a f = f }}} we get the error message {{{ T14880.hs:24:6: error: * The kind of variable `k', namely `v', depends on variable `v' from an inner scope Perhaps bind `k' sometime after binding `v' NB: Implicitly-bound variables always come before other ones. * In the type signature: f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a }}} But is there anything really wrong with this signature? It we topo-sorted the type variables we'd be fine. There are other places (exp in `TcTyClsDecls`) where we seem to put all the inferred variables around the outside. I don't know how to be sure in which, if any, of these case we have a bug. Maybe we need more topo-sorts? Amnother oddd thing about this ticket is the data decl for `Foo`: {{{ data Foo (v :: Type) :: forall (a :: v). Proxy a -> Type }}} That is a strange kind signature. I don't expect to see foralls to the right of the `::` in such a decl. So, more questions * Is it valuable to permit TyCons whose kinds are not in prenex form (i.e. all foralls at the front)? If so, we should document it. Meanwhile I'm not going to fix this because it may all come out in the wash of Richards's upcoming kind-inference patch. It's nothing to do with roles! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14880#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler