Lets say I have data type Expr a as defined in Types
And I have some parser, the details really don’t matter at all here.
The problem arises in my renamer module. The representation for Type is
exactly the same for both modules, yet I need boilerplate to convince the
typechecker. Does there exist some nice way to avoid this?
The problem is exaggerated for modules that modify the tree even less, e.g a desugar module.
I know syb helps with this if the
type of the tree is the same, but that is not the case here.
{-# LANGUAGE TypeFamilies #-}
module Types where
type Pos = (Int, Int)
data Rn
data Ps
data Expr a
= Var (XVar a) String
| Lam (XLam a) String (Type a) (Expr a)
| App (XApp a) (Expr a) (Expr a)
data Type a = Int (XInt a) | Fun (XFun a) (Type a) (Type a)
type family XVar a
type family XLam a
type family XApp a
type family XInt a
type family XFun a
{-# LANGUAGE TypeFamilies #-}
module Parse where
import Types
type instance XVar Ps = Pos
type instance XLam Ps = Pos
type instance XApp Ps = Pos
type instance XInt Ps = ()
type instance XFun Ps = ()
parse :: String -> Expr Ps
parse input = error "todo"
{-# LANGUAGE TypeFamilies #-}
module Rename where
import Types
import Parse ()
type instance XVar Rn = Pos
type instance XLam Rn = Pos
type instance XApp Rn = Pos
type instance XInt Rn = ()
type instance XFun Rn = ()
rename :: Expr Ps -> Expr Rn
rename expr = case expr of
Lam pos var ty body -> Lam pos var (boilerplate ty) (rename body)
App pos l r -> App pos (rename l) (rename r)
Var _ _ -> error "..."
boilerplate :: Type Ps -> Type Rn
boilerplate (Int field) = Int field
boilerplate (Fun field l r) = Fun field (boilerplate l) (boilerplate r)
The closest thing to an “improvement” that I can see for this situation (other than “just use the same type in the first place”) is a bit of unsafe magic:
coercibly
:: forall t1 t2 r
. (Coercible (XInt t1) (XInt t2), Coercible (XFun t1) (XFun t2))
=> (Coercible (Type t1) (Type t2) => r) -> r
coercibly r = case magic of Coercion -> r
where
magic :: Coercion (Type t1) (Type t2)
magic = unsafeCoerce refl
where
refl :: Coercion (Type t1) (Type t1)
refl = Coercion
Then you can bring the instance into scope where needed and use safe coercions:
rename :: Expr Ps -> Expr Rn
rename expr = coercibly case expr of
Lam pos var ty body -> Lam pos var (coerce ty) (rename body)
App pos l r -> App pos (rename l) (rename r)
Var _ _ -> error "..."
This avoids traversing the AST to rebuild it unchanged, though GHC optimisations might already be capable of that much.
Ideally you’d be able to mark the parameter to Type as representationalphantom, actually!, and that would signal to the compiler to infer a Coercible (Type a) (Type b) from (Coercible (XInt a) (XInt b), Coercible (XFun a) (XFun b)). But the docs say that arguments to type families must be nominal.
I don’t know if the existing roles for type families proposal covers this case exactly, but it seems in the same ballpark.
Extensions to the role system get pretty complicated. For cases like this, I think it would be plenty to partially lift the restriction on user-declared Coercible instances: let us standalone-derive them, with GHC throwing a compile error if it can’t prove representational equality from the constraints we supply.
I’d simply go for an unsafeCoerce-based solution such as @Leary’s. The pass parameter can’t really be phantom, because it is used in type families. besides, a coercebased solution is unlikely to be better than one based on unsafeCoerce if you know what you are doing. That is, if you think you should be allowed to use coerce, you can always use unsafeCoerce as well.