Hi Edward, I'd expect (1) to work after fixing #14422/#18276. (3) might have been https://gitlab.haskell.org/ghc/ghc/-/issues/16682, so it should be fixed nowadays. (2) is a neat idea, but requires a GHC proposal I'm not currently willing to get into. I can also see a design discussion around allowing arbitrary "formulas" (e.g., not only what is effectively CNF). A big bonus of your design is that it's really easy to integrate into the current implementation, which is what I'd gladly do in case such a proposal would get accepted.
Cheers Sebastian Am Di., 1. Sept. 2020 um 00:26 Uhr schrieb Edward Kmett <ekm...@gmail.com>: > I'd be over the moon with happiness if I could hang COMPLETE pragmas on > polymorphic types. > > I have 3 major issues with COMPLETE as it exists. > > 1.) Is what is mentioned here: > > Examples for me come up when trying to build a completely unboxed 'linear' > library using backpack. In the end I want/need to supply a pattern synonym > that works over, say, all the 2d vector types, extracting their elements, > but right now I just get spammed by incomplete coverage warnings. > > type family Elem t :: Type > class D2 where > _V2 :: Iso' t (Elem t, Elem t) > > pattern V2 :: D2 t => Elem t -> Elem t -> t > pattern V2 a b <- (view _V2 -> (a,b)) where > V2 a b = review _V2 (a,b) > > There is no way to hang a COMPLETE pragma on that. > > 2.) Another scenario that I'd really love to see supported with COMPLETE > pragmas is a way to use | notation with them like you can with MINIMAL > pragmas. > > If you make smart constructors for a dozen constructors in your term type > (don't judge me!), you wind up needing 2^12 COMPLETE pragmas to describe > all the ways you might mix regular and start constructors today. > > {# COMPLETE (Lam | LAM), (Var | VAR), ... #-} > > would let you get away with a single such definition. This comes up when > you have some kind of monoid that acts on terms and you want to push it > down through > the syntax tree invisibly to the user. Explicit substitutions, shifts in > position in response to source code edits, etc. > > 3.) I had one other major usecase where I failed to be able to use a > COMPLETE pragma: > > type Option a = (# a | (##) #) > > pattern Some :: a -> Option a > pattern Some a = (# a | #) > > pattern None :: Option a > pattern None = (# | (##) #) > > {-# COMPLETE Some, None #-} > > These worked _within_ a module, but was forgotten across module > boundaries, which forced me to rather drastically change the module > structure of a package, but it sounds a lot like the issue being discussed. > No types to hang it on in the interface file. With the ability to define > unlifted newtypes I guess this last one is less of a concern now? > > -Edward > > On Mon, Aug 31, 2020 at 2:29 PM Richard Eisenberg <r...@richarde.dev> > wrote: > >> Hooray Sebastian! >> >> Somehow, I knew cluing you into this conundrum would help find a >> solution. The approach you describe sounds quite plausible. >> >> Yet: types *do* matter, of course. So, I suppose the trick is this: have >> the COMPLETE sets operate independent of types, but then use types in the >> PM-checker when determining impossible cases? And, about your idea for >> having pattern synonyms store pointers to their COMPLETE sets: I think data >> constructors can also participate. But maybe there is always at least one >> pattern synonym (which would be a reasonable restriction), so I guess you >> can look at the pattern-match as a whole and use the pattern synonym to >> find the relevant COMPLETE set(s). >> >> Thanks for taking a look! >> Richard >> >> On Aug 31, 2020, at 4:23 PM, Sebastian Graf <sgraf1...@gmail.com> wrote: >> >> Hi Richard, >> >> Am Mo., 31. Aug. 2020 um 21:30 Uhr schrieb Richard Eisenberg < >> r...@richarde.dev>: >> >>> Hi Sebastian, >>> >>> I enjoyed your presentation last week at ICFP! >>> >> >> Thank you :) I'm glad you liked it! >> >> This thread ( >>> https://ghc-devs.haskell.narkive.com/NXBBDXg1/suppressing-false-incomplete-pattern-matching-warnings-for-polymorphic-pattern-synonyms) >>> played out before you became so interested in pattern-match coverage. I'd >>> be curious for your thoughts there -- do you agree with the conclusions in >>> the thread? >>> >> >> I vaguely remember reading this thread. As you write there >> <https://ghc-devs.haskell.narkive.com/NXBBDXg1/suppressing-false-incomplete-pattern-matching-warnings-for-polymorphic-pattern-synonyms#post9> >> >> And, while I know it doesn't work today, what's wrong (in theory) with >>> >>> {-# COMPLETE LL #-} >>> >>> No types! (That's a rare thing for me to extol...) >>> >>> I feel I must be missing something here. >>> >> >> Without reading the whole thread, I think that solution is very possible. >> The thread goes on to state that we currently attach COMPLETE sets to type >> constructors, but that is only an implementational thing. I asked Matt (who >> implemented it) somewhere and he said the only reason to attach it to type >> constructors was because it was the easiest way to implement serialisation >> to interface files. >> >> The thread also mentions that type-directed works better for the >> pattern-match checker. In fact I disagree; we have to thin out COMPLETE >> sets all the time anyway when new type evidence comes up, for example. It's >> quite a hassle to find all the COMPLETE sets of the type constructors a >> given type can be "represented" (I mean equality modulo type family >> reductions here) as. I'm pretty sure it's broken in multiple ways, as >> #18276 <https://gitlab.haskell.org/ghc/ghc/-/issues/18276> points out. >> >> Disregarding a bit of busy work for implementing serialisation to >> interface files, it's probably far simpler to give each COMPLETE set a >> Name/Unique and refer to them from the pattern synonyms that mention them >> (we'd have to get creative for orphans, though). The relation is quite like >> between a type class instance and the type in its head. A more worked >> example is here: >> https://gitlab.haskell.org/ghc/ghc/-/issues/18277#note_287827 >> >> So, it's on my longer term TODO list to fix this. >> >> >>> My motivation for asking is https://github.com/conal/linalg/pull/54 >>> (you don't need to read the whole thing), which can be boiled down to a >>> request for a COMPLETE pragma that works at a polymorphic result type. (Or >>> a COMPLETE pragma written in a module that is not the defining module for a >>> pattern synonym.) https://gitlab.haskell.org/ghc/ghc/-/issues/14422 >>> describes a similar, but even more challenging scenario. >>> >> >> I'll answer in the thread. (Oh, you also found #14422.) I think the >> approach above will also fix #14422. >> >>> >>> Do you see any ways forward here? >>> >> . >> >>> >>> Thanks! >>> Richard >> >> >> Maybe I'll give it a try tomorrow. >> >> >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs