should fintype take a sort?

Stream: general

[Chris Hughes]

This instance would be possible if fintype took a sort instead of a Type. Is it worth changing?
instance (p : fin 3 → Prop) [decidable_pred p] : fintype (Π a, p a → fin 3) := by apply_instance

[Mario Carneiro]

I thought about it, I have also seen this come up, but I don't know a clean way to do it without making lots of later stuff harder

[Chris Hughes]

What would be harder?

[Mario Carneiro]

you have to ulift somewhere, and this will affect proofs that don't care about Prop

[Mario Carneiro]

of course another way to solve the particular problem you show is to have a second pi instance for Props

[Chris Hughes]

I forgot that list didn't take a Sort.

[Mario Carneiro]

Actually, I'm not sure it can be done at all, assuming that list and finset stay as is

[Mario Carneiro]

What would be the type of fintype? If it is Sort u -> Type u then it bumps the universe level in unwanted circumstances (i.e. fintype nat : Type 1), and if it is Sort u -> Sort (max 1 u) then you can't define it

[Mario Carneiro]

since Sort (max 1 u) = Sort (?+1) is unsolvable (you would need a pred u function but that doesn't exist)

[Chris Hughes]

Is there any reason not to just make everything a Sort, just in case some random thing like this comes up where it's useful?

[Simon Hudon]

I think the main thing has to do with elimination. If your type isSort 0, there's a special case that you can only eliminate to Sort 0. Otherwise, in Sort 1, you can eliminate anywhere you like.

[Simon Hudon]

Btw, your instance type checks for me. Are you sure your issues have to do with universes?

[Chris Hughes]

It type checks, but it can't synthesize the instance

[Chris Hughes]

But if there was an instance saying Pi p : Prop, fintype p it would synthesize the instance from pi.fintype

[Simon Hudon]

I think you could make it work with an instance like this:

instance pi.fintype' {α : Prop} {β : α → Type*}
  [decidable α] [∀a, fintype (β a)] : fintype (Πa, β a) :=

[Chris Hughes]

I think the main thing has to do with elimination. If your type isSort 0, there's a special case that you can only eliminate to Sort 0. Otherwise, in Sort 1, you can eliminate anywhere you like.

So that makes sense for making inductive types Types rather than sorts, but for functions defined on an arbitrary Type, I don't see a downside.

[Chris Hughes]

I should probably PR both of these

instance decidable_eq_pfun_fintype (P : Prop) [decidable P] (α : P → Type*) [Π hp : P, fintype (α hp)]
  [Π hp : P, decidable_eq (α hp)] : decidable_eq (Π hp : P, α hp) :=
λ f g, if hp : P then decidable_of_iff (f hp = g hp) (⟨λ h, funext $ λ _, h, λ h, congr_fun h _⟩)
else is_true (funext $ λ h, (hp h).elim)

instance fintype_pfun (P : Prop) [decidable P] (α : P → Type*) [Π hp : P, fintype (α hp)]
  [Π hp : P, decidable_eq (α hp)] : fintype (Π hp : P, α hp) :=
if hp : P then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl⟩
else ⟨finset.singleton (λ h, (hp h).elim), λ x, by simp [hp, funext_iff]⟩

[Simon Hudon]

but for functions defined on an arbitrary Type, I don't see a downside.

I agree. Although, I find that universe constraints have a way of propagating to infect every definition once you have one. Being more polymorphic seems easier said than done.