Hello, I define a `Const`

type and my `Functor`

typeclass:

```
Inductive const (C A: Type): Type :=
| Const: C -> const C A.
Arguments Const {C A} c.
Class Functor (F: Type -> Type) := {
fmap {A B: Type} : (A -> B) -> F A -> F B;
fmap_id : forall (A: Type),
fmap id (A := A)= id;
fmap_preserve_composition : forall (A B C: Type) (f: A -> B) (g: B -> C),
fmap (compose g f) = compose (fmap g) (fmap f)
}.
```

And I am trying to instance `Functor Const`

```
#[export] #[refine] Instance const_Functor (C: Type) : Functor (const C) := {|
fmap A B (f: A -> B) c := let Const c := c in Const c
|}.
...
```

I got this error: `The term "Const c" has type "?F A" while it is expected to have type "?F B".`

But it could compile if I replace `let ... in ...`

with `match ... end`

```
#[export] #[refine] Instance const_Functor (C: Type) : Functor (const C) := {|
fmap A B (f: A -> B) c := match c with
| Const c => Const c
end
|}.
...
```

How can I fix the type error in `let ... in ...`

expression?

When you have `let Const c`

you are defining a new function called `Const`

and shadowing your one. Perhaps you want to use `let '(Const c) := c`

which will pattern match.

Last updated: Jun 15 2024 at 08:01 UTC