[GHC] #15629: "No skolem info" panic (GHC 8.6 only)

11 Sep 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