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`.
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
