# How to force computation?

**URL:** <https://discourse.rocq-prover.org/t/how-to-force-computation/341>\
**Category:** Using Rocq\
**Created:** [June 27, 2019, 11:21pm UTC](https://discourse.rocq-prover.org/t/how-to-force-computation/341 "2019-06-27T23:21:01Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [June 27, 2019, 11:21pm UTC](https://discourse.rocq-prover.org/t/how-to-force-computation/341/1 "2019-06-27T23:21:01Z")

</div>

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 `i`th 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?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [June 29, 2019, 4:44pm UTC](https://discourse.rocq-prover.org/t/how-to-force-computation/341/2 "2019-06-29T16:44:24Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [June 29, 2019, 4:56pm UTC](https://discourse.rocq-prover.org/t/how-to-force-computation/341/3 "2019-06-29T16:56:23Z")

</div>

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 🙂