Wildcards in type synonyms

[ÉRDI Gergő]

In case anyone's still interested, Atze Dijkstra and I have come up with 
an alternative approach to implementing this which requires changing much 
fewer moving parts.

The idea is to internally regard `type MySyn a = T[_, a, _]` as
`type MySyn w1 w2 a = T[w1, a, w2]`, recording in `SynTyCon` that we'll 
need to synthesize 2 wildcard argument; then, during typechecking of 
occurrences, `MySyn` gets expanded into `MySyn _ _`. This is basically a 
simplified version of what languages with implicit parameters do --
in Agda syntax, we'd have

     MySyn : {w1 : Type} {w2 : Type} (a : Type) -> Type

and the application `MySyn A` is short-hand for `MySyn {w1 = _} {w2 = _} A`.

Of course, for a robust implementation, we can't just put all these 
implicit parameters up front, because they can form a telescope with 
other parameters; but, because type synonym applications need to be 
saturated anyway, I think even that could be implemented without 
complicated impredicativity decisions, simply by storing a bit more than 
just a single natural number as the extra info in `SynTyCon`.