TypeApplications-related GHC internal error

This is reproducible with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce

class MFunctor t where
    hoist :: (Monad m) => (forall a . m a -> n a) -> t m b -> t n b

newtype TaggedTrans tag trans m a = TaggedTrans (trans m a)

instance MFunctor trans => MFunctor (TaggedTrans tag trans) where
 hoist = coerce
          @(forall (m :: * -> *)
                   (n :: * -> *)
                   (b :: k).
            Monad m =>
            (forall (a :: *).
             m a -> n a)
            -> trans m b -> trans n b)
          @(forall (m :: * -> *)
                   (n :: * -> *)
                   (b :: k).
            Monad m =>
            (forall (a :: *).
             m a -> n a)
            -> TaggedTrans tag trans m b
               -> TaggedTrans tag trans n b)
          hoist

GHCi, version 8.3.20170516: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:18:26: error:
    • GHC internal error: ‘k’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a1tR :-> Type variable ‘m’ = m,
                               a1tS :-> Type variable ‘n’ = n, a1tT :-> Type variable ‘b’ = b,
                               a1tV :-> Type variable ‘trans’ = trans,
                               a1tW :-> Type variable ‘tag’ = tag, a1tX :-> Type variable ‘m’ = m,
                               a1tY :-> Type variable ‘n’ = n, a1KE :-> Type variable ‘k’ = k,
                               a1KF :-> Type variable ‘k’ = k]
    • In the kind ‘k’
      In the type ‘(forall (m :: * -> *) (n :: * -> *) (b :: k).
                    Monad m =>
                    (forall (a :: *). m a -> n a) -> trans m b -> trans n b)’
      In the expression:
        coerce
          @(forall (m :: * -> *) (n :: * -> *) (b :: k).
            Monad m => (forall (a :: *). m a -> n a) -> trans m b -> trans n b)
          @(forall (m :: * -> *) (n :: * -> *) (b :: k).
            Monad m =>
            (forall (a :: *). m a -> n a)
            -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b)
          hoist
   |
18 |                    (b :: k).
   |                          ^

Trac metadata

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