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

14 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 RyanGlScott):

 Well I'll be danged—it looks like this no longer panics on GHC HEAD!

 {{{
 $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.5.20180413: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.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 Bug.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)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 Bug.hs:34:8: error:
     • Cannot apply expression of type ‘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’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
       In the expression:
         pWeirdCons
           @z
           @x
           @xs
           x
           xs
           (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
       In an equation for ‘elimWeirdList’:
           elimWeirdList
             (SWeirdCons (x :: Sing (x :: z))
                         (xs :: Sing (xs :: WeirdList (WeirdList z))))
             pWeirdNil
             pWeirdCons
             = pWeirdCons
                 @z
                 @x
                 @xs
                 x
                 xs
                 (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil
 pWeirdCons)
    |
 34 |       (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 I'll confirm which commit caused this and add a regression test.

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