automatically infered MonadLifts

Stream: new members

[Simon Daniel]

hello, i am confused to why lean is able to derive one MonadLift automatically, but does not try to infer the second one (even though it can be inferred). I tried to kept my example minimal:

def Free: (Type -> Type) -> (Type -> Type ) := sorry
instance: Monad (Free e) := sorry
instance (e:Type -> Type): MonadLift (e) (Free e) := sorry

def e1: Type -> Type := sorry
def e2: Type -> Type := sorry

instance: MonadLift e1 e2 := sorry

class Sig where
  sig: (Type -> Type)

instance s: Sig where
  sig := e2

def test: Free (s.sig) Unit := do
  let test_e2: e2 Unit := sorry
  let _ <- test_e2 -- lifts just fine
  let test_e1: e1 Unit := sorry
  let lifter: MonadLift e1 e2 := inferInstance
  let _ <- test_e1 -- does not infer the Lift instance automatically

  return