refactor: don't extend Applicative in Alternative

src/Init/Control/Basic.lean

@@ -97,7 +97,7 @@ Error recovery and state can interact subtly. For example, the implementation of
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add
 -- * `List`, where `failure` is the empty list and `<|>` concatenates.
-class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicative f where
+class Alternative (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
   from failures. See `Alternative` for more details.
@@ -111,20 +111,18 @@ class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicati
 
 instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orElse⟩
 
-variable {f : Type u → Type v} [Alternative f] {α : Type u}
-
 export Alternative (failure)
 
 /--
 If the proposition `p` is true, does nothing, else fails (using `failure`).
 -/
-@[always_inline, inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
+@[always_inline, inline] def guard {f : Type → Type v} [Alternative f] [Pure f] (p : Prop) [Decidable p] : f Unit :=
   if p then pure () else failure
 
 /--
 Returns `some x` if `f` succeeds with value `x`, else returns `none`.
 -/
-@[always_inline, inline] def optional (x : f α) : f (Option α) :=
+@[always_inline, inline] def optional {f : Type u → Type v} {α : Type u} [Alternative f] [Applicative f] (x : f α) : f (Option α) :=
   some <$> x <|> pure none
 
 class ToBool (α : Type u) where

src/Init/Control/Reader.lean

@@ -31,7 +31,7 @@ Fails with a recoverable error.
 protected def failure [Alternative m] : ReaderT ρ m α :=
   fun _ => failure
 
-instance [Alternative m] [Monad m] : Alternative (ReaderT ρ m) where
+instance [Alternative m] : Alternative (ReaderT ρ m) where
   failure := ReaderT.failure
   orElse  := ReaderT.orElse
 

src/Init/Control/StateRef.lean

@@ -63,7 +63,7 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
 instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
-instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
+instance [Alternative m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 instance [Monad m] [MonadAttach m] : MonadAttach (StateRefT' ω σ m) := inferInstanceAs (MonadAttach (ReaderT _ _))
 
 /--

src/Init/Data/Option/Basic.lean

@@ -58,12 +58,12 @@ deriving instance BEq for Option
 @[simp, grind =] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
 
 /-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/
-def getM [Alternative m] : Option α → m α
+def getM [Alternative m] [Pure m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[simp, grind =] theorem getM_none [Alternative m] : getM none = (failure : m α) := rfl
-@[simp, grind =] theorem getM_some [Alternative m] {a : α} : getM (some a) = (pure a : m α) := rfl
+@[simp, grind =] theorem getM_none [Alternative m] [Pure m] : getM none = (failure : m α) := rfl
+@[simp, grind =] theorem getM_some [Alternative m] [Pure m] {a : α} : getM (some a) = (pure a : m α) := rfl
 
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
@@ -582,7 +582,7 @@ instance : Alternative Option where
   orElse  := Option.orElse
 
 -- This is a duplicate of `Option.getM`; one may be deprecated in the future.
-def liftOption [Alternative m] : Option α → m α
+def liftOption [Alternative m] [Pure m] : Option α → m α
   | some a => pure a
   | none   => failure
 

src/lake/Lake/Util/Lift.lean

@@ -10,7 +10,7 @@ public import Init.System.IO
 
 namespace Lake
 
-public instance (priority := low) [Monad m] [MonadExceptOf PUnit m] : Alternative m where
+public instance (priority := low) [MonadExceptOf PUnit m] : Alternative m where
   failure := throw ()
   orElse := tryCatch
 
@@ -20,7 +20,7 @@ public instance (priority := high) [MonadLift α β] : MonadLiftT α β := ⟨Mo
 public instance (priority := low) [Pure m] : MonadLiftT Id m where
   monadLift act := pure act.run
 
-public instance (priority := low) [Alternative m] : MonadLiftT Option m where
+public instance (priority := low) [Alternative m] [Pure m] : MonadLiftT Option m where
   monadLift
     | some a => pure a
     | none => failure

src/lake/Lake/Util/Log.lean

@@ -215,7 +215,7 @@ public abbrev stream [MonadLiftT BaseIO m]
   (out : IO.FS.Stream) (minLv := LogLevel.info) (useAnsi := false)
 : MonadLog m where logEntry e := logToStream e out minLv useAnsi
 
-@[inline] public def error [Alternative m] [MonadLog m] (msg : String) : m α :=
+@[inline] public def error [Applicative m] [Alternative m] [MonadLog m] (msg : String) : m α :=
   logError msg *> failure
 
 end MonadLog

tests/lean/run/expandWhereStructInstIssue.lean

@@ -1,4 +1,4 @@
-instance [Alternative m] : MonadLiftT Option m where
+instance [Alternative m] [Pure m] : MonadLiftT Option m where
   monadLift := fun
     | some a => pure a
     | none => failure

tests/lean/run/printStructure.lean

@@ -80,34 +80,6 @@ constructor:
 #guard_msgs in
 #print PrivCtor
 
-/-! Extended class -/
-/--
-info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
-number of parameters: 1
-parents:
-  Alternative.toApplicative : Applicative f
-fields:
-  Functor.map : {α β : Type u} → (α → β) → f α → f β :=
-    fun {α β} x y => pure x <*> y
-  Functor.mapConst : {α β : Type u} → α → f β → f α :=
-    fun {α β} => Functor.map ∘ Function.const β
-  Pure.pure : {α : Type u} → α → f α
-  Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
-  SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α :=
-    fun {α β} a b => Function.const β <$> a <*> b ()
-  SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β :=
-    fun {α β} a b => Function.const α id <$> a <*> b ()
-  Alternative.failure : {α : Type u} → f α
-  Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α
-constructor:
-  Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α)
-    (orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f
-field notation resolution order:
-  Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
--/
-#guard_msgs in
-#print Alternative
-
 /-! Multiply extended class -/
 /--
 info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)

tests/lean/run/structInst2.lean

@@ -39,13 +39,11 @@ def optMonad2 {m} [Monad m] : Monad (OptionT m) :=
 
 def optAlt1 {m} [Monad m] : Alternative (OptionT m) :=
 { failure       := OptionT.fail,
-  orElse        := OptionT.orElse,
-  toApplicative := Monad.toApplicative }
+  orElse        := OptionT.orElse }
 
 def optAlt2 {m} [Monad m] : Alternative (OptionT m) :=
-⟨OptionT.fail, OptionT.orElse⟩ -- it works because it treats `toApplicative` as an instance implicit argument
+⟨OptionT.fail, OptionT.orElse⟩
 
 def optAlt3 {m} [Monad m] : Alternative (OptionT2 m) :=
 { failure       := OptionT2.fail,
-  orElse        := OptionT2.orelse,
-  toApplicative := Monad.toApplicative }
+  orElse        := OptionT2.orelse }