type instance failing with subtype

Stream: new members

[Xavier Martinet]

Hi everyone,

Another weird behaviour with type instance: it seems that when there is a subtype that is set as a constant (e.g., pnat), if one replace this constant by its definition (e.g., {n // 0 < n}), the type class mechanism fails.

import data.pnat.basic

#check (1 : pnat)
-- 1 : ℕ+
#check (1 : {n // 0 < n})
/-
failed to synthesize type class instance for
⊢ has_one {n // 0 < n}
-/

Actually what I would like to do is to be able to write λ n : {n // 0 < n}, n + 1 and the elaborator understands it :

import data.pnat.basic

#check λ n : pnat, n + 1
-- λ (n : ℕ+), n + 1 : ℕ+ → ℕ+

-- replacing `pnat` by its definition does not work with class instance synthesis
#check λ n : {n // 0 < n}, (n : pnat) + 1
/-
failed to synthesize type class instance for
n : {n // 0 < n}
⊢ has_one {n // 0 < n}
-/

-- however this example works
#check λ n : pnat, (n : {n // 0 < n}) + 1
-- λ (n : ℕ+), n + 1 : ℕ+ → ℕ+

-- and this one too
#check λ n : {n // 0 < n}, (@has_add.add pnat pnat.has_add) (n)  1
-- λ (n : {n // 0 < n}), n + 1 : {n // 0 < n} → ℕ+

/-
I suppose that in the last two examples, the definition is "unfolded" so it passes typechecking
-/

Is there a workaround?

[Eric Wieser]

It's worth remembering that if x : X, foo (x : Y) tells lean that x should be parsed as a Y. However, it doesn't record this decision unless its forced to insert a coe, so as far as foo knows, x still has type X

[Eric Wieser]

You can fix this by using @id Y x or show Y, from x instead of (x : Y), which actually inserts an extra function call in your term

[Notification Bot]

This topic was moved here from #metaprogramming / tactics > type instance failing with subtype by Eric Wieser

[Eric Wieser]

(moved since this doesn't seem to be about meta or writing tactics)

[Eric Wieser]

Alternatively, we could fix this by changing how pnat is defined to be more in line with docs#nnreal etc

[Eric Wieser]

(which uses the instances on the raw subtype defined in https://leanprover-community.github.io/mathlib_docs/algebra/order/nonneg.html)