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