I have the following definitions

```
Parameter bt : nat -> Type.
Parameter ct : nat -> Type -> Type.
Parameter ap : forall {m} {A} (b : bt m), (ct m A) -> (ct m A).
Parameter e : forall m, ct m bool.
Parameter v : bt 1.
```

so writing

```
Check ap v (e 1).
```

is ok. Now I would like to turn `ap`

into a coercion so to be able to just write `v (e 1)`

.

I have tried

```
Coercion ap : bt >-> Funclass
```

but there is a problem of uniform inheritance. I've tried with `Identity Coercion`

but without any success. Is there a way to make `ap`

a coercion accepted by Coq?

Does it work if you put `{A}`

after `(b : bt m)`

in the type of `ap`

? (Is that acceptable?)

(Note that you may have to write `v _ (e 1)`

then, see also https://github.com/coq/coq/pull/11327)

@Laurent Théry It is still an accepted coercion, but Coq just complains about it. AFAIK Coq complains about a lot of sensible coercions. If the warning is annoying you can always disable it specifically before and after the problematic command.

Yes by moving A I can write `v _ (e 1)`

but is there a way to make `A`

implicit?

@Ali Caglayan do you mean

```
Parameter ap : forall {m} {A} (b : bt m), (ct m A) -> (ct m A).
Coercion ap : bt >-> Funclass.
```

should work even if there is a warning?

```
```

Hmm it is being accepted as a coercion, but is probably not the coercion you are looking for.

I do believe this is the kind of problem the PR Jason pointed to will solve.

@Ali Caglayan something weird happens, `v (e 1)`

is not accepted but now

```
Check ap v (e 1).
```

returns

```
bool v (e 1)
: ct 1 bool
```

!!!

I agree this should be related to 11327

cc @Hugo Herbelin

Looks indeed related to 11327.

Last updated: Jun 15 2024 at 08:01 UTC