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 `match`es 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.