Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types

On our work on the new front-end AST for GHC based on TTG, we would like to use a pattern synonym similar to the following:

pattern LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
pattern LL s m <- (decomposeSrcSpan -> (m , s))
  where
        LL s m =  composeSrcSpan (m , s)

We know that any match on LL patterns, makes the pattern matching total, as it uses a view pattern with a total output pattern (i.e., in decomposeSrcSpan -> (m , s), the pattern (m , s) is total).

As far as I understand, currently COMPLETE pragmas cannot be used with such a polymorphic pattern synonym. I believe we need to enhance COMPLETE pragmas to support such pattern synonyms.

This can be done either syntactically, or (preferably) type-directed.

For example, we should be able to write {-# COMPLETE LL #-} or {-# COMPLETE LL :: HasSrcSpan a => a #-}.

In the type-directed approach a. the totality checker *may* need to track, at least, the set of required constraints of pattern synonyms mentioned in a COMPLETE pragma; and b. the order of pattern synonyms mentioned in a pragma should be taken into account (as noted by @carter).

For example, in the case of LL, HasSrcSpan a is a required type constraint.

Trac metadata

Trac field	Value
Version	8.6.2
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture