GHC-inferred type signature doesn't actually typecheck

This code typechecks:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *

data Sigma (a :: *) :: (a ~> *) -> * where
  MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
             Sing x -> Apply p x -> Sigma a p

data instance Sing (z :: Sigma a p) where
  SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)

I was curious to know what the full type signature of SMkSigma was, so I asked GHCi what the inferred type is:

λ> :i SMkSigma
data instance Sing z where
  SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
                                                       x) (px :: Apply p x).
              (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)

I attempted to incorporate this newfound knowledge into the program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *

data Sigma (a :: *) :: (a ~> *) -> * where
  MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
             Sing x -> Apply p x -> Sigma a p

data instance Sing (z :: Sigma a p) where
  SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).
              Sing sx -> Sing px -> Sing (MkSigma sx px)

But to my surprise, adding this inferred type signature causes the program to no longer typecheck!

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

Bug.hs:23:31: error:
    • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
    • In the first argument of ‘Sing’, namely ‘px’
      In the type ‘Sing px’
      In the definition of data constructor ‘SMkSigma’
   |
23 |               Sing sx -> Sing px -> Sing (MkSigma sx px)
   |                               ^^

I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.

Trac metadata

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