GHC doesn't reduce type family in kind signature unless its arm is twisted

Here's some code (inspired by Richard's musings here) which typechecks with GHC 8.2.1 or HEAD:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data family Sing (a :: k)

data SomeSing (k :: Type) where
  SomeSing :: Sing (a :: k) -> SomeSing k

type family Promote k :: Type

class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing :: Demote k -> SomeSing k

type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a

type instance Promote Type = Type

instance SingKind Type where
  type Demote Type = Type
  fromSing = error "fromSing Type"
  toSing   = error "toSing Type"

-----

data N = Z | S N

data instance Sing (z :: N) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)
type instance Promote N = N

instance SingKind N where
  type Demote N = N
  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)
  toSing Z = SomeSing SZ
  toSing (S n) = case toSing n of
                   SomeSing sn -> SomeSing (SS sn)

Things get more interesting if you try to add this type instance at the end of this file:

type instance DemoteX (n :: N) = n

Now GHC will complain:

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

Bug.hs:49:34: error:
    • Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
    • In the type ‘n’
      In the type instance declaration for ‘DemoteX’
   |
49 | type instance DemoteX (n :: N) = n
   |                                  ^

That error message smells funny, since we do have a type family instance that says Demote N = N! In fact, if you use Template Haskell to split up the declarations manually:

...

instance SingKind N where
  type Demote N = N
  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)
  toSing Z = SomeSing SZ
  toSing (S n) = case toSing n of
                   SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n

Then the file typechecks without issue.

Trac metadata

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