Support Existential Recursion

[johnynek]

the encoding of existential types forall a. (forall b. (P[b] -> a) -> a) inside a recursive data type currently isn't supported.

It should be safe for covariant paths to the same time inside the P[b] in the above.

[johnynek]

the test here needs more than just better recursion checking, it also needs polymorphic recursion, which I'm not sure I would even want to add (monomorphic recursion means we could monomorphize in principle before emitting code, which could be very nice if we ever wanted to add an optimizing back end).

It would be nice to find a test that separates the concerns.

[codecov-commenter]

Codecov Report

Merging #1022 (9349c65) into master (ac20cad) will increase coverage by 0.14%. The diff coverage is 97.43%.

:exclamation: Your organization is not using the GitHub App Integration. As a result you may experience degraded service beginning May 15th. Please install the Github App Integration for your organization. Read more.

@@            Coverage Diff             @@
##           master    #1022      +/-   ##
==========================================
+ Coverage   91.95%   92.09%   +0.14%     
==========================================
  Files          90       90              
  Lines        9381     9409      +28     
  Branches     2172     2204      +32     
==========================================
+ Hits         8626     8665      +39     
+ Misses        755      744      -11     

Files Changed	Coverage Δ
core/src/main/scala/org/bykn/bosatsu/Pattern.scala	96.22% <ø> (ø)
...ain/scala/org/bykn/bosatsu/DefRecursionCheck.scala	97.25% <97.43%> (-0.15%)	:arrow_down:

... and 7 files with indirect coverage changes

[johnynek]

Thinking on this algorithm more:

The variance/kind checker already bans recursive ADTs where the recursion isn't covariant. So, I think this checker only needs to check that we are calling the function on something reachable only an arg in the recur position.

I think the algorithm could work like this: we track all the names in the recur pattern for the branch. We allow a recursive call in the correct index of a parameter reachable from one of those names. We say it is reachable if:

1. it is one of those names
2. it is an argument of a lambda passed to a reachable name.

thus once we are in a branch, we have to track all the shadowing bindings which could confuse us into thinking we are using a name from a match (or reachable) when in fact we aren't.

[johnynek]

we can pick this back up after #1041