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

GHC ghc-devs at haskell.org
Thu Nov 29 19:43:51 UTC 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):

 The error message has changed once again in GHC HEAD (as of commit
 2257a86daa72db382eb927df12a718669d5491f8):

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

 ../Bug.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl0
                                        -> (forall y. p0 w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs ::
 WeirdList (WeirdList z1)).
                                            Sing x -> Sing xs -> p0 w1 xs
 -> p0 w2 ('WeirdCons x xs))
                                        -> p0 w3 wl0’
       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)
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

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


More information about the ghc-tickets mailing list