Skip to content

Bug Fix: Function Application in Bidirectional Type Checking

Alistair O'Brien requested to merge ajob410/bidir-bug-fix-1 into dev

type:fixed

Bug: Adding constant C_ID : forall 'a. 'a -> 'a resulted in inconsistent errors:

let id (type a) (x : a) : a = [%external ("ID", x)]

let sum (_x : unit) (_y : unit) : unit = ()

let main (_ : unit * unit) : operation list * unit =
  (* OK *)
  (* let s : unit = (id ((id sum) ())) () in *)
  (* not OK *)
  let s : unit = [%external ("ID", ([%external ("ID", sum)] ()))] () in
  (([] : operation list), s)
Underspecified type ^gen#448.

Source of the bug was a difference between implementation and specified typing rule for function application: Screenshot_2022-09-07_at_10.17.27

Changelog details:

Bug fix for function application in bidirectional type checking

Merge request reports