How to force computation?

Using Coq
1

I have the following constructor:

  | PSelect
    : ∀ {n : nat} {ss : Vector.t SType n}
    (i : Fin.t n)
    , (Message C[ss[@i]] → Process)
    → Message C[Select ss]
    → Process

Where the ith element of the vector ss is fetched. When I try to supply such an argument, I get the following:

The term "?( _ ); ε" has type "Message ?ST ?MT C[ ? ?m; ø] → Process ?ST ?MT"
while it is expected to have type "Message ?ST ?MT C[ ?ss[@Fin.F1]] → Process ?ST ?MT".

If however I enter proof mode and run simpl, the types advance and I can give the argument. Is there a way to hint coq that I want these types to always be computed?

2

It’s hard to be sure without the source, but most likely, your problem happens during type inference, not typechecking. When comparing types A and B, Coq will automatically simplify them both as needed.

However, that cannot be done as well when inferring arguments; in your case, I expect Coq cannot infer ss. Maybe you should make ss a non-implicit argument. Or, if Select is a constructor, you might be able to change the argument order to get Message C[Select ss] → (Message C[ss[@i]] → Process) → Process.

Coq cannot infer ss by knowing that ss[@i] is a certain S : SType; it would have to solve equation ?ss [@i] = S in ?ss, but that equation does not have a single solution. Indeed, when Coq prints the error you see, it has not yet inferred what ss should be, and writes ?ss instead.
Quite possibly, when you enter the proof mode, things happen to be inferred in a different order and everything works out.

3

Thanks for the explanation of what’s happening, changing the order of the arguments made the trick – I have some fancy notation so for the user things are staying as they are :slight_smile:

1 Like