Opened 3 months ago

Closed 2 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 3 months ago by RyanGlScott

Here's another occurrence of this panic I found when writing similar code:

{-# 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.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 Bug              ( Bug.hs, interpreted )

Bug.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)
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Bug.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)
   |                                         ^

Bug.hs:26:44: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.0.20170623 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

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

comment:2 Changed 3 months ago by RyanGlScott

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 3 months ago by RyanGlScott

comment:4 Changed 3 months ago by simonpj

Keywords: TypeApplications added

comment:5 Changed 3 months ago by Iceland_jack

Cc: Iceland_jack added

comment:6 Changed 2 months ago by RyanGlScott

This appears to be fixed in GHC HEAD. I need to figure out which commit did the deed.

comment:7 Changed 2 months ago by RyanGlScott

Er, to be clear, the original program is fixed. I can't tell if the program in comment:2 panics anymore since it triggers #14038, and the program in comment:1 still panics, so at the very least I'll open a new ticket for the comment:1 program.

comment:8 Changed 2 months ago by RyanGlScott

Commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.) fixed the original program. TODO Add regression test.

comment:9 Changed 2 months ago by RyanGlScott

I've opened a separate ticket #14040 for the program in comment:1, since it wasn't fixed by 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76.

comment:10 Changed 2 months ago by RyanGlScott

Differential Rev(s): Phab:D3794
Status: newpatch

comment:11 Changed 2 months ago by Ryan Scott <ryan.gl.scott@…>

In 424ecadb/ghc:

Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794

comment:12 Changed 2 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: indexed-types/should_fail/T13877
Note: See TracTickets for help on using tickets.