Lean Auto fails to translate some type classes

[volodeyka]

Hey! I was playing with lean auto and found some wired bug involving simple type classes. Lean auto sometimes fails to translate typeclasses which depend on arbitrary types. For instance:

import Auto.Tactic

set_option auto.smt true
set_option auto.smt.trust true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true

class foo (t : Type) where
  le : t -> t -> Prop

example [foo Nat] (x y : Nat) : foo.le x y := by
  auto -- calls smt solver, but fails to find a proof

example {α : Type} [foo α] (x y : α) : foo.le x y := by
  auto -- fails to translate (and doen't even call the solver) with the following error: 
 /-
 getSexp :: Malformed (prefix of) input (
  ;; universe for smti_1:
  ;;   smti_1!val!1 smti_1!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun smti_1!val!1 () smti_1)
  (declare-fun smti_1!val!0 () smti_1)
  ;; cardinality constraint:
  (forall ((x smti_1)) (or (= x smti_1!val!1) (= x smti_1!val!0)))
  ;; -----------
  (define-fun valid_fact_0 () Bool
    (not (smti_3 smti_0 smti_2)))
  (define-fun smti_2 () smti_1
    smti_1!val!1)
  (define-fun smti_0 () smti_1
    smti_1!val!0)
  (define-fun smti_3 ((x!0 smti_1) (x!1 smti_1)) Bool
    false)
)
 -/

Could you help me with this issue? Is it a fundamental limitation or just a bug?