missing `CoeFun` instance for `SubType`

Stream: lean4

[Jovan Gerbscheid]

I would have expected the following to work:

example (x : {f : Nat → Nat // f 3 = 2}) : Nat → Nat :=
  fun n => x n

It works when writing x instead of fun n => x n. Is this intended behaviour? There are quite a few instances in mathlib that are special cases of the above missing instance.

[Aaron Liu]

this seems normal to me

[Jovan Gerbscheid]

You don't think that it would make sense for all coercions to a function to be synthesized by CoeFun?

[Aaron Liu]

I don't think that would make sense

[Aaron Liu]

I think CoeFun is for when a term in an application position is not a function

[Jovan Gerbscheid]

Yes, x : {f : Nat → Nat // f 3 = 2} is not a function. And I know it has a coercion to a function, so I'd want it to get picked up by CoeFun.

[Aaron Liu]

interesting take

[Aaron Liu]

it won't get pretty-printed as a coefun though

[Aaron Liu]

import Mathlib

def test (x : {f : Nat → Nat // f 3 = 2}) : Nat → Nat :=
  fun n => (x : Nat → Nat) n

/--
info: def test : { f // f 3 = 2 } → ℕ → ℕ :=
fun x n => ↑x n
-/
#guard_msgs in
#print test

[Eric Wieser]

I think that's a feature

[Eric Wieser]

We don't want two spellings of the same thing in the infoview

[Aaron Liu]

yes and that's why I think it shouldn't be a coefun

[Eric Wieser]

That's why it shouldn't be a DFunLike

[Aaron Liu]

then you would have to deal with Subtype.val _ and DFunLike.coe _ being two different spellings of the same thing

[Aaron Liu]

that would be bad

[Aaron Liu]

so definitely not DFunLike

[Aaron Liu]

but maybe we could register Subtype.val as a CoeFun instance I think is the issue being brought up here

[Eric Wieser]

I think that

instance {p : (α → β) → Prop} : CoeFun (Subtype p) (fun _ => α → β) where
  coe := Subtype.val

is relatively harmless, and that the primary reason it doesn't exist is that in lean 3 it would have behaved as DFunLike does now

[Eric Wieser]

Or even

instance {X f} {p : X → Prop} [CoeFun X f] : CoeFun (Subtype p) (fun p => f p.1) where
  coe x := CoeFun.coe x.val

[Jovan Gerbscheid]

Yes I think the second option is better

instance {X f} {p : X → Prop} [CoeFun X f] : CoeFun (Subtype p) (fun x => f x.val) where
  coe x := CoeFun.coe x.val

(avoiding repeating variable p)

[Jovan Gerbscheid]

Should I try to add this to core, or for now to Mathlib.Data.Subtype?

[Eric Wieser]

I think probably core

[Eric Wieser]

Either this is a good idea for everyone or it isn't, this doesn't seem mathlib specific

[Jovan Gerbscheid]

A slight annoyance here is that

`CoeFun` instances apply to `CoeOut` as well.

So, adding this instance means that there are now two different CoeOut instances for Subtype.

[Eric Wieser]

Are they likely to actually be different?

[Jovan Gerbscheid]

I was saying it more out of efficiency considerations

[Jovan Gerbscheid]

I wonder if there is any reason why we can't define CoeFunT as the transitive closure of CoeOut, and generate that instead of CoeFun. Then it would just need to check that the generated type is indeed a function. Currently if it generates a non-function type, it says:

failed to coerce
  x
to a function, after applying `CoeFun.coe`, result is still not a function
  x.bla
this is often due to incorrect `CoeFun` instances, the synthesized instance was
  instCoeFunMyFun'MyFun

[Edward van de Meent]

i imagine because CoeFunT will then include lots of instances which will not at all be conducive in creating a function?

[Jovan Gerbscheid]

Yeah. I thought at first that there wouldn't be other CoeOut instances for function-like types. But they do exists, for example

instance coeOutMonoidHom : CoeOut (A →ₐ[R] B) (A →* B)

[Jireh Loreaux]

Eric Wieser said:

instance {X f} {p : X → Prop} [CoeFun X f] : CoeFun (Subtype p) (fun p => f p.1) where
  coe x := CoeFun.coe x.val

You're proposing adding both the above and also this:

Eric Wieser said:

instance {p : (α → β) → Prop} : CoeFun (Subtype p) (fun _ => α → β) where
  coe := Subtype.val

right? Because the first one doesn't imply the second, unless I'm grossly mistaken.

[Jovan Gerbscheid]

Note that the docstring of CoeFun.coe is also confused about the non-transitive nature of CoeFun

/-- Coerces a value `f : α` to type `γ f`, which should be either be a
  function type or another `CoeFun` type, in order to resolve a mistyped
  application `f x`. -/

But if I try to have γ f be another CoeFun type, I get an error:

structure A where
  a : Nat → Nat

structure B where
  b : A

instance : CoeFun A (fun _ => Nat → Nat) := ⟨A.a⟩
instance : CoeFun B (fun _ => A) := ⟨B.b⟩

variable (x : B) (n : Nat)

#check x n -- error

[Jovan Gerbscheid]

Another option is to add this instance to Mathlib:

instance {F α β} {p : F → Prop} [DFunLike F α β] : DFunLike (Subtype p) α β where
  coe x := DFunLike.coe x.val
  coe_injective' _ _ h := Subtype.ext (DFunLike.coe_injective' h)

I've started trying this at #27143

[Aaron Liu]

Doesn't that not fix the original issue, since functions aren't funlike?

[Jovan Gerbscheid]

You're right. I think I'll then also add an instance to make functions be funlike

[Jireh Loreaux]

No, please don't.

[Jovan Gerbscheid]

What is the disadvantage of an instance of DFunLike (∀ a, β a) α β?

[Yaël Dillies]

It has absolutely awful performance

[Jovan Gerbscheid]

Really? I though DFunLike F _ _ goals in type class search usually arise when F is NOT a function. So a DFunLike (∀ a, β a) α β instance would essentially do nothing performance wise.

[Jovan Gerbscheid]

Anyways, it turns out my idea doesn't work, because it gives an application of DFunLike.coe instead of Subtype.val.