Skolem escape at the kind level

This program should be rejected

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE KindSignatures #-}

module Foo2 where

import Data.Kind ( Type )
import Data.Type.Equality
import Data.Proxy
import GHC.Exts

data SameKind :: k -> k -> Type

f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
                       g = undefined
                   in ()

But

• 8.0 rejects it, with an unhelpful message
• 8.2 accepts it, and the result satisfies Core Lint
• HEAD accepts it, and produces a Core Lint Error