Irrefutable patterns

There is a notion of ``irrefutable patterns'' used by some syntactic constructions. Matching against these patterns never fails. An ``irrefutable pattern'' is either:

• A variable.
• The wildcard ``_''.
• The constructor ``()''.
• A t-uple with irrefutable patterns.
• A record with irrefutable patterns.
• An irrefutable pattern with a type constraint.

Note that the term ``irrefutable'' does not apply to all patterns which never fail: constructors alone in their type declarations, except ``()'', are not said ``irrefutable''.