#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