I also realised the COMPLETE pragmas are even less helpful (at least for my case mentioned above) as they cannot be used when orphaned. For example, I tried to follow the partial solution of introducing multiple COMPLETE pragmas, one per a concrete instance of `HasSrcSpan`. I defined the pattern synonym `LL` in `basicTypes/SrcLoc.hs` and wanted to naturally define a COMPLETE pragma for when `LL` is used for `Pat` in `hsSyn/HsPat.hs`. I got an error complaining about orphaned COMPLETE pragmas. The only unacceptable way (that I can see) that makes it work is to have a module defining `LL`, importing all the instances of `HasSrcSpan`, and all the COMPLETE pragmas (one per instance).
I have made a ticket about the original concern here: https://ghc.haskell.org/trac/ghc/ticket/15885 Until we come up with a good and general solution to this ticket, do you know of a hack to suppress the false incomplete pattern matching warnings in GHC? Should we add clauses like `foo _ = panic "Impossible! How did you manage to bypass a complete matching?"`? /Shayan On Mon, 29 Oct 2018 at 14:52, Sylvain Henry <sylv...@haskus.fr> wrote: > > I've just found this related ticket: > https://ghc.haskell.org/trac/ghc/ticket/14422 > > > On 10/26/18 7:04 PM, Richard Eisenberg wrote: > > Aha. So you're viewing complete sets as a type-directed property, where we > can take a type and look up what complete sets of patterns of that type might > be. > > Then, when checking a pattern-match for completeness, we use the inferred > type of the pattern, access its complete sets, and if these match up. > (Perhaps an implementation may optimize this process.) > > What I like about this approach is that it works well with GADTs, where, > e.g., VNil is a complete set for type Vec a Zero but not for Vec a n. > > I take back my claim of "No types!" then, as this does sound like it has the > right properties. > > For now, I don't want to get bogged down by syntax -- let's figure out how > the idea should work first, and then we can worry about syntax. > > Here's a stab at a formalization of this idea, written in metatheory, not > Haskell: > > Let C : Type -> Set of set of patterns. C will be the lookup function for > complete sets. Suppose we have a pattern match, at type tau, matching against > patterns Ps. Let S = C(tau). S is then a set of sets of patterns. The > question is this: Is there a set s in S such that Ps is a superset of s? If > yes, then the match is complete. > > What do we think of this design? Of course, the challenge is in building C, > but we'll tackle that next. > > Richard > > On Oct 26, 2018, at 5:20 AM, Sylvain Henry <sylv...@haskus.fr> wrote: > > Sorry I wasn't clear. I'm not an expert on the topic but it seems to me that > there are two orthogonal concerns: > > 1) How does the checker retrieve COMPLETE sets. > > Currently it seems to "attach" them to data type constructors (e.g. Maybe). > If instead it retrieved them by matching types (e.g. "Maybe a", "a") we could > write: > > {-# COMPLETE LL #-} > > From an implementation point of view, it seems to me that finding complete > sets would become similar to finding (flexible, overlapping) class instances. > Pseudo-code: > > class Complete a where > conlikes :: [ConLike] > instance Complete (Maybe a) where > conlikes = [Nothing @a, Just @a] > instance Complete (Maybe a) where > conlikes = [N @a, J @a] > instance Complete a where > conlikes = [LL @a] > ... > > > 2) COMPLETE set depending on the matched type. > > It is a thread hijack from me but while we are thinking about refactoring > COMPLETE pragmas to support polymorphism, maybe we could support this too. > The idea is to build a different set of conlikes depending on the matched > type. Pseudo-code: > > instance Complete (Variant cs) where > conlikes = [V @c | c <- cs] -- cs is a type list > > (I don't really care about the pragma syntax) > > Sorry for the thread hijack! > Regards, > Sylvain > > > On 10/26/18 5:59 AM, Richard Eisenberg wrote: > > I'm afraid I don't understand what your new syntax means. 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. > > Thanks, > Richard > > On Oct 25, 2018, at 12:24 PM, Sylvain Henry <sylv...@haskus.fr> wrote: > > > In the case where all the patterns are polymorphic, a user must > > provide a type signature but we accept the definition regardless of > > the type signature they provide. > > Currently we can specify the type *constructor* in a COMPLETE pragma: > > pattern J :: a -> Maybe a > pattern J a = Just a > > pattern N :: Maybe a > pattern N = Nothing > > {-# COMPLETE N, J :: Maybe #-} > > > Instead if we could specify the type with its free vars, we could refer to > them in conlike signatures: > > {-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-} > > The COMPLETE pragma for LL could be: > > {-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-} > > > I'm borrowing the list comprehension syntax on purpose because it would allow > to define a set of conlikes from a type-list (see my request [1]): > > {-# COMPLETE [ V :: (c :< cs) => c -> Variant cs > | c <- cs > ] :: Variant cs > #-} > > > To make things more formal, when the pattern-match checker > > requests a set of constructors for some data type constructor T, the > > checker returns: > > > > * The original set of data constructors for T > > * Any COMPLETE sets of type T > > > > Note the use of the phrase *type constructor*. The return type of all > > constructor-like things in a COMPLETE set must all be headed by the > > same type constructor T. Since `LL`'s return type is simply a type > > variable `a`, this simply doesn't work with the design of COMPLETE > > sets. > > Could we use a mechanism similar to instance resolution (with > FlexibleInstances) for the checker to return matching COMPLETE sets instead? > > --Sylvain > > > [1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html > > _______________________________________________ > 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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs