28 Mar
2018
28 Mar
'18
11:37 a.m.
On Tue, Mar 27, 2018 at 6:24 AM, Joachim Breitner
2. The distinction between existentials and universals is oddly abrupt.
This is a good point. In addition to what Joachim said, universals can also depend on existentials which I find weird. As an aside, here is one corner case which I don't think is handled in the proposal: data T a where MkT :: forall a. T a 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. Roman