强制静态地完成一元计算

Question

在Matthew Pickering 的关于内联的博客文章中，他提到了一个技巧来强制 GHC 内联应用于静态已知参数的递归定义：

然而，有一个技巧可以用来告诉 GHC 一个参数是真正静态的。我们用类型参数替换值参数。然后通过定义合适的类型类实例，我们可以像对普通值一样递归类型的结构。然而这一次，GHC 会很高兴地内联每个“递归”调用，因为对 sum 的每个调用都是不同的类型。

然后博客文章继续展示一个使用类型级别Nat的非常简单的例子。我的问题是强制 GHC 在实际有趣的类型上完全内联函数。

就我而言，我有一个通过 monadic DSL 进行的计算。在幕后，DSL 是一个RWS. 查看带有大量INLINE编译指示的生成的 Core ，我可以看到<>对为编写器输出实现的递归函数的调用。由于这些函数是递归的，GHC 不会内联它们。但如果是这样，由于完整的 RWS 计算足够静态，编写器输出的脊椎可以在编译期间完全展开，它会在有限的多个步骤后到达 Core，而没有留下任何递归定义。

从 Matt 的博客文章中获取想法，我们需要对 monadic 值进行类型级别的表示；我很想看到这样的版本（特别是具有良好的人体工程学！），但我并不太乐观：与 Servant 方法不同，我们需要一种将变量绑定到结果的方法（a la monadic >>=）。或者，是否有任何其他机制可以告诉 GHC 它的输入大小是静态已知的，因此它不应该回避积极地内联递归定义？例如，是否可以通过在索引中使用具有适当大小度量的分级 monad来模拟 Agda 样式的大小类型？

Ps：我的目标不仅仅是优化，而是解决 Clash 错误，因此通过积极的内联消除递归定义需要是可靠的，而不是一个很好的性能改进。