如何在本地使用UndecidableInstances？

Question

是的,我知道这UndecidableInstances可能很糟糕.我真的很努力地设计我的模块,所以它不需要它但是我有这样的东西:

instance Foo x (C x y) => Bar (C x y) where

    ...

并且改变它会使API变得更加丑陋.我从来没有推出过Foo,Bar所以没有办法做出循环.

另一方面,UndecidableInstances使得愚蠢的错误容易被忽视.例如,我可以写错误的东西:

instance Foo x (C x z) => Bar (C x y) where

    ...

在那里z从来没有在右侧出现.

问题:是否可以UndecidableInstances在模块中本地使用,即明确标记解除通常终止规则的位置？

当然它对终止没有帮助,但它会让决定更加明智地使用这个扩展.

问题2:是否有一些弱于此的东西UndecidableInstances仍然不能保证终止,但会禁止更多的边界线情况,如第二个代码片段？

Answer 1

到目前为止，语言编译指示是针对每个模块的，因此第一个问题的答案是否定的。至于第二个问题，我不太确定，但我知道除了 UndecidableInstances 之外没有其他扩展允许该实例。

然而，UndecidableInstances 并没有那么糟糕，它只是允许类型检查器尝试解析无法证明终止的实例。不过，上下文堆栈阻止它实际上永远循环。