[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
GHC
ghc-devs at haskell.org
Thu Jul 27 15:47:20 UTC 2017
#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:
Component: Compiler | Version: 8.0.2
(Type checker) |
Keywords: TypeInType, | Operating System: Unknown/Multiple
TypeFamilies, |
PartialTypeSignatures |
Architecture: | Type of failure: Compile-time
Unknown/Multiple | crash or panic
Test Case: | Blocked By:
Blocking: | Related Tickets: #13877
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
{{{#!hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type -> Type where
WeirdNil :: WeirdList a
WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
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
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
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)
}}}
{{{
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p x0 t3 'WeirdNil)
-> (forall z (x :: z) (xs ::
WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p (WeirdList z) t2 xs
-> p z t1 ('WeirdCons x xs))
-> p a t0 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)
}}}
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
{{{
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• 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
• Relevant bindings include
elimWeirdList :: Sing wl
-> (forall y. p x0 t0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList
z)).
Sing x
-> Sing xs -> p (WeirdList z) t1 xs -> p z t2
('WeirdCons x xs))
-> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: z_a13X[sk]
}}}
{{{
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• 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)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• 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)
| ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at
compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in
ghc:TcErrors
}}}
(The error messages from HEAD, at commit
791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list