failed to synth Applicative Option instance in nightly

Stream: lean4

[Kaushik Chakraborty]

  variable {α β γ ζ : Type u}
  variable {a : Type u -> Type v}
  def liftA3 [Applicative a] (f: α -> β -> γ -> ζ) (x: a α) (y: a β) (z: a γ) : a ζ := f <$> x <*> y <*> z

   #check liftA3 (· + · + ·) (Option.some 1) (Option.some 2) (Option.some 3)
  -- leanprover/lean4:stable
  --    liftA3 (fun (a a_1 a_2 : Nat) => a + a_1 + a_2) (some 1) (some 2) (some 3) : Option Nat
  -- leanprover/lean4:nightly-2021-12-04
  --   failed to synthesize instance
  --      Applicative Option

[Kaushik Chakraborty]

what changed from m2 to nightly that this error is happening ? How to fix the same ?

[Henrik Böving]

Option is not a type that carries instances for Applicative Monad etc. anymore, it has been replaced by OptionM which is basically an OptionT with an Id Monad which makes them definitionally equivalent:

example  : OptionM α = Option α := by rfl

so f you tell the liftA3 here that you are actually passing in OptionM Nat it will automatically convert the other Option Nat into OptionM Nat as well, e.g.:

def foo : OptionM Nat :=  (some 1)
#check liftA3 (· + · + ·) foo (Option.some 2) (Option.some 3)

maybe there is an even smarter way to do this? But it can definitely be made to work this way. @Kaushik Chakraborty

[Kaushik Chakraborty]

thanks @Henrik Böving

[Kaushik Chakraborty]

@Henrik Böving I see this line here which is what you mentioned above

abbrev OptionM (α : Type u) := OptionT Id α

curious what's the difference between abbrev and def (abbrev is never mentioned in any of the docs) ?

[Mac]

@Kaushik Chakraborty abbrev makes the definition be immediately inlined in things like typeclass resolution. This means that an abbrev definition will inherit the instances of its right-hand side (e.g., OptionM will inherit the instances of OptionT Id α). A normal def, on the other hand, will not.