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 |