GHC REWRITE pragma必须保持类型吗？

Question

import Data.Void (Void,absurd)

说我有一个小语言:

data Term c v where
  Var :: v               -> Term c v
  Con :: c -> [Term c v] -> Term c v

如果我要的类型的术语结合Term c Void和Term c Int,这应该是可能的,因为我有第一项不包含任何变量的保证.因此,我可以编写函数:

castVar :: Term c Void -> Term c v
castVar (Var i   ) = absurd i
castVar (Con x xs) = Con x (map castVar xs)

然而,实际运行这个函数真是太遗憾了,因为我知道它实际上并没有改变任何东西.添加以下编译指示是否安全:

{-# NOINLINE castVar #-}
{-# RULES "castVar/id" forall x. castVar x = x; #-}

这会实际达到预期的效果吗？

有更好的方法吗？

Answer 1

不,这不行.只有在检查类型时才会应用重写规则.在这种情况下,规则只会在您运行时触发castVar :: Term c Void -> Term c Void,这不是很有帮助.(有关重写规则的更多信息,请参阅https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/rewrite-rules.html)

你想要的是强迫这种类型.它的安全要做到这一点,因为你知道有没有Void的Term.您可以通过导入做到这一点Unsafe.Coerce,并castVar = unsafeCoerce或作出Term的一个实例Functor(你可以得到它为这个简单的版本),并使用unsafeVacuous从Data.Void.Unsafe.