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

[GHC]

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

Comment (by simonpj):

 The original program now reports just one error
 {{{
 T14040.hs:41:8: error:
     • Cannot apply expression of type ‘Sing wl0
                                        -> (forall y. p0 _0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs ::
 WeirdList (WeirdList z1)).
                                            Sing x -> Sing xs -> p0 _1 xs
 -> p0 _2 ('WeirdCons x xs))
                                        -> p0 _3 wl0’
       to a visible type argument ‘(WeirdList z)’
 }}}
 And that's right: the signature for `elimWierdList` is a partial
 signature, so we do ''inference'' on the definition.  So at the recursive
 call to `elimWierdList`, the function is a monotype, and can't be applied
 to type arguments.

 However, for the `elimWierdList x = error "urk"` version I get
 {{{
 WARNING: file compiler/types/TyCoRep.hs, line 3033
   in_scope InScope {a_a10j wl_a10k p_a10l}
   tenv [aX1 :-> a_a10j[tyv:1], aX2 :-> wl_a10k[tyv:1],
         aX4 :-> p_a10l[tyv:1]]
   cenv []
   tys [Sing wl_aX2[tyv:1]
        -> (forall y. p_aX4[tyv:1] __aZo[tau:2] 'WeirdNil)
        -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
            Sing x
            -> Sing xs
            -> p_aX4[tyv:1] __aZL[tau:2] xs
            -> p_aX4[tyv:1] __aZP[tau:2] ('WeirdCons x xs))
        -> p_aX4[tyv:1] __aZW[tau:1] wl_aX2[tyv:1]]
   cos []
   needInScope {z_aX6[sk:2], x_aZm[tau:2], __aZo[tau:2], __aZL[tau:2],
                __aZP[tau:2], __aZW[tau:1]}
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1211:29 in
 ghc:Outputable
         warnPprTrace, called at compiler/types/TyCoRep.hs:3027:6 in
 ghc:TyCoRep
         checkValidSubst, called at compiler/types/TyCoRep.hs:3050:29 in
 ghc:TyCoRep
         substTy, called at compiler/typecheck/TcSigs.hs:507:49 in
 ghc:TcSigs
 ghc-stage1: panic! (the 'impossible' happened)
   (GHC version 8.7.20190215 for x86_64-unknown-linux):
         ASSERT failed!
   2
   0
   __a23h[tau:0]
   Any
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in
 ghc:Outputable
         pprPanic, called at compiler/utils/Outputable.hs:1220:5 in
 ghc:Outputable
         assertPprPanic, called at compiler/typecheck/TcMType.hs:805:54 in
 ghc:TcMType

 Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
 }}}
 So there is still stuff wrong here.

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