type instance failing with subtype

Stream: metaprogramming / tactics

[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?

[Notification Bot]

This topic was moved by Eric Wieser to #new members > type instance failing with subtype