Universe metavariables and typeclass resolution failure

[joehendrix]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Typeclass resolution unexpectedly fails due to unresolved universe metavariables.

I have an example below, but Lean wasn't able to resolve a type class instance due to the interaction of a couple behaviors.

First, if an operation in a type class is quantified over universe variables, then the variables are bound at the type class rather than quantified over the field. This is expected due to how type classes are represented, and perhaps unavoidable. I think it'd be worth having a warning on this though or just forcing the universe variables to be explicit.

Secondly, if an instance contains unresolved metavariables including universe metavariables, then type class resolution fails.

Steps to Reproduce

Here's an artificial example below that illustrates the problem.

-- This type class actually has two implicit universe variables due to the eval method.
class cl (α : Type) :=
(pp   : α → string)
(eval : Π{m} [monad m], α → m punit)

-- Print universe variables.
set_option pp.all true

-- Observe the extra universe variables at the top-level (not quantified in eval).
#print cl

-- Make string a instance for debugging purposes.
instance cl_string : cl string := sorry

-- Observe that cl_string works for two universes.
#print cl_string

-- This succeeds as eval refers to all the universe variables.
def do_eval : string → io unit := cl.eval

-- Print trace to see error message.
set_option trace.class_instances true

-- This fails as the the universes in the monad are not bound.
def do_pp : string → string := cl.pp

I think my preference is that typeclass resolution is changed to work when universe metavariables are still unbound.

I also would prefer that Lean require that the universe variables introduced by class members are explicit so that users aren't surprised by where they appear.

Versions

Lean (version 3.4.2, commit 1229f9b2d7f0, Release) running on OSX.

Additional Information

None