No more useless subst

[HoshinoTented]

The subst of parameters of Ctor now disappear after tyck that Pat.Ctor. For example:

open data Nat
| O
| S (_1 : Nat)

def justMatch (m n : Nat) : Nat
| O, n => O
| S m', n => m'

There is a subst _1 |-> m' when we tyck the n pattern in | S m', n => m', which is useless.

[codecov]

Codecov Report

Merging #623 (f677dcd) into main (a9f7355) will increase coverage by 0.00%.
The diff coverage is 96.55%.

❗ Current head f677dcd differs from pull request most recent head c91c451. Consider uploading reports for the commit c91c451 to get more accurate results

@@            Coverage Diff            @@
##               main     #623   +/-   ##
=========================================
  Coverage     79.96%   79.97%           
- Complexity     2815     2818    +3     
=========================================
  Files           229      229           
  Lines          8906     8920   +14     
  Branches       1097     1097           
=========================================
+ Hits           7122     7134   +12     
- Misses         1195     1197    +2     
  Partials        589      589           

Impacted Files	Coverage Δ
base/src/main/java/org/aya/tyck/pat/PatTycker.java	91.10% <96.15%> (+0.39%)	⬆️
base/src/main/java/org/aya/core/visitor/Subst.java	90.47% <100.00%> (+0.47%)	⬆️
...ase/src/main/java/org/aya/tyck/pat/TypedSubst.java	100.00% <100.00%> (ø)
...main/java/org/aya/cli/library/LibraryCompiler.java	82.51% <0.00%> (-1.18%)	⬇️

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

[ice1000]

bors r+

[bors]

Build succeeded:

• commit-check
• gradle-check