Type ascription ignored by typeclass synthesis

Stream: lean4

[Alex Keizer]

I am in a situation where I want to index a Vector \a n with a Fin (n.succ - 1). I am also experimenting with the following, stricter GetElem instance, which requires indices to match.

/-
  Replace the exisiting instance for indexing a collection with `Fin n`.
  The new instance is more strict, only allowing a `Vector _ n` to be indexed by `Fin n`, where the
  older version allowed the same vector to be indexed by, say `Fin (n+1)` if it could be proven that
  the actual value of the `Fin` was less than `n`.
  This extra proof causes problems in rewrites.
-/
attribute [-instance] instGetElemFinVal
section GetElem
  variable (cont : ℕ → Type u)

instance [GetElem (cont n) Nat elem (fun _ i => i < n)] : GetElem (cont n) (Fin n) elem fun _ _ => True where
  getElem xs i _ := getElem xs i.1 i.2

end GetElem

We have that n.succ - 1 is defEq to n so this should work ,and I can confirm this with

variable (i : Fin (n+1-1))
#check (i : Fin n)

However v[i], and surprisingly also v[(i : Fin n)] will try to find an instance for Fin (n+1-1) and fail.
I can make it work by desugaring into

getElem (idx := Fin <| n + 1 - 1) (tail v) i  True.intro

But that is not very satisfying. Note that this issue doesn't seem to be specific to the notation: using getElem with a type ascription (and without explicitly passing idx) also fails

getElem (tail v) (i : Fin (n.succ - 1)) True.intro -- fails

[Sebastian Ullrich]

A type ascription merely checks that the given type is defeq to the inferred type, it does not change the core term and thus type. You can use show t from v or @id t v to affect the type

[Alex Keizer]

That is surprising, I though it does affect type inference for things like anonymous constructors, right?

[Alex Keizer]

Thanks for the suggestion. This is for a simp-lemma, though, so I think I shouldn't introduce an extra id in there

[Sebastian Ullrich]

It affects the expected type, but not the inferred type. That is, it only has an effect inside the parentheses, not outside

[Alex Keizer]

Right, that makes more sense. I got the idea from (0 : Nat) and (0 : Int) influencing the OfNat instance, but that is indeed inside the parenthesis. Thanks for clarifying!

[James Gallicchio]

what was the reason for it being different from show t from v? I've had to explain this before to others, and I'm never really sure what to say, since my intuition from other languages is that it should behave as show t from v.

[Kyle Miller]

show t from v is more or less let this : t := v; this, so the type of v is changed since there's a let binding (IIRC, the actual expansion uses let_fun).

(x : t) elaborates x with t as the expected type and then ensures the result has type t (so, defeq check, and if it fails synthesize a coercion if possible). To get the type to actually change you'd have to insert something like @id t x like Sebastian mentioned, which changes the term. I think you wouldn't want type ascriptions to insert lets/let_funs/ids just because the type is only defeq and not syntactically equal.

[James Gallicchio]

Sure, the term needs to be changed -- but from a programming background I don't have an expectation that (x : t) leaves the term untouched (see C/Java casting). I do have an expectation that (x : t) has type t (syntactically). I don't think I've encountered a situation where I need the (x : t) behavior instead of the show t from x behavior, so that is what I'm wondering about.

Interestingly, I have encountered situations where I use (x :), but I think its behavior matches what I would intuitively expect.

[Kyle Miller]

I think one of the gotchas for programmers coming to Lean is that type ascriptions aren't casts, for example if n m : Nat then (n + m : ℚ) gives ↑n + ↑m with coercions on each argument.

The way type ascriptions work is sort of a direct interface to the elaboration algorithm, which might be one answer for why they are the way they are.

[Kyle Miller]

(Another answer for why show t from v and (v : t) are different might be if they were the same then there'd be no need for two notations. I guess show t from v is "use this type both inwards and outwards", but (v : t) is "just use this type inwards".)

[Mario Carneiro]

Kyle Miller said:

(Another answer for why show t from v and (v : t) are different might be if they were the same then there'd be no need for two notations. I guess show t from v is "use this type both inwards and outwards", but (v : t) is "just use this type inwards".)

That's not a very convincing answer, though. I think the reason there are two notations is a combination of historical precedent and desires for those two styles of syntax in certain kinds of proof, and the elaboration differences are somewhat idiosyncratic

[James Gallicchio]

Yeah, I guess my complaint is if nobody wants the (x : t) behavior as it is atm then maybe we should just make it insert a let_fun like show does?

[Mario Carneiro]

No, the difference is definitely important for some use cases

[Mario Carneiro]

Personally I would prefer all type ascription-like syntaxes act like (x : t), I don't want junk in my term

[Mario Carneiro]

there are some technical challenges with making this interact as intended wrt typeclass inference and the like though

[James Gallicchio]

hm, okay. Maybe when I use show _ from _ there's better workarounds.