Instances cannot be found when records are directly involved
Opened this issue · 0 comments
viluon commented
state.ml
open import "prelude.ml"
type state 's 'a = State of 's -> 'a * 's
instance functor (state 's) begin
let f <$> State a = State (fun s -> let (a, s) = a s in (f a, s))
end
instance applicative (state 's) begin
let pure a = State (fun s -> (a, s))
let State sf <*> State sa = State (fun st -> let (f, st) = sf st in let (a, st) = sa st in (f a, st))
end
instance monad (state 's) begin
let State a >>= f = State (fun s -> let (a, s) = a s in let State sb = f a in sb s)
end
class monad_state 'm 's | 'm -> 's begin
val get: 'm 's
val put: 's -> 'm ()
end
instance monad_state (state 's) 's begin
let get = State (fun s -> (s, s))
let put s = State (fun _ -> ((), s))
end
open import "prelude.ml"
open import "./state.ml"
type int_state <- state {i: int}
let oof (): int_state () =
let! n = get
put (n.i + 1)
let rec run (): int_state () =
let! _ = oof ()
run ()
transcript
src/intstate.ml[11:9 ..14:1]: error (E2018)
No instance for monad_state (state { i : int }) Public.int arising from use of the expression
│
12 │ let! _ = oof ()
│ ^^^^^^
• Note: this constraint was not quantified over because
recursive binding groups must have complete type signatures
in all of their bindings.
│
11 │ let rec run (): int_state () =
│ ^^^^^^^^^^^^^^^^^^^^^^
This binding should have had a complete type signature.
The following message has a detailed explanation: 2018.
Try 'amc explain 2018' to see it.