[GHC] #14880: GHC panic: updateRole

[GHC]

#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       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:  #15076            |  Differential Rev(s):  Phab:D4769,
       Wiki Page:                    |  Phab:D5141
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Good grief.  More revelations/insight concerning `closeOverKinds`.

 * The actual bug is fixed by the small patch in comment:13, concerning
   `candidateQTyVarsOfType` in `TcType`.  Nothing to do with `TyCoRep`.

 * But this patch did not quite work for reasons that are lost in the
   mists of time.  Later, Ricahrd produced Phab:D4769 (see comment:19).

 * But Pahb:D4769 was significantly more ambitious, which in turn led
   to the detective work on this ticket.  Concering `closeOverKinds`,
   it added this in `TyCoRep`:
 {{{
 Note [Closing over free variable kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Note that it's necessary to close over kinds at the /end/ of collecting
 the variables. This is for two reasons:

 1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k),
 then
    we don't want to have to traverse k more than once.

 2. Correctness. Imagine we have forall k. b -> k, where b has
    kind k, for some k bound in an outer scope. If we look at b's kind
 inside
    the forall, we'll collect that k is free and then remove k from the set
 of
    free variables. This is plain wrong. We must instead compute that b is
 free
    and then conclude that b's kind is free.
 }}}

 * It seems that moving `closeOverKinds` from the ''occurrences'' of
   a type variable to ''after finding the free vars'' (i.e. Step 2)
   is responsible for the perf regressions reported in comment:121.

   But note that, contrary to my claim in comment:108, this change in
   `closeOverKinds` does not fix the original bug -- that was in `TcType`!

 My new insight is this: '''Step 2 is absolutely unnecessary'''.

 Consider the two points in the Note above.

 1. Efficiency: we now have an accumulator, so the seond time we
    encounter 'a', we'll ignore it, certainly not looking at its kind.

 2. Correctness: we have an "in-scope set" (I think we should call it
    it a "bound-var set"), specifying variables that are bound by
    a forall in the type we are traversing; we simply ignore these
    variables, certainly not looking  at their kind.

    So consider `forall k. b -> k`, where `b :: k->Type` is free; but of
    course, it's a different `k`!  When looking at `b -> k` we'll have
    `k` in the bound-var set.  So we'll ignore the `k`.  But suppose this
    is our first encounter with `b`; we want the free vars of its kind.
    '''But we want to behave as if we took the free vars of its kind
    at the end; that is, with no bound vars in scope'''.

    So it's easy. Our current code is this
 {{{
 ty_co_vars_of_type (TyVarTy v) is acc
   | v `elemVarSet` is  = acc
   | v `elemVarSet` acc = acc
   | otherwise          = ty_co_vars_of_type (tyVarKind v) is (extendVarSet
 acc v)
 }}}
    All we need do is to take the free vars of `tyVarKind v` ''with an
 empty bound-var set'', thus:
 {{{
 ty_co_vars_of_type (TyVarTy v) is acc
   | v `elemVarSet` is  = acc
   | v `elemVarSet` acc = acc
   | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet
 (extendVarSet acc v)
                                                           ^^^^^^^^^^^
 }}}
 This change is subtle, but it's both more efficient and less code
 than my suggestion in comment:122.

 The same change should be made in the `FV` version lower down in
 `TyCoRep`.

 Would you like to try that.

 '''Richard: do you agree?'''

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14880#comment:123>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler