[GHC] #13790: GHC doesn't reduce type family in kind signature unless its arm is twisted

[GHC]

#13790: GHC doesn't reduce type family in kind signature unless its arm is twisted
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's some code (inspired by Richard's musings
 [https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297
 here]) which typechecks with GHC 8.2.1 or HEAD:

 {{{#!hs
 {-# 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:

 {{{#!hs
 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:

 {{{#!hs
 ...

 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.

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