So this stuff isn’t my biggest priority either, which would probably be GHC modularity and build system concerns, but I can only beat that drum so hard without pissing everyone off. In other words, I don’t think I am taking away energy from that my first priorities, but spending energy I would otherwise be blocked spending at all by focusing on more things at once, does that make sense? (For similar reasons, I work on Haskell and Nix things in parallel also.)
I am trying to do this GHC Proposal 448 amending stuff because I think it is is good for Depenent Haskell and (more importantly) it will clean up the language for those that don’t even care about new expressive power.
(Probably the most exciting part for me would actually be deprecating type families; I am quite annoyed about how they work today, and have worked on projects in Haskell which us authors collectively decided to put on hiatus because the language wasn’t good enough (which I personally think was in large part frictions from type families).)
The variable binding rules for pattern signatures indeed have nothing directly to do with signature patterns (though the fact that type families having capitalized names being dubious might bring the two topics closer together), but I view this stuff a puzzle where it takes a number of fine adjustments to get to where we want with a new design that is still coherent. The journey is quite complex!
The build system and modularity stuff that I said was my first priority itself isn’t the end goal either. Really, I don’t like working on end goals much because by the time the benefits are obvious it’s usually much easier to find volunteers. I like instead working on these “yak shaves of yak shaves” where the plot is not at all clear, but far fewer people are interested and thus it seems like me doing or not doing the thing has much greater impact.
(To add more perspective, if the modularity of GHC was really good, I honestly believe @int-index and the other good folks working on DH could just go bang out a pretty complete DH prototype with less work, and then the proposal process could be about reconciling a fork which would make the big picture much clearer. Instead, it is too difficult to just make the thing, and so we have to design and implement as we go, which makes it easy to get snagged on various bikeshed level things, and meanwhile there is no working protoype. So ideally the modularity stuff could just be done first, and then modularity + DH would be less work over all; but it is infeasible to just have the DH work stop and wait for a number of perfectly valid/understandable reasons, so then both much precede in parallel.
@int-index had a blog post a while back which discussed "should we do Dependent Haskell or just work on Agda, with the observation that actually those things converge in that it is easier to compile Agda to a more powerful and similar Haskell than an older Haskell. I think that’s correct, and it is a somewhat related observation. A GHC family of libraries that supports a number of different frontend and backends would be a very powerful piece of software, made wiser by more perspectives, and prevented from “overfitting” any one of them. SPJ himself has similarly long wanted Core to work perfectly well for Strict or Lazy languages.)