Skip to content

Commit

Permalink
chore: modify MonadStats to not extend parents multiple times
Browse files Browse the repository at this point in the history
MonadStats was extending `MonadLiftT` twice, but the two parents were defeq. This was a hack to get around the fact that the parent instances were providing `MonadLiftT` instances rather than a `MonadLift` instance, breaking `MonadLiftT` inference.

This changes it to *not* extend `MonadLiftT`, instead embedding it as a field, and then writing an explicit `MonadLift` instance.

This is motivated by [lean4#5770](leanprover/lean4#5770), which will log warnings when structures extend parents multiple times.
  • Loading branch information
kmill committed Oct 19, 2024
1 parent b20a886 commit cdea48a
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions Aesop/Stats/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -175,12 +175,12 @@ end Stats

abbrev StatsRef := IO.Ref Stats

class MonadStats (m) extends
MonadLiftT (ST IO.RealWorld) m,
MonadLiftT BaseIO m,
MonadOptions m where
class MonadStats (m) extends MonadOptions m where
[instLift : MonadLiftT BaseIO m]
readStatsRef : m StatsRef

instance [MonadStats m] : MonadLift BaseIO m := ⟨MonadStats.instLift.monadLift⟩

export MonadStats (readStatsRef)

variable [Monad m]
Expand Down

0 comments on commit cdea48a

Please sign in to comment.