GHC warns an injective type family "may not be injective"

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

data family Sing (a :: k)

data instance Sing (z :: Maybe a) where
  SNothing :: Sing Nothing
  SJust :: Sing x -> Sing (Just x)

class SingKind k where
  type Demote k = r | r -> k
  fromSing :: Sing (a :: k) -> Demote k

instance SingKind a => SingKind (Maybe a) where
  type Demote (Maybe a) = Maybe (Demote a)
  fromSing SNothing = Nothing
  fromSing (SJust x) = Just (fromSing x)

f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing

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

Bug.hs:26:5: error:
    • Couldn't match type ‘Demote a’ with ‘Demote a1’
      Expected type: Sing (x a) -> Maybe (Demote a1)
        Actual type: Sing (x a) -> Demote (Maybe a)
      NB: ‘Demote’ is a type function, and may not be injective
    • In the expression: fromSing
      In an equation for ‘f’: f = fromSing
    • Relevant bindings include
        f :: Sing (x a) -> Maybe (Demote a1) (bound at Bug.hs:26:1)
   |
26 | f = fromSing
   |     ^^^^^^^^

That NB: ‘Demote’ is a type function, and may not be injective suggestion shouldn't be shown here, since Demote is definitely injective.

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