SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

Incorrect warning about exhaustiveness for shadowed constructors

Open elpinal opened this issue 3 years ago • 0 comments

Taking inspiration from #261, I've found that SATySFi misjudges exhaustiveness of patterns when constructors are shadowed.

shadow-con.saty:

type t =
  | A
  | B

type u =
  | A  % Shadows the previous `A`.

let f x = match x with
  | B -> 4
  | _ -> 7  % We cannot refer to `A` of type `t` so use `_` instead.

in

page-break
  A0Paper
  (fun _ -> (|text-height = 0pt; text-origin = (0pt, 0pt)|))
  (fun _ -> (|header-content = block-nil; header-origin = (0pt, 0pt);
              footer-content = block-nil; footer-origin = (0pt, 0pt);
            |))
  block-nil

This code results in an unexpected warning: pattern #2 is unused.

$ satysfi shadow-con.saty:

 ---- ---- ---- ----
  target file: 'shadow-con.pdf'
  dump file: 'shadow-con.satysfi-aux' (already exists)
  parsing 'shadow-con.saty' ...
 ---- ---- ---- ----
  type checking 'shadow-con.saty' ...
! [Warning about pattern-matching] at "shadow-con.saty", line 8, character 10 to line 10, character 10
    pattern #2 is unused

  type check passed. (document)
  preprocessing 'shadow-con.saty' ...
 ---- ---- ---- ----
  evaluating texts ...
  evaluation done.
 ---- ---- ---- ----
  breaking contents into pages ...
  all cross references were solved.
 ---- ---- ---- ----
  embedding fonts ...
 ---- ---- ---- ----
  writing pages ...
 ---- ---- ---- ----
  output written on 'shadow-con.pdf'.

Version

SATySFi version 0.0.5

elpinal avatar Feb 10 '21 13:02 elpinal