fix: symmetric predicate check runs on empty type graph

[liangyiliang]

Description

Resolves #1110

Symmetric predicate declarations require that the two argument types, T1 and T2, are exactly equal. To check equality, we check that T1 is a subtype of T2, and that T2 is a subtype of T1. This is done by querying the subtype graph.

The issue is that the checks are performed before the computation of the type graph. As an example,

type T1
type T2
symmetric predicate P(T1, T2)

This should fail, since T1 and T2 are not subtypes of each other. Indeed it does (correctly), but it also generates two errors in the browser console hidden from users that T2 is not in the subtype graph.

The overall behavior, exposed to the users, is actually correct, but the hidden error is bad.

This is because the complete type graph hasn't been generated yet.

Implementation strategy and design decisions

We delay the checking of the domain symmetric predicates until after the type graph has been generated. In other words, this is now the order of execution:

• Check all statements except the number of arguments and argument types of symmetric relations
• Generate the type graph
• Check all symmetric predicate arguments

Examples with steps to reproduce them

Here

When we compile this in the previous version, it both yields an error, and outputs something to console.error.

When we compile this in the new version, it yields an error, but no console.error output, which is good.

Checklist

• I have commented my code, particularly in hard-to-understand areas
• My changes generate no new ESLint warnings
• I have reviewed any generated registry diagram changes

[github-actions]

± Registry diff

📊 Performance

Key

Note that each bar component rounds up to the nearest 100ms, so each full bar is an overestimate by up to 400ms.

     0s   1s   2s   3s   4s   5s   6s   7s   8s   9s
     |    |    |    |    |    |    |    |    |    |
name ▝▀▀▀▀▀▀▀▀▀▀▀▚▄▄▄▄▄▄▄▄▄▞▀▀▀▀▀▀▀▀▀▀▀▀▚▄▄▄▄▄▄▄▄▄▖
      compilation labelling optimization rendering

Data

                                        0s   1s   2s   3s   4s   5s   6s   7s   8s
                                        |    |    |    |    |    |    |    |    |
3d-projection-fake-3d-linear-algebra    ▝▞▖
allShapes-allShapes                     ▝▚▚▄▖
arrowheads-arrowheads                   ▝▞▖
caffeine-structural-formula             ▝▀▀▀▚▀▚
center-shrink-circle-animation          ▝▞▖
circle-example-euclidean                ▝▀▚▀▀▀▚
collinear-euclidean                     ▝▀▞▖
congruent-triangles-euclidean           ▝▀▀▚▚
continuousmap-continuousmap             ▝▚▚
cubic-bezier-cubic-bezier               ▝▚▀▀▚
full-moon-full-moon                     ▝▀▀▚▀▀▚
glutamine-molecules-basic               ▝▀▚▚
half-adder-distinctive-shape            ▝▀▞▚
hypergraph-hypergraph                   ▝▀▀▀▚▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▖
incenter-triangle-euclidean             ▝▀▀▞▖
lagrange-bases-lagrange-bases           ▝▚▚
midsegment-triangles-euclidean          ▝▀▞▖
mobius-mobius                           ▝▞▖
non-convex-non-convex                   ▝▀▞▖
one-water-molecule-atoms-and-bonds      ▝▀▞▖
parallel-lines-euclidean                ▝▀▞▖
persistent-homology-persistent-homology ▝▀▀▚▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▚▖
points-around-line-shape-distance       ▝▀▚▚
points-around-polyline-shape-distance   ▝▀▀▞▖
points-around-star-shape-distance       ▝▀▀▀▚▚
siggraph-teaser-euclidean-teaser        ▝▀▚▚
small-graph-disjoint-rect-line-horiz    ▝▀▀▞▖
small-graph-disjoint-rects              ▝▞▖
small-graph-disjoint-rects-large-canvas ▝▞▖
small-graph-disjoint-rects-small-canvas ▝▚▚
tree-tree                               ▝▀▄▄▞▖
tree-venn                               ▝▀▚▚
tree-venn-3d                            ▝▀▞▄▄
two-vectors-perp-vectors-dashed         ▝▀▞▖
vector-wedge-exterior-algebra           ▝▚▚
wet-floor-atoms-and-bonds               ▝▚▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▀▚
word-cloud-example-word-cloud           ▝▀▞▖
wos-laplace-estimator-walk-on-spheres   ▝▀▀▞▖
wos-nested-estimator-walk-on-spheres    ▝▀▀▚▀▀▀▀▀▀▀▀▚
wos-offcenter-estimator-walk-on-spheres ▝▀▚▀▀▀▀▖
wos-poisson-estimator-walk-on-spheres   ▝▀▚▀▀▖

[codecov]

Codecov Report

Merging #1248 (cc2d159) into main (b21e716) will decrease coverage by 0.02%.
The diff coverage is 100.00%.

@@            Coverage Diff             @@
##             main    #1248      +/-   ##
==========================================
- Coverage   63.45%   63.44%   -0.02%     
==========================================
  Files          61       61              
  Lines        7170     7176       +6     
  Branches     1664     1667       +3     
==========================================
+ Hits         4550     4553       +3     
- Misses       2537     2540       +3     
  Partials       83       83              

Impacted Files	Coverage Δ
packages/core/src/compiler/Domain.ts	84.02% <100.00%> (-1.09%)	⬇️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[cloudflare-pages]

Deploying with    Cloudflare Pages

Latest commit:	cc2d159
Status:	✅  Deploy successful!
Preview URL:	https://eee97a9b.penrose-72l.pages.dev
Branch Preview URL:	https://empty-type-graph.penrose-72l.pages.dev

View logs

[wodeni]

Looks good! Although a little awkward to do a two-pass check, this is totally okay as a fix: . The example seems to work well. Thanks!

[samestep]

Ah clever! LGTM 👍