[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:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:  fixed             |  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):

 There's still something wrong here, in the original program.  Even if we
 write
 {{{
 elimWeirdList x = error "urk"
 }}}
 GHC HEAD still complains mysteriously about the type signature
 {{{
 T14040a.hs:21:18: error:
     • Couldn't match type ‘k0’ with ‘a’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
                                                                 x ->
 WeirdList x -> *).
                            Sing wl
                            -> (forall y. p k0 w0 'WeirdNil)
                            -> (forall z1 (x :: z1) (xs :: WeirdList
 (WeirdList z1)).
                                Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                            -> p k3 w3 wl
         at T14040a.hs:(21,18)-(28,23)
       Expected type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
         Actual type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
     • In the ambiguity check for ‘elimWeirdList’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 T14040a.hs:29:1: error:
     Can't quantify over ‘a’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 T14040a.hs:29:1: error:
     Can't quantify over ‘wl’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 T14040a.hs:29:1: error:
     Can't quantify over ‘p’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

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