Skip to content

Commit

Permalink
fix(init/control/state): flip typeclass args for monad_state_trans (#461
Browse files Browse the repository at this point in the history
)

As of 3.7.0c, typeclass resolution solves instance arguments from right-to-left (via #139). #139 also explicitly flips the typeclass arguments of definitions like monad_reader_trans, but does not flip the typeclass arguments of monad_state_trans, causing the following example:

```
def ex1 : option_t (state_t string id) string :=
  do
    s <- get,
    option_t.mk $ return s
```

to return the error: `maximum class-instance resolution depth has been reached`. Flipping the typeclass arguments for monad_state_trans fixes this particular issue.

Closes #460
  • Loading branch information
ammkrn committed Sep 4, 2020
1 parent 96a1980 commit edf549e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion library/init/control/state.lean
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ variables {σ : Type u} {m : Type u → Type v}

-- NOTE: The ordering of the following two instances determines that the top-most `state_t` monad layer
-- will be picked first
instance monad_state_trans {n : Type u → Type w} [has_monad_lift m n] [monad_state σ m] : monad_state σ n :=
instance monad_state_trans {n : Type u → Type w} [monad_state σ m] [has_monad_lift m n] : monad_state σ n :=
⟨λ α x, monad_lift (monad_state.lift x : m α)⟩

instance [monad m] : monad_state σ (state_t σ m) :=
Expand Down

0 comments on commit edf549e

Please sign in to comment.