You're absolutely right that improvement doesn't solve your problem. But what I didn't say is that there is no real reason (I think) that we can't improve improvement to produce givens. This would likely require a change to the coercion language in Core (and thus not to be taken lightly), but if we can identify a class of programs that clearly benefits from that work, it is more likely to happen. The thoughts about improvement were just a very basic proof-of-concept. Sadly, the proof-of-concept failed, so I think a first step in this direction would be to somehow encode these partial improvements, and then work on changing Core. That road seems too long, though, so in the end, I think constrained type families (with superclass constraints) might be a more fruitful direction.
Richard > On Jan 5, 2020, at 6:02 PM, Alexis King <[email protected]> wrote: > >> On Jan 4, 2020, at 20:38, Richard Eisenberg <[email protected]> wrote: >> >> I thought that, maybe, we could use partial improvement to give you what you >> want > > I think that improvement alone cannot possibly be enough here, as improvement > by its nature does not provide evidence. Improvement allows us to take a set > of constraints like > > [G] FD2 a Bool > [W] FD2 a b > > and derive [WD] b ~ Bool, but importantly this does not produce a new given! > This only works if b is a metavariable, since we can solve the new wanted by > simply taking b := Bool, but if b is rigid, we are just as stuck as before. > In other words, improvement only helps resolve ambiguities, not derive any > new information. > > That’s why I think the “superclass” characterization is more useful. If > instead we express your FD2 class as > > class b ~ B a => FD2 a b where > type B a > > then if we have [G] FD2 a Bool, we can actually derive [G] B a ~ Bool, which > is much stronger than what we were able to derive using improvement. > > I imagine you are aware of all of the above already, but it’s not immediately > clear to me from your description why you need functional dependencies (and > therefore improvement) rather than this kind of approximation using > superclasses and type families. Would modeling things with that approximation > help at all? If not, why not? I think that would help me understand what > you’re saying a little better. > > Thanks, > Alexis _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
