[GHC] #13877: GHC panic: No skolem info: k2

[GHC]

#13877: GHC panic: No skolem info: k2
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

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

 {{{#!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.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
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13877#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler