gfngfn / SATySFi

A statically-typed, functional typesetting system
GNU Lesser General Public License v3.0
1.16k stars 82 forks source link

Cannot report code positions for some error #318

Open gfngfn opened 2 years ago

gfngfn commented 2 years ago

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.
leque commented 2 years ago

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, ....