[Agda] heterogeneous equality

[Dan Licata]

Is it possible to define heterogeneous equality in Agda?  I tried:

  data HId {A : Set} : {B : Set} -> A -> B -> Set where
    HRefl : {a : A} -> HId {A} {A} a a 

but I can't figure out how to use it.  

E.g., for a context- and object-language-type-indexed expression type
Tm, I want a congruence for the successor constructor:

  help : { G G' : Ctx} {e : Tm G nat} {e' : Tm G' nat} 
       -> HId e e' -> HId (Succ e) (Succ e')
  help {G} {.G} {e} {.e} HRefl = ?

But I can't seem to match the input equality with HRefl here:

  G != G' of type .lib.List.List.ListOpenInPrelude.List Tp
  when checking that the pattern HRefl has type HId e' e0

Any advice?

Thanks!
-Dan