# Zulip Chat Archive

## Stream: new members

### Topic: accessing typeclass member fails

#### Chris M (Nov 03 2020 at 15:23):

I just wrote this for a quick test, and it gives me an unexpected error:

```
class FinT (T:Type*) :=
(n:nat) (emb:T → nat) (embinv:nat → T) (finite:∀ t, emb t < n) (bijective: ∀ t, embinv (emb t) = t)
set_option trace.eqn_compiler.elim_match true
def summation (T:Type*) (f:(T → Prop) → nat) [h:FinT T]: T → nat := fun t:T,
let n:nat := ((h.emb) t) in
match n with
| (nat.succ k) := 1
| zero := 0
end
```

gives me the error:

```
invalid field notation, function 'FinT.emb' does not have explicit argument with type (FinT ...)
```

What is weird is that if I replace the `let`

statement with the following, it doesn't give any errors:

```
let embbbb:T → nat := h.emb in
let n:nat := ((embbbb) t) in
```

#### Johan Commelin (Nov 03 2020 at 15:24):

Replacing `h.emb`

with `FinT.emb`

should work.

#### Johan Commelin (Nov 03 2020 at 15:24):

typeclass arguments are implicit, so you typically can't use them with projection notation.

#### Chris M (Nov 03 2020 at 15:32):

thanks :)

#### Chris M (Nov 03 2020 at 15:52):

Actually a related weird problem :

```
open nat
section FinT
class FinT (T:Type*) :=
(n:nat) (emb:T → nat) (embinv:nat → T) (finite:∀ t, emb t < n) (bijective: ∀ t, embinv (emb t) = t)
end FinT
open FinT
def summation (T:Type*) (f:(T → Prop) → nat) [h:FinT T]: T → nat := fun t:T,
let n:nat := (emb t) in
match n with
| (succ k) := 3
| zero := 4
end
def summeasure (f:nat → nat) : nat → nat
| (succ k) := f(succ k) + summeasure k
| zero := f zero
open decidable
def pred_to_count {T:Type*} (f:T → Prop) [h:∀t, decidable (f t)]: T → nat := fun t:T, if h:(f t) then 1 else 0
def sumprednat (P:nat → Prop) [h:∀t, decidable (P t)] : nat → nat := fun n:nat, summeasure (pred_to_count P) n
def sumpred {T:Type*}[FinT T] (P:T → Prop) [h:∀t, decidable (P t)] : nat → nat :=
let Q := (fun n:nat, P (FinT.embinv T n)) in
fun n:nat, summeasure (pred_to_count Q) n
```

What is surprising to me about this, is that in the last definition, I have to write `(FinT.embinv T n)`

instead of `(FinT.embinv n)`

for it to type check. If I don't add it, I get the error

```
type mismatch at application
embinv n
term
n
has type
ℕ : Type
but is expected to have type
Type ? : Type (?+1)
```

Why is this, given that typeclasses are supposed to be implicit, and given that the same is not needed for `let n:nat := (emb t) in`

in the earlier definition of `summation`

?

#### Mario Carneiro (Nov 03 2020 at 15:53):

typeclasses are implicit, but the types are not (necessarily)

#### Mario Carneiro (Nov 03 2020 at 15:54):

if you want `FinT.embinv`

to take `T`

as implicit, write the field as ` (embinv {} : nat → T)`

#### Chris M (Nov 03 2020 at 15:58):

ok that makes sense, thanks.

Last updated: May 09 2021 at 18:17 UTC