Re: [GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

4 Apr 2018

      #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I regret to report that even after Richard's "solveEqualties" patch
 #14066, the example in comment:2 yields
 {{{
 T14040.hs:91:28: error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180402 for x86_64-unknown-linux):
         No skolem info:
   [a1_aWV[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
 }}}
 This arises during the error-report-generation stage.  The residual
 constraint is this
 {{{
 reportUnsolved (after zonking):
   Free tyvars: (t_a1e3[tau:2] :: Proxy x_a1dP[sk:2]) a_aWV[sk:1]
   Tidy env: ([ESf6y :-> 1, ESf7a :-> 1, ESfO0 :-> 2,
               ESgiS :-> 1],
              [aWV :-> a1_aWV[sk:1], a1dP :-> x_a1dP[sk:2],
               a1dQ :-> a_a1dQ[sk:2], a1e3 :-> t0_a1e3[tau:2]])
   Wanted: WC {wc_impl =
                 Implic {
                   TcLevel = 2
                   Skolems = (x_a1dP[sk:2] :: a_aWV[sk:1])
                             a_a1dQ[sk:2]
                             (f_a1dR[sk:2] :: forall (x :: a_a1dQ[sk:2]).
 Proxy x ~> *)
                             (x_a1dS[sk:2] :: a_a1dQ[sk:2])
                   No-eqs = True
                   Status = Unsolved
                   Given =
                   Wanted =
                     WC {wc_simple =
                           [D] _ {0}:: Sing t_a1e3[tau:2]
                                       -> Sing
                                            (Apply
                                               (f_a1dR[sk:2] x_a1dP[sk:2])
                                               t_a1e3[tau:2]) (CHoleCan:
 TypeHole(_))}
                   Binds = EvBindsVar<a2gv>
                   Needed inner = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
                                   a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
 :-> co_a2hR,
                                   a2hS :-> co_a2hS, a2i2 :-> $dIP_a2i2]
                   Needed outer = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
                                   a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
 :-> co_a2hR,
                                   a2hS :-> co_a2hS]
                   the type signature for:
                     dapp :: forall (x :: a_aWV[sk:1]) a (f :: forall (x ::
 a).
                                                               Proxy x ~>
 *) (x :: a).
                             Sing (f x) -> Sing x -> f x @@ 'Proxy }
 }}}
 And indeed you can see that the skolem `a1_aWV` is not bound by any
 implication.  This must be a bug.

 Richard?

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