Opened 5 months ago
Closed 4 months ago
#13877 closed bug (fixed)
GHC panic: No skolem info: k2
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | TypeApplications | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | indexed-types/should_fail/T13877 |
Blocked By: | Blocking: | ||
Related Tickets: | #13910, #14040 | Differential Rev(s): | Phab:D3794 |
Wiki Page: |
Description
The following code causes a GHC panic on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Eliminator where import Data.Kind data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) | (:~>) class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 $(return []) instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 listElim :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) -> p l listElim = listElimPoly @(:->) @a @p @l listElimTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> p @@ '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) -> p @@ l -- The line below causes a GHC panic. It should not typecheck; -- uncomment the line below it for the correct version listElimTyFun = listElimPoly @(:->) @a @p @l -- listElimTyFun = listElimPoly @(:~>) @a @p @l listElimPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) -> App [a] arr Type p l listElimPoly SNil pNil _ = pNil listElimPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (listElimPoly @arr @a @p @xs xs pNil pCons)
$ /opt/ghc/8.2.1/bin/ghci Eliminator.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Eliminator ( Eliminator.hs, interpreted ) Eliminator.hs:72:17: error:ghc: panic! (the 'impossible' happened) (GHC version 8.2.0.20170623 for x86_64-unknown-linux): No skolem info: k2_a5cr 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 Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Change History (12)
comment:1 Changed 5 months ago by
comment:2 Changed 5 months ago by
Going back to the original program, if you change this line:
listElimTyFun = listElimPoly @(:->) @a @p @l
To this:
listElimTyFun = listElimPoly @(:->)
You get a different panic:
$ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Eliminator ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.0.20170623 for x86_64-unknown-linux): piResultTy Fun [a_a5hm[sk:2]] (':->) * l_a5ho[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/types/Type.hs:948:35 in ghc:Type Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
comment:3 Changed 5 months ago by
Related Tickets: | → #13910 |
---|
comment:4 Changed 5 months ago by
Keywords: | TypeApplications added |
---|
comment:5 Changed 5 months ago by
Cc: | Iceland_jack added |
---|
comment:6 Changed 4 months ago by
This appears to be fixed in GHC HEAD. I need to figure out which commit did the deed.
comment:7 Changed 4 months ago by
comment:8 Changed 4 months ago by
Commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.
) fixed the original program. TODO Add regression test.
comment:9 Changed 4 months ago by
Related Tickets: | #13910 → #13910, #14040 |
---|
I've opened a separate ticket #14040 for the program in comment:1, since it wasn't fixed by 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76.
comment:10 Changed 4 months ago by
Differential Rev(s): | → Phab:D3794 |
---|---|
Status: | new → patch |
comment:12 Changed 4 months ago by
Milestone: | → 8.4.1 |
---|---|
Resolution: | → fixed |
Status: | patch → closed |
Test Case: | → indexed-types/should_fail/T13877 |
Note: See
TracTickets for help on using
tickets.
Here's another occurrence of this panic I found when writing similar code: