[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       |           Version:  8.0.1
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 The following code causes a GHC panic on GHC 8.0.1, 8.0.2, 8.2.1, and
 HEAD:

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

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