<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Tue, Mar 27, 2018 at 6:24 AM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
2. The distinction between existentials and universals is oddly abrupt.<br></blockquote><div><br></div><div>This is a good point. In addition to what Joachim said, universals can also depend on existentials which I find weird.</div><div><br></div><div>As an aside, here is one corner case which I don't think is handled in the proposal:</div><div><br></div><div>data T a where</div><div>  MkT :: forall a. T a</div><div><br></div><div>With -XPolyKinds, the type inferred for T is forall k (a :: k). T a. Now, k is an existential but can it be bound in a pattern? The proposal only mentions 2 cases: no forall and a forall that mentions all type variables and neither applies here.</div><div><br></div><div>Roman</div><div><br></div><div><br></div></div></div></div>