Hi, Am Mittwoch, den 02.05.2018, 14:10 -0400 schrieb Richard Eisenberg:
OK -- I could agree with forbidding braces on `data` (given that the GADT-syntax alternative exists), but what about `class`? And then if we allow it on `class`, it seems a bit silly not to do the analogous thing on `data`. (Note that the proposal currently describes the same scheme as I have described in this email thread, but only about `class`.)
Indeed, and the Unresolved questions go into some detail here. It still is a bit weird to have `C {a}` affect _not_ C but _only_ the methods, but since that is the only place where {a} appears, it is hard to avoid. Your solution for C is to say: Write a kind signature, i.e. if I write class C {k} (a : k) where meth :: a and I want the {k} to be also inferred in C’s kind, I have to write type C :: forall {k}. k -> Constraint By a similar reasoning one could expect the user, if they want to change the specificity of meth, to write out the its full type signature separately: class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint This would even allow more fine-grained control: You get to choose for each meth what the specificity is. In a way, that is similar to Coq’s [Arguments] command, which changes specificity after-the-fact. And we already have something similar in Haskell: role annotations. So maybe another alternative is to say class C k (a : k) where meth :: a specificity meth inferred specified (The rambliness of this mail is an indication that the proposal does not immediately resonates as the obvious right and best solution with me…) Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/