Re: [GHC] #15076: Typed hole causes GHC to panic (No skolem info)

22 Apr 2018

      #15076: Typed hole causes GHC to panic (No skolem info)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |             Keywords:  TypedHoles,
      Resolution:                    |  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14040            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Echoing simonpj's comments in
 https://ghc.haskell.org/trac/ghc/ticket/14040#comment:7, we can see from
 `-ddump-tc-trace` that:

 {{{
 reportUnsolved (after zonking):
   Free tyvars: (t_a1TL[tau:2] :: Proxy x_a1TC[sk:2]) a_a1Sj[sk:1]
   Tidy env: ([ESf9Q :-> 1, ESfa3 :-> 1, ESfWb :-> 2,
               ESgJA :-> 1],
              [a1Sj :-> a1_a1Sj[sk:1], a1TC :-> x_a1TC[sk:2],
               a1TD :-> a_a1TD[sk:2], a1TL :-> t0_a1TL[tau:2]])
   Wanted: WC {wc_impl =
                 Implic {
                   TcLevel = 2
                   Skolems = (x_a1TC[sk:2] :: a_a1Sj[sk:1])
                             a_a1TD[sk:2]
                             (f_a1TE[sk:2] :: forall (x :: a_a1TD[sk:2]).
 Proxy x -> *)
                   No-eqs = True
                   Status = Unsolved
                   Given =
                   Wanted =
                     WC {wc_simple =
                           [D] _ {0}:: Proxy t_a1TL[tau:2]
                                       -> Proxy
                                            (f_a1TE[sk:2] x_a1TC[sk:2]
 t_a1TL[tau:2]) (CHoleCan: TypeHole(_))}
                   Binds = EvBindsVar<a1TM>
                   Needed inner = []
                   Needed outer = []
                   the type signature for:
                     foo :: forall (x :: a_a1Sj[sk:1]) a (f :: forall (x ::
 a).
                                                               Proxy x ->
 *).
                            S (f x) -> () }}
 ...
 Adding error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180420 for x86_64-unknown-linux):
         No skolem info:
   [a1_a1Sj[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
 }}}

 Here, `a1_a1Sj` is not bound by any implication.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler