Skip to content

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

@zachhalle

Description

@zachhalle

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions