如何调试类型级程序

我正在尝试进行一些类型级别的编程，但它不起作用。我正在绞尽脑汁地试图弄清楚为什么 GHC 完全无法推断出我想要的类型签名。

有什么方法可以制作GHC吗tell me它在做什么？

I tried -ddump-tc，它只打印出最终的类型签名。 （是的，他们错了。谢谢，我已经知道了。）

我也尝试过-ddump-tc-trace，它会转储出大约 70KB 难以理解的乱码。 （特别是，我看不到任何提到的用户编写的标识符anywhere.)

我的代码是so close工作，但不知何故，一个额外的类型变量不断出现。由于某种原因，GHC 无法看到该变量应该被完全确定。确实，如果我manually写下五英里类型的签名，GHC 很高兴地接受了。所以我显然只是在某个地方缺少一个约束......但是哪里？！？>_

正如评论中提到的，用 :kind 和 :kind! 来探索一下！在 GHCi 中通常是我这样做的方式，但令人惊讶的是，将函数放置在哪里也很重要，而且看起来应该是相同的，但事实并非总是如此。

例如，我试图为个人项目制作一个等价的依赖类型函子，它看起来像

class IFunctor f where 
  ifmap :: (a -> b) -> f n a -> f n b 

我正在写这个例子

data IEither a n b where 
  ILeft :: a -> IEither a Z b 
  IRight :: b -> IEither a (S n) b 

我想，这应该相当简单，只需忽略左侧情​​况下的 f ，将其应用于右侧即可。

I tried

instance IFunctor (IEither a) where
  ifmap _ l@(ILeft _) = l 
  ifmap f (IRight r) = IRight $ f r

但对于本例中 ifmap 的专门版本是ifmap :: (b -> c) -> IEither a Z b -> IEither a Z c，Haskell 推断 l 的类型为IEither a Z b在 LHS 上，这是有道理的，但后来拒绝生产b ~ c.

所以，我必须解开 l，获取类型 a 的值，然后重新包装它以获得IEither a Z c.

这不仅适用于依赖类型，也适用于 n 级类型。 例如，我试图将适当形式的同构转换为自然变换，我认为这应该相当容易。

显然，我必须将解构函数放在函数的 where 子句中，否则类型推断将无法正常工作。