Correct function domain coverage

[AshleyYakeley]

Prior issues

• Check case expressions for exhaustive covering #114
• Replace Greatest Dynamic Supertype with general retractive subtypes #341
• fn type annotations #342

What we want

• Pinafore should infer a domain type for multi-case function statements that is
  • covered by the cases
  • as wide as possible
  • even when no type annotation is given (fn type annotations #342)

Approach

We assume two types of pattern: total (such as binding or wildcard), and constructor. A constructor pattern consists of a constructor followed by zero or more patterns. Every pattern constructor has a datatype.

We keep the partial/retractive-subtype mechanism from #341. In addition, datatypes can have parent datatypes. For example:

datatype A {
  A1;
  subtype datatype B {
    B1;
    B2;
  };
  subtype datatype C {
    C1;
    C2;
  };
};

In this case, in addition to the retractive subtype relations, we also have that A is the parent datatype of B and C, while A has no parent datatype.

We also know from this that B & C is empty, since otherwise the paths B&C <: B <: A and B&C <: C <: A would not commute.

Every datatype (and therefore every constructor) has a root datatype, which is its top ancestor. In this case, the root datatype of A, B, and C is A.

Method

We have a function with cases, each on a pattern. If any pattern is total, then (1) we use the method of #341 and (2) give an error if it's not the last pattern.

Otherwise, we first sort the patterns into one or more collections, according to the root datatypes of their constructors. (See below for handling of multiple collections.)

Each collection has a root datatype. For each constructor that is mentioned in a pattern, we ensure that the collection of patterns that use that constructor cover it. Then, we take the set of all constructors mentioned and match it against all datatypes in the family to see if it exactly matches one. If it doesn't, we give an error.

Example

f1 = fn {
  B1 => 1;
  B2 => 2;
};

f2 = fn {
  B1 => 1;
  B2 => 2;
  C1 => 3;
};

f3 = fn {
  A1 => 0
  B1 => 1;
  B2 => 2;
  C1 => 3;
  C2 => 4;
};

then we have f1 : B -> Natural and f3 : A -> Natural while f2 is rejected.

Multiple Collections

Consider this:

datatype P {P1; P2;};
datatype Q {Q1; Q2;};

fpq = fn {
  P1 => 1;
  Q1 => 2;
  P2 => 3;
  Q2 => 4;
};

then the domain of fpq can be P & partial Q or partial P & Q but not partial P & partial Q.

In this case P & partial Q would make the last Q2 case unreachable. So in general we use the last case to determine the "strict collection"; all the other collections are partial. So we have fpq : partial P & Q.

Complications

• dynamic-type patterns are treated as all the constructors of the matched type
• "both"-patterns are tricky and we may have to restrict those to total-pattern@pattern
• we still have to figure out how nested pattern coverage works