Dot notation on abbreviation

Stream: general

[Yaël Dillies]

Consider the following:

import data.fintype.basic

structure foo_on {α : Type*} (s : finset α) :=
(n : ℕ)

abbreviation foo (α : Type*) [fintype α] := foo_on (finset.univ : finset α)

example {α : Type*} [fintype α] (bar : foo α) : bar.n = bar.n :=
begin
  -- bar.n = bar.n
end

def foo_on.m {α : Type*} {s : finset α} (bar : foo_on s) : ℕ := bar.n

example {α : Type*} [fintype α] (bar : foo α) : bar.m = bar.m :=
begin
  -- foo_on.m bar = foo_on.m bar
end

Dot notation sees through abbreviation, but gets pretty-printed correctly only for fields of the original structure. Is there any way around that? by manipulating the transparency of foo_on.m, maybe?

[Eric Wieser]

In general the pretty printer is much more conservative about what it shows with dot notation than the elaborator is in what it accepts.

[Eric Wieser]

Although I think that would be easy to change