Hi,

in the following code, `Applicative.class_of`

can be compiled without `Definition comp_pureMap_class_of ...`

.

But, it is not compiled with the error `The term "comp" has type "(?B2 -> ?A4) -> (?C -> ?B2) -> ?C -> ?A4" while it is expected to have type "?A3"`

.

Why the type-check do not work well by adding `comp_pureMap_class_of`

.

```
Module Pure.
Definition Eta (m:Type -> Type) := forall A, A -> m A.
Record class_of (m:Type -> Type) :=
Class {
eta : Eta m;
}.
Section Packing.
Structure map := Pack {apply; _: class_of apply}.
Variable (cF : map).
Definition class :=
let: Pack _ c := cF return class_of (apply cF) in c.
End Packing.
Module Exports.
Notation pureMap := map.
Notation Eta := Eta.
Coercion apply : map >-> Funclass.
Definition eta T := (eta (class T)).
End Exports.
End Pure.
Import Pure.Exports.
(* 1 *)
Definition comp_pureMap_class_of (m n:pureMap) : Pure.class_of (m \o n)
:= (Pure.Class (fun A => (@eta m _ \o @eta n A))).
(* 2 *)
Module Applicative.
Definition Applicative (m:Type -> Type)
:= forall A B, m (A -> B) -> m A -> m B.
Record class_of (m:Type -> Type) :=
Class {
base : Pure.class_of m;
applicative : Applicative m;
_: forall A B (f g:A -> B),
f =1 g ->
applicative (eta (Pure.Pack base) f)
=1 applicative (eta (Pure.Pack base) g);
_: forall A (x:m A),
applicative (eta (Pure.Pack base) id) x = x;
_: forall A B C (f:m (B -> C)) (g:m (A -> B)) x,
applicative (applicative
(applicative
(eta (Pure.Pack base) comp) f)
(* (@eta (Pure.Pack base)
((_ -> _) -> (_ -> _) -> _) comp) f)*)
g) x =
applicative f (applicative g x);
_: forall A B (f:A -> B) x,
applicative (eta (Pure.Pack base) f) (eta (Pure.Pack base) x) =
eta (Pure.Pack base) (f x);
_: forall A B (f:m (A -> B)) x,
applicative f (eta (Pure.Pack base) x) =
applicative (eta (Pure.Pack base) (@^~ x)) f
}.
End Applicative.
```

Itâ€™s not possible to step through your code as is, I think it lacks notations (`\o`

and `@^~`

) and something for implicit arguments at least? Could you provide those or an import so that we can try and debug it?

Meven, it works with

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
```

This is a universe issue: defining `comp_pureMap_class_of`

forces some constraints between the universe levels of `comp`

and those of the other definitions you have around. There are at least two solutions: the easy one is to replace `m \o n`

by `fun x => m (n x)`

in the definition of `comp_pureMap_class_of`

. A better solution to keep using `comp`

would be to declare it universe polymorphic, which is not done in ssreflect for various technical reasons, but you could try and redefine your own.

Using this should do the trick:

```
Polymorphic Definition comp {A B C} (f : B -> A) (g : C -> B) : C -> A :=
fun x => f (g x).
Notation "f1 \o f2" := (comp f1 f2) : fun_scope.
```

Last updated: Jan 31 2023 at 14:03 UTC