Debugging coverage errors

This page lists techniques for debugging input coverage and output coverage errors.

Debugging input coverage errors by adding type annotations

Motivating example

As a motivating example, we define a simple subtyping relation on the types of a programming language. The language includes integers, floating point numbers, and functions. We consider int to be a subtype of float, and we give the usual contravariant rule for functions:

%sort tp %.
%term int tp %.
%term float tp %.
%term arrow %pi tp %-> tp %-> tp %.
%sort sub {_ tp} {_ tp} %.
%term sub-ii sub int int %.
%term sub-ff sub float float %.
%term sub-if sub int float %.
%term sub-arrow %pi (sub (arrow T S) (arrow T' S')) %<- (sub T' T) %<- (sub S S') %.

Let’s prove that this subtyping relation is transitive. When writing STELF code, it’s sometimes convenient to just blaze ahead with a proof without thinking to hard about what you’re doing, and then think about what’s going on only if STELF reports an error. So a first proof attempt might look like this:

%sort sub-trans {_ sub T1 T2} {_ sub T2 T3} {_ sub T1 T3} %.
%mode sub-trans %in %in %out %.
%term _ sub-trans (%the (sub T T) D) (%the (sub T T) D') D %.
%term _ sub-trans sub-ii sub-if sub-if %.
%term _ sub-trans sub-if sub-ff sub-if %.
%term arrow
  %pi (sub-trans (sub-arrow DS DT) (sub-arrow DS' DT') (sub-arrow DS'' DT''))
  %<- (sub-trans DT DT' DT'')
  %<- (sub-trans DS DS' DS'') %.

We let our fingers do the proving and came up with the straightforward inductive proof. Each case type checks. Does it work?

%worlds () (sub-trans _ _ _).
%total D (sub-trans D _ _).

STELF reports an input coverage error: we didn’t cover the case for sub-arrow against sub-arrow.
We think: “But I wrote a case for sub-arrow against sub-arrow right up there! What do you mean I didn’t cover it?!”

Debugging technique

What STELF is saying is that we didn’t cover the general case for sub-arrow against sub-arrow. That is, the inferred type of the constant -arrow must be less general than required. One way to figure out the problem is to read the type of the constant:

-arrow : sub-trans
         (sub-arrow DS DT)
         (sub-arrow DS' DT')
         (sub-arrow DS'' DT'')
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.

As you can see, the type that STELF inferred has the same type X4 as all three types related by DT and DT'. Because STELF unified these parameters, -arrow doesn’t cover the whole space that we think it does.

Now, we have to figure out why STELF inferred this type. What mistake did we actually make? One good way to figure this out is to start adding type annotations giving the constants fully general types. By doing so, we can turn a coverage error into a type error on the constant.

For example, let’s annotate this constant more carefully with what we expect the inputs to be:

-arrow : sub-trans
         (sub-arrow (DS : sub S1 S2) (DT : sub T2 T1))
         (sub-arrow (DS' : sub S2 S3) (DT' : sub T3 T2))
         (sub-arrow DS'' DT'')
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.

This causes STELF to report a type error, so we know we’re on the right track—the constant doesn’t cover what we want it to.

We can make this type error more comprehensible by removing some of the constraints. Specifically, we can take out the return term to remove some of the constraints on DT_:

-arrow : sub-trans
         (sub-arrow (DS : sub S1 S2) (DT : sub T2 T1))
         (sub-arrow (DS' : sub S2 S3) (DT' : sub T3 T2))
         _
         <- sub-trans DT DT' DT''
         <- sub-trans DS DS' DS''.

Ah ha! STELF is pointing us to the first premise, as saying that because DT has type sub T2 T1, the second argument DT' needs to have type sub T1 X1 for some X1; but we wrote a term with type sub T3 T2. If we annotate the constant enough that STELF knows that T1 and T3 are supposed to be different, this is reported as a type error. Otherwise, STELF unifies these two, coming up with a valid type for the constant; but because this type doesn’t cover the part of the relation that we thought it did, we get an input coverage error.

As you may have figured out already, the problem is that the first recursive call should swap the two arguments:

%term arrow
  %pi (sub-trans (sub-arrow (%the (sub S1 S2) DS) (%the (sub T2 T1) DT)) (sub-arrow (%the (sub S2 S3) DS') (%the (sub T3 T2) DT')) (sub-arrow DS'' DT''))
  %<- (sub-trans DT' DT DT'')
  %<- (sub-trans DS DS' DS'') %.