When I define type synonyms I typically erase them as 0 Foo : Type. If there are parameters to that synonym, I can also erase those, like

0 Foo : (0 _ : Nat) -> (0 _ : Type) -> Type

but what does that mean? Since Foo doesn't exist at runtime, nothing it's passed needs to exist at runtime either. We can see this by defining a similar example without erased args

0 Foo' : Nat -> Type -> Type

and defining Foo in terms of Foo'

Foo x a = Foo' x a

which compiles fine. Is there any purpose to erasing arguments to erased functions?