[Ryan Scott:] In other words, this would work provided that you'd be willing to list every single instance of `HasSrcSpan` in its own COMPLETE set. It's tedious, but possible.
Yes, for the cases where `LL` is used monomorphically, we can use the per-instance COMPLETE pragma, but it does not scale to the generic cases where `LL` is used polymorphically. Consider the following where `Exp` and `Pat` are both instances of `HasSrcSpan`: {{{ {-# COMPLETE LL :: Exp #-} {-# COMPLETE LL :: Pat #-} unLocExp :: Exp -> Exp unLocExp (LL _ m) = m unLocPat :: Pat -> Pat unLocPat (LL _ m) = m unLocGen :: HasLoc a => a -> SrcSpanLess a unLocGen (LL _ m) = m }}} In the functions `unLocExp` and `unLocPat`, the related COMPLETE pragmas rightly avoid the false incomplete pattern matching warnings. However, to avoid the false incomplete pattern matching warning in `unLocGen`, either I should add a catch-all case `unLocGen _ = error "Impossible!"` or expose the internal view patterns and hence break the abstraction `unLocGen (decomposeSrcSpan->(_ , m)) = m` We want to avoid both solutions and unfortunately, this problem arises frequently enough. For example, in GHC, there are plenty of such generic cases (e.g., `sL1` or the like in the parser). I believe the source of the issue is what you just mentioned:
[Ryan Scott:] Complete sets of patterns must be identified relative to a type.
Technically `HasSrcSpan a0 |- a0` is a type, for a Skolem variable
`a0`; I understand if you mean relative to a concrete type, but I
don't understand why (I have no experience with GHC's totality checker
code).
Why can't it be syntactic? We should allow programmers to express
things like "when you see `LL` treat the related pattern matching
group as total".
/Shayan
On Thu, Oct 25, 2018 at 4:40 PM Ryan Scott
You *can* put `LL` into a COMPLETE set, but under the stipulation that you specify which type constructor it's monomorphized to. To quote the wiki page on COMPLETE sets:
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. The type constructor for the whole set of patterns is the type constructor as specified by the user. If the user does not provide a type signature then the definition is rejected as ambiguous.
This design is a consequence of the design of the pattern match checker. Complete sets of patterns must be identified relative to a type. This is a sanity check as users would never be able to match on all constructors if the set of patterns is inconsistent in this manner.
In other words, this would work provided that you'd be willing to list every single instance of `HasSrcSpan` in its own COMPLETE set. It's tedious, but possible.
Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#Typing _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs