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: Oct 13 2024 at 01:02 UTC