TC now requires more universe annotations

[dselsam]

namespace Test

def set (α : Type _) := α → Prop
def set_of (f : α → Prop) : set α := f
constant continuous (f : α → β) : Prop := false

instance : CoeSort (set α) (Type u) := ⟨Subtype⟩

variable {α : Type u} {β : Type v}

-- This works:
instance : CoeFun ((set_of λ f : α → β => continuous f) : Type (max u v)) (λ _ => α → β) :=
⟨Subtype.val⟩

-- This fails:
instance : CoeFun (set_of λ f : α → β => continuous f) (λ _ => α → β) :=
⟨Subtype.val⟩
end Test

The failure is due to a floating universe meta-variable:

    [Meta.synthInstance.generate] instance boolToProp
    [Meta.synthInstance.tryResolve]
      [Meta.synthInstance.tryResolve] Coe ?m.458 (Sort ?u.370) =?= Coe Bool Prop
      [Meta.isDefEq]
        [Meta.isDefEq.step] Coe ?m.458 (Sort ?u.370) =?= Coe Bool Prop
        [Meta.isDefEq.delta]
            [Meta.isDefEq.step] ?m.458 =?= Bool
            [Meta.isDefEq] ?m.458 [assignable] =?= Bool [nonassignable]
              [Meta.isDefEq.assign]
                [Meta.isDefEq.assign] ?m.458 := Bool
                [Meta.isDefEq.assign.beforeMkLambda] ?m.458 [] := Bool
                [Meta.isDefEq.assign.checkTypes]
                  [Meta.isDefEq.step] Sort ?u.446 =?= Type
                  [Meta.isLevelDefEq.step] ?u.446 =?= 1
                  [Meta.isDefEq.assign.final] ?m.458 := Bool
            [Meta.isDefEq.step] Sort ?u.370 =?= Prop
            [Meta.isLevelDefEq.step] ?u.370 =?= 0
              [Meta.isLevelDefEq.stuck] ?u.370 =?= 0
  [Meta.isDefEq]

Inside synthInstance, isDefEq throws a isDefEqStuck exception, which is not caught by synthInstance.

The problem arises because the main goal of TC has a non-TC meta-variable:

CoeT (Test.set (α → β)) (Test.set_of fun (f : α → β) => Test.continuous f) (Sort ?u.370)

Note that unlike CoeSort, CoeT does not make its second argument an outParam. The elaborator does not try CoeSort directly.

[leodemoura]

The issue is not related to coeSort. The following example also doesn't work, and it doesn't use CoeSort.

def set (α : Type _) := α → Prop
def set_of (f : α → Prop) : set α := f
constant continuous (f : α → β) : Prop := false

instance : Coe (set α) (Type u) := ⟨Subtype⟩

variable {α : Type u} {β : Type v}

def tst : Type _ :=
  set_of λ f : α → β => continuous f

In Lean 4, we made the design decision that TC resolution should never assign metavariables created by other modules (e.g., the elaborator). The idea is to make sure TC should not fill "holes" it is not meant to fill. In Lean 3, this design decision is not strictly enforced as in Lean 4, and it produced counterintuitive behavior in the past. So, I think it is a bad idea to relax this restriction in Lean 4.

CoeFun is defined as

class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
  coe : (a : α) → γ a

So, when we write CoeFun (set_of λ f : α → β => continuous f) (λ _ => α → β), there is nothing restricting the universe u for the first argument. I considered the following workaround that makes CoeFun less general

class CoeFun_2 (α : Sort u) (γ : outParam (α → Sort u)) where --- the second `u` is a `v` at CoeFun
  coe : (a : α) → γ a

However, it is too restrictive and we would not be able to write

structure ConstantFunction where
  domain : Type
  range  : Type
  f      : domain → range
  h      : ∀ a b, f a = f b

instance : CoeFun ConstantFunction (fun s => s.domain → s.range) where
  coe s := s.f

since ConstantFunction is in Type 1 instead of Type (i.e., Type 0).

I also considered converting pending universe metavariables into parameters before all "holes" have been filled, but I fear this will create counterintuitive behavior.

We can try to improve the error message and make it clear the issue is due to universe metavariables.

[digama0]

We can try to improve the error message and make it clear the issue is due to universe metavariables.

What's the workaround though? This seems like very reasonable code to write; it's not clear how we should get typeclass inference to deduce the universe metavariable if that's the desired effect in context. In particular, I worry that this will mean that users will have to pay closer attention to universe variables - in mathlib we use Type* for everything and lean is surprisingly good at making universe arithmetic completely invisible for 98% of use cases.

I don't know that I can make a good suggestion for what to do here though. One possibility is to exempt universe metavariables from this TC resolution rule, although I can see why that would be undesirable. Another option would be to have an out_param-like annotation for universe variables - in lean 3 this is essentially the default setting for all universe variables in instances, and I don't think it's a bad default, since I can't think of any example where you want to find different typeclasses based on the universes.

[leodemoura]

What's the workaround though?

Daniel included a workaround using type ascription.

instance : CoeFun.{max u v + 1} ((set_of λ f : α → β => continuous f : Type (max u v))) (λ _ => α → β) :=
  ⟨Subtype.val⟩

Here is another one where we provide the univer parameter to CoeFun.

instance : CoeFun.{max u v + 1} (set_of λ f : α → β => continuous f) (λ _ => α → β) :=
  ⟨Subtype.val⟩

[leodemoura]

It's not clear how we should get typeclass inference to deduce the universe metavariable if that's the desired effect in context.

We could try to add an outParam annotation for universe parameters or an attribute that allows us to control this kind of behavior.

In particular, I worry that this will mean that users will have to pay closer attention to universe variables - in mathlib we use Type* for everything and lean is surprisingly good at making universe arithmetic completely invisible for 98% of use cases.

We should investigate and see what happens. I don't want to keep adding hacks and workarounds as we did in Lean 3 because the system becomes very hard to maintain.

[dselsam]

It still seems funny to me that outParams are only considered for the outermost TC goal. Here the original CoeT goal produces a CoeSort subgoal, but CoeSort's outParam annotation is ignored because it is not a top-level goal. I think my prior expectation may have been that any instance that returns a class with an outParam can muck with metavariables in that slot.

[leodemoura]

It still seems funny to me that outParams are only considered for the outermost TC goal. Here the original CoeT goal produces a CoeSort subgoal, but CoeSort's outParam annotation is ignored because it is not a top-level goal. I think my prior expectation may have been that any instance that returns a class with an outParam can muck with metavariables in that slot.

@dselsam I don't think it makes sense. Happy to chat in a virtual meeting, it is too much work to write down why it doesn't make sense.

[digama0]

We should investigate and see what happens. I don't want to keep adding hacks and workarounds as we did in Lean 3 because the system becomes very hard to maintain.

That's totally fair. As long as we find something with approximately equivalent or better ergonomics for end users, I'm all for getting rid of the hacks. In this case, I think that universe outParams are the most principled solution, in the sense that this best expresses the intent, although there might be unforeseen technical issues with this.