[Haskell-cafe] Partial type family application

[mniip]

On Wed, Apr 26, 2017 at 10:58:10AM -0400, Richard Eisenberg wrote:
> The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in.

I'm reading your thesis, and in it you propose to make all -> arrows
unmatchable, and all constructors automagically get '-> arrows.

Naturally, if we implement just this type extension, then it'd make
sense to leave the -> arrow as is and introduce an ~> unmatchable arrow.
However this makes transition to fully dependent arrows even more
awkward.

On the other hand we would have to pull the implicit '-> constructor
arrows into this proposal, which makes it not so independent from
dependent types, so still awkward.

What do you think should be done?

--mniip