[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
GHC
ghc-devs at haskell.org
Wed Feb 13 15:13:40 UTC 2019
#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.10.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 for the `error "urk"` version has changed once again in
GHC HEAD. Simon, can you spot-check this to see if this looks correct?
(Modulo wildcard pretty-printing, of course.)
{{{
$ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20190212: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘_1 :: x0’
Where: ‘x0’ is an ambiguous type variable
‘_1’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘p’, namely ‘_’
In the 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’
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
|
24 | -> (forall (y :: Type). p _ WeirdNil)
| ^
Bug.hs:26:44: error:
• Found type wildcard ‘_’
standing for ‘GHC.Types.Any :: WeirdList z’
Where: ‘z’ is a rigid type variable bound by
‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList
z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
at Bug.hs:25:27
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘p’, namely ‘_’
In the 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’
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
|
26 | Sing x -> Sing xs -> p _ xs
| ^
Bug.hs:27:24: error:
• Found type wildcard ‘_’ standing for ‘GHC.Types.Any :: z’
Where: ‘z’ is a rigid type variable bound by
‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList
z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
at Bug.hs:25:27
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘p’, namely ‘_’
In the 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’
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
|
27 | -> p _ (WeirdCons x xs))
| ^
Bug.hs:28:20: error:
• Found type wildcard ‘_’ standing for ‘_0 :: a’
Where: ‘a’ is an ambiguous type variable
‘_0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘p’, namely ‘_’
In the 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’
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
|
28 | -> p _ wl
| ^
Bug.hs:37:19: error:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls:
(forall y. p _1 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p GHC.Types.Any xs
-> p GHC.Types.Any ('WeirdCons x xs))
-> p _0 wl
GHC doesn't yet support impredicative polymorphism
• In the expression: error "urk"
In an equation for ‘elimWeirdList’: elimWeirdList x = error "urk"
• Relevant bindings include
x :: Sing wl (bound at Bug.hs:37:15)
elimWeirdList :: Sing wl
-> (forall y. p _1 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList
z)).
Sing x
-> Sing xs
-> p GHC.Types.Any xs
-> p GHC.Types.Any ('WeirdCons x xs))
-> p _0 wl
(bound at Bug.hs:37:1)
|
37 | elimWeirdList x = error "urk"
| ^^^^^^^^^^^
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#comment:18>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list