Stream: Coq users

Topic: type inference in `let in` expression


view this post on Zulip Remzi Yang (Apr 19 2023 at 08:04):

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?

view this post on Zulip Ali Caglayan (Apr 19 2023 at 08:25):

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