<div dir="ltr"><div>Hello,</div><div><br></div><div>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?</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div>{-# Language TypeInType, TypeFamilies #-}</div><div><br></div><div>module Help where</div><div><br></div><div>import Data.Kind</div><div><br></div><div>type family IxKind (m :: Type) :: Type</div><div>type family Value (m :: Type) :: IxKind m -> Type</div><div><br></div><div>data T (k :: Type) (f :: k -> Type)</div><div><br></div><div>type instance IxKind (T k f) = k</div><div>type instance Value (T k f) = f</div><div><br></div><div>{-</div><div>[1 of 1] Compiling Help             ( Desktop/Help.hs, interpreted )</div><div>Desktop/Help.hs:13:31: error:</div><div>    • Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’</div><div>    • In the type ‘f’</div><div>      In the type instance declaration for ‘Value’</div><div>   |</div><div>13 | type instance Value (T k f) = f</div><div>   |                               ^</div><div>Failed, no modules loaded.</div><div>-}</div></div>