SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

Cannot report code positions for some error

Open gfngfn opened this issue 2 years ago • 1 comments

Reported by @TonalidadeHidrica at https://satysfi.slack.com.

let f = 1
let a = f RGB(0.1, 0.2, 0.3)
 ---- ---- ---- ----
  target file: '2022-01-29-172058.pdf'
  dump file: '2022-01-29-172058.satysfi-aux' (will be created)
  parsing '2022-01-29-172058.satyh' ...
 ---- ---- ---- ----
  type checking '2022-01-29-172058.satyh' ...
! [Type Error] (cannot report position; 'constructor-unitvalue', 'product')
    this expression has type
      unit,
    but is expected of type
      float * float * float.

gfngfn avatar Jan 29 '22 08:01 gfngfn

This case is roughly processed as below.

  1. Function application and constructor application are left associative, so the parser recognizes f RGB(0.1, 0.2, 0.3) as (f RGB) (0.1, 0.2, 0.3).
  2. In SATySFi, nullary data constructors internally take an unit argument, so the parser supplements an unit argument to RGB: (f RGB) (0.1, 0.2, 0.3) = (f (RGB ())) (0.1, 0.2, 0.3) https://github.com/gfngfn/SATySFi/blob/133dcfb244774db14c19241bc85fc4186c297c89/src/frontend/parser.mly#L812-L815
  3. But the type checker complains: it is a type error; RGB should take a float * float * float argument, not unit.
  4. The error cause is the unit argument, so the error should be reported based on it. But it was introduced by the parser, and has no position information. The implementation cannot report the error position.

There would be several ways fixing this: changing the representation of nullary data constuctors, attaching rough position information to dummy positions, ....

leque avatar Jul 30 '22 00:07 leque