GHC internal error: "not in scope during TC but it passed the renamer"

{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds #-}

import Type.Reflection
import Data.Kind

data Dict c where Dict :: c => Dict c

asTypeable :: TypeRep a -> Dict (Typeable a)
asTypeable rep =
  withTypeable rep
    Dict

pattern Typeable :: () => Typeable a => TypeRep a
pattern Typeable <- (asTypeable -> Dict) 
  where Typeable = typeRep

data N = O | S N

type SN = (TypeRep :: N -> Type)

pattern SO = (Typeable :: TypeRep (O::N))

pattern SS :: 
     forall (t :: k').
     () 
  => forall (a :: kk -> k') (n :: kk). 
     (t ~ a n)
  => 
  TypeRep n -> TypeRep t 
pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k')) n)

fails with **GHC internal error**

$ ghci -ignore-dot-ghci Bug.hs 
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:31:47: error:
    • GHC internal error: ‘kk’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a1Ao :-> Type variable ‘k'’ = k' :: *,
                               a1Aq :-> Type variable ‘t’ = t :: k',
                               a1Hs :-> Type variable ‘a’ = a :: k0,
                               r1v4 :-> Identifier[asTypeable::forall k (a :: k).
                                                               TypeRep a
                                                               -> Dict (Typeable a), TopLevelLet]]
    • In the kind ‘kk -> k'’
      In the first argument of ‘TypeRep’, namely ‘(a :: kk -> k')’
      In the type ‘TypeRep (a :: kk -> k')’
   |
31 | pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k')) n)
   |                                               ^^
Failed, 0 modules loaded.
Prelude> 

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture