Opened 5 months ago

#12717 new feature request

Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)

Reported by: ezyang Owned by:
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: backpack Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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?)

Change History (0)

Note: See TracTickets for help on using tickets.