Make type indices take local constraints into account in type instance declaration
Given
infixl 1 :$
infixr :->
data Sig x where
Full :: a -> Sig a
(:->) :: a -> Sig a -> Sig a
data AST dom a where
Sym :: dom a -> AST dom a
(:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b
class Syntactic a dom | a -> dom where
type Rep a
desugar :: a -> AST dom (Full (Rep a))
sugar :: AST dom (Full (Rep a)) -> a
I want to be able to define the trivial instance for Syntactic (AST dom (Full a))
:
instance Syntactic (AST dom (Full a)) dom where
type Rep (AST dom (Full a)) = a
desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
desugar = id
sugar = id
This should be the only Syntactic
instance for AST _ _
so I would like to apply the ‘constraint’ trick (link) but I cannot use the Rep
instance as before:
-- • Type indexes must match class instance head
-- Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’
-- • In the type instance declaration for ‘Rep’
-- In the instance declaration for ‘Syntactic (AST dom full_a) dom’
instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
type Rep (AST dom (Full a)) = a
Maybe this could be accepted, given that full_a ~ Full a
, therefore the instance head is equal to AST dom (Full a)
?
My current workaround is using a type family
type family
Edrú a where
Edrú (Full a) = a
instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
type Rep (AST dom full_a) = Edrú full_a
desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
desugar = id
sugar = id