[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:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #15076


Comment:

 I think that this ticket and #15076 share a symptom in common. This claim
 is based on the fact that slightly tweaking the program in comment:6 /
 comment:7 :

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

 quux :: forall arg. Proxy (Foo arg) -> ()
 quux (_ :: _) = ()
 }}}

 Yields:

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:12:12: error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180420 for x86_64-unknown-linux):
         No skolem info:
   [arg_aZr[sk:1]]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in
 ghc:TcErrors
 }}}

 Which is the same panic as in #15076. Plus, if you run this program with
 `-ddump-tc-trace`, you see:

 {{{
 reportUnsolved (after zonking):
   Free tyvars: arg_aZr[sk:1]
   Tidy env: ([ESf71 :-> 1], [aZr :-> arg_aZr[sk:1]])
   Wanted: WC {wc_impl =
                 Implic {
                   TcLevel = 2
                   Skolems = (a_a1p8[sk:2] :: arg_aZr[sk:1]) arg_a1p9[sk:2]
                   No-eqs = True
                   Status = Unsolved
                   Given =
                   Wanted =
                     WC {wc_simple =
                           [D] _ {0}:: Proxy
                                         (Foo arg_a1p9[sk:2] a_a1p8[sk:2])
 (CHoleCan: TypeHole(_))}
                   Binds = EvBindsVar<a1pg>
                   Needed inner = []
                   Needed outer = []
                   the type signature for:
                     quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo
 arg a) -> () }}
 }}}

 Just like in #15076, `arg_aZr` is not bound in any implication. On the
 other hand, there is another type variable, `arg_a1p9`, that is
 suspiciously similar. Moreover, the type signature it gives for `quux`:

 {{{
 quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo arg a) -> ()
 }}}

 Seems to have //two// different copies of `arg`! This is especially
 interesting in light of comment:3, where simonpj discovered that the
 existentially quantified tyvars in `MkBar` were screwed up, leading to two
 copies of `arg`.

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