[GHC] #14880: GHC panic: updateRole

[GHC]

#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