Search code examples
haskellghcpragma

Do GHC REWRITE pragmas have to be type preserving?

import Data.Void (Void,absurd)

Say I have a small term language:

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

If I want to combine terms of the type Term c Void and Term c Int, that should be possible, since I have the guarantee that the first term does not contain any variables. Therefore, I can write the function:

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

However, it'd be a shame to actually run this function, since I know for a fact that it doesn't actually change anything. Is it safe to add the following pragmas:

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

And will this actually achieve the desired result?

Are there better ways of doing this?

Solution

  • No, this wouldn't work. Rewrite rules are only applied if the types check. In this case the rule would only fire if you ran castVar :: Term c Void -> Term c Void, which isn't very helpful. (See https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/rewrite-rules.html for more info on rewrite rules)

    What you want is to coerce the type. It's safe to do this because you know there's no Void in the Term. You could either do this by importing Unsafe.Coerce and castVar = unsafeCoerce or make Term an instance of Functor (you can derive it for this simple version) and use unsafeVacuous from Data.Void.Unsafe.