I codici di REBR. GHC devono essere di tipo preservativo?

Question

import Data.Void (Void,absurd) 

dire che ho un linguaggio piccolo termine:

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

Se voglio combinare i termini del tipo Term c Void e Term c Int, che dovrebbe essere possibile, dal momento che ho la garanzia che il primo termine non contiene qualsiasi variabile Pertanto, posso scrivere la funzione:

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

Tuttavia, sarebbe un peccato per eseguire effettivamente questa funzione, perché so per certo che in realtà non cambia nulla. È sicuro aggiungere i seguenti pragmi:

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

E questo effettivamente raggiungere il risultato desiderato?

Ci sono modi migliori per farlo?

Answer 1

No, questo non funzionerebbe. Le regole di riscrittura vengono applicate solo se i tipi controllano. In questo caso, la regola si attiva solo se hai eseguito castVar :: Term c Void -> Term c Void, che non è molto utile. (Vedi https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/rewrite-rules.html per maggiori informazioni sulle regole di riscrittura)

Quello che vuoi è forzare il tipo. È sicuro farlo perché sai che non c'è Void nello Term. È possibile farlo importando Unsafe.Coerce e castVar = unsafeCoerce o creareun'istanza di Functor (è possibile derivarlo per questa versione semplice) e utilizzare unsafeVacuous da Data.Void.Unsafe.