Eta contraction doesn't seem to work correctly in some cases

Issue #21 resolved
Dominic Mulligan
created an issue

In Kayvan and Justus' CSEM development there is the following line:

let list_diff eq = List.fold_left (fun x y -> delete eq y x)

This causes Lem to raise the following internal error:

File "global.lem", line 47, character 20 to line 47, character 60 processed by: do_substitutions LEM internal error: type mismatch: bind_free_env 'a and list 'b in binding e

Replacing the line above with the fully eta-expanded version:

let list_diff eq l e = List.fold_left (fun x y -> delete eq y x) l e

Is accepted by the system fine.

Comments (8)

  1. Dominic Mulligan reporter

    OK, I can't reproduce that. Running:

    ../../lem/lem -lib ../../lem/library multiset.lem global.lem

    In the CSEM/model directory the files process fine. The only backend where this problem occurs is in the Coq backend, apparently. Given do_substitutions is what apparently applies macros it seems one of the Coq macros is doing something funny with types (changing types, or something similar) but is not being picked up properly by the checks meant to ensure that macros are type preserving, causing an internal error at runtime.

  2. Dominic Mulligan reporter

    Ah, I see. More complete test case:

    let rec delete eq x = function
      | []    -> []
      | y::ys -> if eq x y then ys else y :: delete eq x ys
    let list_diff eq = List.fold_left (fun x y -> delete eq y x)
  3. Log in to comment