Do not rely on any explicitness information for inference and constraint resolution

[umazalakain]

Currently we use a global set of type variables to preserve, but we still rely on explicitness information to preserve bound variables. Given that we have globally unique variable names we can simply add every bound variable to the set of variables to preserve. The preserve set needs to be modified in recursive calls to solveOne (we currently don't have to do that because we use _.asImplicit on some variables instead).

Fragment kinds and matrix layouts are now traversed too and their identifiers are correctly picked up. These identifiers are however ignored by makeClosed, because they cannot be bound.

IsClosedForm now correctly traverses lambdas, it used to skip their types.

It doesn't seem to make a noticeable impact on the performance of the test suite.

[Bastacyclop]

Looks like a good solution to me overall. I think that we should unify the terminology around "preserve"/"bound"/"scope"/"environment" in the code and variable names. For the explicitlyDependent stuff maybe you should talk to @fedepiz .

PS: what tests are currently failing?

[Bastacyclop]

+ n? same in other spots. I wonder if we could also alternatively directly apply the required substitutions (na -> n and nb -> n) where necessary and only generate 1 constraint instead of 3 here. Something like:

val n = NatIdentifier(freshName("n"))
decomposed(Seq(TypeConstraint(
  substitute.natsInType(ta, Map(na -> n)),
  substitute.natsInType(tb, Map(nb -> n))
))), preserve + n)

[umazalakain]

Yup, I was just picking up on that, I will get back to you!

[umazalakain]

@Bastacyclop Regarding the naming, I think it would make sense to use "typing environment" or "typing context" on the infer side: it is more than a scope, since it has kinding information; it is in line with using "exprEnv" for the expression world, and we are not yet concerned about how this typing environment is used. On the constraints side I would switch to "preserve", since we add and remove things to it regardless of any typing contexts.

I added the explicit variables that we create to the preserve set (I think it's best if we leave making any optimizations for later on once the tests pass). There are 13 tests that don't pass, I will send you a file with the results on zulip.

Re the dependent types @fedepiz, I tried collecting the identifiers that are made implicit into a set and then subtracting those from the preserve set in lines 133-135, but it didn't seem to help.

[fedepiz]

One quick remark about explicit dependence. I have in recent times started to phase it out in my work. and prefer instead throwing the compiler more handwritten constraints until it's happy. That's because it can only infer some marginally more complex situations, but in the end, writing out one type of signature can save your bacon much more reliably.

So, if the explicit dependence stuff is getting in the way, please feel free to throw the mechanism and the few associated tests that might fail if you don't feel like providing type signatures for some alien-looking tests. As long as most of the basic dependent stuff is in place, then I am more than happy with it.

[umazalakain]

Thomas and I had a meeting and identified some of the possible things that might have been going wrong (there are about 10 test cases that don't pass currently) and talked about a possible roadmap:

• Solutions should not substitute within opaques. Moreover, solutions should not contain type variables of opaques as keys. We should add an assertion that makes sure of this.
• At some point we can remove the explicitly dependent stuff if it gets in the way.
• Rewrites need to happen a la eqsat: get the expression and type environment from the LHS, give those to the inference that is being ran on the RHS. This removes the need for type assertions.
• There is no need for per-subconstraint environment information in solveOne, preservation information should be shared among subcontraints.
• What happens to the environment information attached to a constraint when substitutions are applied to that constraint? Substitutions should also be applied to the environment information.
• Does the application of solutions need to be scoped? Add the following test case:

  ((dt1 : data) -> _x) _x
  ((dt2 : data) -> dt2) _x
  

  inference creates a new type variable dt and substitutes dt1 |-> dt and dt2 |-> dt:

  ((dt : data) -> _x) _x
  ((dt : data) -> dt) _x
  

  then inference creates a constraint _x ~ dt resulting in the substitution _x |-> dt. applying this substitution globally gives

  ((dt : data) -> dt) dt
  ((dt : data) -> dt) dt
  

  however note that here the function argument dt is not bound: the expression is ill-scoped.

[Bastacyclop]

Looks good to me. Maybe we can open relevant issues for the points discussed in #174 (comment) ?

[umazalakain]

@Bastacyclop will do, thanks for the review!

[umazalakain]

Looks good to me. Maybe we can open relevant issues for the points discussed in #174 (comment) ?

I created issues for the first #177 and last #178 points, the rest has been resolved