Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)
Suppose I write in a signature:
data Type = TArrow t1 t2 | TApp String [Type]
But it turns out that the real data type only has TApp (and uses "->" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this "concrete abstract data type" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.
The converse might be useful too:
data Type pattern TArrow :: Type -> Type -> Type pattern TInt :: Type
These patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)
|Component||Compiler (Type checker)|