SATySFi
SATySFi copied to clipboard
Incorrect warning about exhaustiveness for shadowed constructors
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