"No skolem info" panic (GHC 8.6 only)

The following program:

{-# 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
   |                                    ^^^^^^^

Trac metadata

Trac field	Value
Version	8.6.1-beta1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture