[GHC] #15629: "No skolem info" panic (GHC 8.6 only)
GHC
ghc-devs at haskell.org
Tue Sep 11 18:35:54 UTC 2018
#15629: "No skolem info" panic (GHC 8.6 only)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.6.1-beta1
(Type checker) |
Keywords: TypeInType | Operating System: Unknown/Multiple
Architecture: | Type of failure: Compile-time
Unknown/Multiple | crash or panic
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
The following program:
{{{#!hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k -> Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t -> Sing (Apply f t)) -> Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k -> Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type -> Type) x. Proxy (m x) -> ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z)
.@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
}}}
Panics on GHC 8.6:
{{{
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m
ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$
To1Sym0) :: Rep1 m ab
~> Rep1 m ab)
|
50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z)
.@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64-unknown-linux):
No skolem info:
[ab_a1UW[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in
ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in
ghc:TcErrors
}}}
But merely errors on GHC 8.4.3:
{{{
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m
ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$
To1Sym0) :: Rep1 m ab
~> Rep1 m ab)
|
50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z)
.@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5-112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)
|
51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
| ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5-112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)
|
51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
| ^^^^^^^
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15629>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list