[GHC] #14369: GHC warns an injective type family "may not be injective"

[GHC]

#14369: GHC warns an injective type family "may not be injective"
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  InjectiveFamilies                  |
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14369>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler