accessing typeclass member fails

Stream: new members

[Chris M]

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]

Replacing h.emb with FinT.emb should work.

[Johan Commelin]

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

[Chris M]

thanks :)

[Chris M]

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]

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

[Mario Carneiro]

if you want FinT.embinv to take T as implicit, write the field as (embinv {} : nat → T)

[Chris M]

ok that makes sense, thanks.