Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Instance search fails to terminate on "simple" example #51

Open
zachhalle opened this issue Jun 29, 2016 · 0 comments
Open

Instance search fails to terminate on "simple" example #51

zachhalle opened this issue Jun 29, 2016 · 0 comments

Comments

@zachhalle
Copy link

zachhalle commented Jun 29, 2016

The following is the source for "implicits.ml"

module type Show = sig
  type t
  val show : t -> string
end

let show {S : Show} (e : S.t) = S.show e
let writeln {S : Show} (e : S.t) = print_endline (S.show e)

implicit module IntShow = struct
  type t = int
  let show = string_of_int
end

module type Functor = sig
  type 'a t
  val map : ('a -> 'b) -> ('a t -> 'b t)
end

let map {F : Functor} f c = F.map f c

type 'a tree = Leaf | Node of 'a * 'a tree * 'a tree

implicit module TreeFunctor = struct
  type 'a t = 'a tree
  let rec map f tr = match tr with
    | Leaf -> Leaf
    | Node (x,l,r) -> Node (f x, map f l, map f r)
end

implicit module TreeShow {S : Show} = struct
  type t = S.t tree
  let rec show tr = match tr with
    | Leaf -> "Leaf"
    | Node (x,l,r) -> "Node (" ^ S.show x ^ ", " ^ show l ^ ", " ^ show r ^ ")"
end

let rec mkTree n = match n with
  | 0 -> Leaf
  | n -> let tr = mkTree (n-1) in Node (n, tr, tr)

let _ =  writeln (map (fun x -> x mod 2) (mkTree 3))

When compiled (command: ocamlopt implicits.ml) the following error message is shown:

File "Implicits.ml", line 43, characters 9-16:
Error: Termination check failed when searching for implicit S.

If the last line is changed to the following,

let tr = map (fun x -> x mod 2) (mkTree 3)
let _ = writeln tr

It compiles without incident.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant