A few days ago, I ran into a fairly ugly problem involving matches in dependent types. This post will walk through a simplified version of this problem, demonstrating the different solution attempts I made along the way and explaining why they do not work, until arriving at a somewhat satisfactory solution. While this post doesn’t contain anything groundbreaking, it might strengthen your understanding of the effects matches have on types. I won’t go over the basics of functional or dependently typed programming. However, a sound intuition for the matter should be sufficient to understand this post.

The example we will use throughout this post is a simple language of arithmetic expressions arith made up of binary operators and constants. Instead of explicitly choosing which constants and operators to include, we generalize the type arith over a class of signatures Signature, which specifies types containing the operator and constant symbols. Declaring it as a class instead of a regular structure gives us the benefit Coq of attempting to automatically infer which Signature we are trying to use, saving us some typing. We also write a recursive function eval that can evaluate an expression, given functions describing how to treat the operators and constants.

Class Signature := B_S { ops : Type ; consts : Type }.

Section Arith.
  Context {Sigma : Signature}.

  Inductive arith : Type :=
  | Op : ops -> arith -> arith -> arith
  | C : consts -> arith.

  Fixpoint eval (oint : ops -> nat -> nat -> nat) (cint : consts -> nat) e :=
    match e with
    | Op o e1 e2 => oint o (eval oint cint e1) (eval oint cint e2)
    | C c => cint c
    end.
End Arith.

Having set up the basic definitions, we can move on to the problematic bits. It can often be useful to define functions that transform a given signature. For our example, we will consider the function sig_ext which extends a signature with one new constant symbol inr I.

Definition sig_ext (Sigma : Signature) :=
  match Sigma with
    B_S ops consts => B_S ops (consts + True)
  end.

Such a signature transformation calls for a matching function on expressions. Hence, we define a function lift_arith that lifts expressions in an expression Sigma to expressions in sig_ext Sigma. Our first, naive attempt would probably look like this:

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  match e with
  | Op o e1 e2 => Op o (lift_arith e1) (lift_arith e2)
  | C c => C (inl c)
  end.

However, Coq will reject this definition with the following gripe:

The term "lift_arith Sigma e1" has type "@arith (sig_ext Sigma)"
while it is expected to have type "@arith Sigma".

The reason for this is fairly easy to figure out. Coq has inferred that Op is the constructor to @arith Sigma, as it is applied o : @ops Sigma. This can be fixed by explicitly telling Coq which variant of Op we want.

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  match e with
  | Op o e1 e2 => @Op (sig_ext Sigma) o (lift_arith e1) (lift_arith e2)
  | C c => @C (sig_ext Sigma) (inl c)
  end.

However, Coq is still not happy with this. This time, it tells us:

The term "o" has type "@ops Sigma" while it is expected to have type
"@ops (sig_ext Sigma)".

Now, what went wrong here? Clearly, looking at the definition of sig_ext, we know that @ops Sigma = @ops (sig_ext Sigma). However, the reason Coq can not infer this is fairly simple. Unfolding sig_ext Sigma, we arrive at

match Sigma with B_S ops consts => B_S ops (consts + True) end

Coq is unable reduce this match (and hence can’t infer that o : @ops (sig_ext Sigma)) as it does not know the specific makeup of Sigma. If this were a proof, we would have to do a destruct of Sigma to get this match to reduce. The Gallina equivalent of a destruct is a match, hence we have to insert a match on Sigma into the function lift_arith. However, this turns out to be problematic. Naively inserting the match like this will not work.

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  match Sigma with
    B_S os cs as Sig =>
      match e with
      | Op o e1 e2 => @Op (sig_ext Sig) o (lift_arith e1) (lift_arith e2)
      | C c => @C (sig_ext Sigma) (inl c)
      end
  end.

Coq will complain with the following message (after a Set Printing All):

Error:
In environment
e : @arith Sigma
o : @ops Sigma
(* ... *)
The term "o" has type "@ops Sigma" while it is expected to have type
"@ops (sig_ext Sig)".

As we can see, the types of e and o are unaffected by the match (we might expect them to be of type @arith Sig and @ops Sig, respectively). This seemingly strange behavior is caused by the details of how match works. Intuitively, we would expect all occurrences of Sigma to be replaced by Sig. However, this is not really what it does. This replacement is only performed in our “goal” (that is, the return type of the match). In this case, this is @arith (sig_ext Sigma) which is transformed into @arith (sig_ext Sig). As e is not part of the goal, it remains unchanged.

This behavior might be surprising to readers familiar with proving in Coq, as destruct does also perform these replacements in your hypothesis. However, a quick look at the proof generated (using Show Proof) will reveal that destruct cleverly reverts all the relevant hypothesis before performing the match, thereby moving them into the goal. We can fix our example by copying that trick. That is, we revert the expression e before the match and reintroduce it afterwards.

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  (match Sigma with
    B_S os cs as Sig => fun e' : @arith Sig =>
      match e' with
      | Op o e1 e2 => @Op (sig_ext Sig) o (lift_arith e1) (lift_arith e2)
      | C c => @C (sig_ext Sig) (inl c)
      end
  end) e.

I hope this ordeal has improved or reinforced your intuition about the effects on types matches have in Coq, just as it did for me. While this definition looks somewhat inelegant, it is the nicest solution to this problem that I know of. If you know an even nicer solution, please do not hesitate to contact me with it.