Should GHC REWRITE pragmas save type?

Question

import Data.Void (Void,absurd) 

Let's say I have a little language of terms:

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

If I want to combine terms like Term c Void and Term c Int , this should be possible, since I have a guarantee that the first member does not contain any variables. So I can write a function:

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

However, it would be a shame to actually run this function, since I know that nothing really changes. Is it possible to add the following pragmas:

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

And will it really achieve the desired result?

Are there any better ways to do this?

Answer 1

No, that will not work. Rewrite rules apply only to type checking. In this case, the rule will only work when castVar :: Term c Void -> Term c Void started, which is not very useful. (See https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/rewrite-rules.html for more information on rewriting rules)

What you want is type coercion. This is safe because you know that there is no Void in Term . You can either do this by importing Unsafe.Coerce and castVar = unsafeCoerce , or make a Term instance of the Functor (you can get it for this simple version) and use unsafeVacuous from Data.Void.Unsafe .