coercion from GL to matrices fails without hints

Stream: mathlib4

[Kevin Buzzard]

It's well-known that things like this fail:

import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

variable {n : Type*} {R : Type*}

def IsFoo (M : Matrix n n R) : Prop := sorry

example (M : GL Unit ℤ) : Prop := IsFoo (M : Matrix Unit Unit ℤ) -- works
example (M : GL Unit ℤ) : Prop := IsFoo M -- application type mismatch

with error

application type mismatch
  IsFoo M
argument
  M
has type
  GL Unit ℤ : Type
but is expected to have type
  Matrix ?m.101 ?m.101 ?m.102 : Type (max ?u.100 ?u.99)

The usual explanation is something like "When Lean is given M : GL Unit ℤ and it wants a matrix, it knows the coercion from GL Unit ℤ to Matrix Unit Unit ℤ but doesn't apply it because there might be other coercions to Matrix n n R". But can we just make Lean choose the obvious one automatically somehow?

[Yaël Dillies]

This same issue happens all the time with the coercion Finset α → Set α. We really really need a solution here

[Yaël Dillies]

I was hoping default instances could fix it, but I am not sure of the performance impact of making docs#Finset.instCoeTCSet a default instance, as there are many CoeTC instances out there

[Matthew Ballard]

An RFC for cut rules for synthesis would be great

[Matthew Ballard]

This came up recently elsewhere (and has a few times before)

[Eric Wieser]

What's the status of unification hints?

[Matthew Ballard]

Has their status changed recently?

[Eric Wieser]

Well, there's a risk they're transitioning from "unused" to "not supported"

[Matthew Ballard]

If I step through this, I get a problem with metavariable depth (probably) making it unassignable.