Question about TypeInType

[Iavor Diatchki]

Hello,

I was experimenting with TypeInType and run into a problem, that can be
reduced to the following example.  Does anyone have any insight on what
causes the error, in particular why is `IxKind` not being reduced?

-Iavor


{-# Language TypeInType, TypeFamilies #-}

module Help where

import Data.Kind

type family IxKind (m :: Type) :: Type
type family Value (m :: Type) :: IxKind m -> Type

data T (k :: Type) (f :: k -> Type)

type instance IxKind (T k f) = k
type instance Value (T k f) = f

{-
[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )
Desktop/Help.hs:13:31: error:
    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’
    • In the type ‘f’
      In the type instance declaration for ‘Value’
   |
13 | type instance Value (T k f) = f
   |                               ^
Failed, no modules loaded.
-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180412/0df9af5c/attachment.html>