Skip to content
This repository has been archived by the owner on Oct 18, 2021. It is now read-only.

Instances cannot be found when records are directly involved #293

Open
viluon opened this issue Feb 25, 2021 · 0 comments
Open

Instances cannot be found when records are directly involved #293

viluon opened this issue Feb 25, 2021 · 0 comments
Labels
bug TC: Type Classes Issues/PRs relating to the type checking of definitions of type classes and instances

Comments

@viluon
Copy link

viluon commented Feb 25, 2021

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 ()

image

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.
@SquidDev SquidDev added bug TC: Type Classes Issues/PRs relating to the type checking of definitions of type classes and instances labels Feb 27, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug TC: Type Classes Issues/PRs relating to the type checking of definitions of type classes and instances
Projects
None yet
Development

No branches or pull requests

2 participants