uncurry fails with `Icc`

Stream: mathlib4

[Tomas Skrivan]

I found out that HasUncurry.uncurry does not play well with Icc

import Mathlib
-- this fails
#check ↿fun (i j : Set.Icc (-1) 1) => (1 : Nat)

I thought that it has to do with the coercion of Icc to Type but that is not the case because this works

import Mathlib
-- this works
#check ↿fun (i j : Metric.sphere (0:ℝ) 1) => (1 : Nat)

What is going wrong here?

[Tomas Skrivan]

It has to be something odd with elaboration because this works

import Mathlib
def f := fun (i j : Set.Icc (-1) 1) => (1 : Nat)
-- this works
#check ↿f

[Eric Wieser]

This works:

#check ↿(by exact fun (i j : Set.Icc (-1) 1) => (1 : Nat))

[Tomas Skrivan]

What a hack! I'm doing this inside of some notation so I can add the by exact to make it work.

[Eric Wieser]

In that case you can probably just elaborate things in a different order

[Eric Wieser]

Though I guess if you're in MacroM not TermElabM you can't