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

29 Oct 2018

      #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.8.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 RyanGlScott):

 simonpj, isn't it expected that GHC would complain if you implemented
 `elimWeirdList` as `elimWeirdList x = error "urk"`? After all,
 `elimWeirdList` contains higher-rank arguments, and trying to instantiate
 them with `error "urk" :: forall a. a` would require instantiating `a`
 with a polytype, which is impredicative.

 Also, it's worth noting that on GHC HEAD, you get one fewer error than you
 do in comment:12:

 {{{
 GHCi, version 8.7.20181029: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:37: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
    |
 37 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:37: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
    |
 37 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:37: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
    |
 37 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Failed, no modules loaded.
 }}}

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