Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix/t3152 find member #338

Merged
merged 72 commits into from
Jan 31, 2015
Merged

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jan 27, 2015

Is based on #331. Review by @smarter

Moved working tests to pos, annotated non-working ones.
Cases handled are:

     Null <: (A & B) { ... }
     Null <: (A | B) { ... }
Plus, RefinedThis gets a second parameter, `level`. This will replace the first one in due time.
Given

    class C { type T }
    C { type U = this.T } { val x: U }

the second refinement does refer via the alias to the refinement type itself.
Capture original types in enclosing scope instead of passing them
explicitly.
Temporary solution for better diagnsitics.
When doing a findMember we now look at the level of a RefinedThis instead
of its `rt` field. This required several fixes to how levels are assigned
to RefinedThis types.
Cyclic reference was caused when compiling pos/i94-nada.scala with

    typer = new Printer

and -Yfront set.
Symptom was: When compiling Definitions.scala with the changes in the subsequent
commits, an empty tree was passed as implicit parameter, without an "implicit not found"
error being reported. The problem needed a fix in TyperState.
We will need that at some point because type checking refined types will generate skolem
variables for representing RefinedThis types if the lower type is not a singleton.
- Instead of rebasing, use the DeBrujn level of a RefiendThis.
- Make sure lower type is a singleton by skolemizing it if necessary.
- Do the correct rebinding of the upper type's RefinedThis.

Remarks:

 - The new scheme discovered quite a lot of errors which are mostly fixded in
other commits of this branch. i0268 (GADT matching) still does not work, moved to pending.

 - Some optimizations are currently missing:
   (1) fast path refined subtyping
   (2) faster operations for substituting refined thistypes which
       explot the fact that RefinedThis is relatively rare.
The previous scheme did not ensure that transitivity was eliminated.
Example scenario:

We have in the constraint

   P <: Q

for constrained variables P, Q and add

   Q <: T

Previous propagation added the constraint and then tested
whether the bounds of all variables were satisfiable. For
Q we test

    P <: T

but that is true because P <: Q and we already added the constraint Q <: T.
So we fail to add the constraint P <: T, and transitivity is no longer eliminated.

Instead we now test the new bounds (in this case P <: T) *before* adding
the new constraint Q <: T. This is also simpler than the previous scheme.
Now that new scheme works we can drop the alternative.
... into a new trait "Skolemization".
Since we cache the information whether a refinement contains RefinedThis
occurrences to the refinement itself, we can use this info to avoid substututing
RefinedThis types. Used in findMember and hasMatchingMember.

The commit uncovered an issue with constraint handling that will be fixed in the next commit.
After last commit, dotc/config died with the "isSatisfiable" assertion
in TypeComparer. The problem was that when deeling with a variable/variable
constraint

  A <: B

we treated this as the two independent actions of adding

  A <: B
  B >: A

But this means we no longer have a clean inductive satisfiability check before
something gets added - A <: B gets added before the satisfiability check of B >: A
is started. The fix splits satisfiability check and actual constraint update in
two separate actions.
As before, optimize for the case where correspnding refinements
have the same name and the lower one is a type alias.
The previous idea to keep original types around in `origN` types
to be accessed from nested methods was not needed in the end.
A configuratin now decides whether fast path is taken or not. That way
we can more easily test either way if something goes wrong.
Dropped a member calculation which was unncessessary and which would not work
anymore if RefinedThis types lost their RefinedType target field.
See comment for an example what changes.
Move non-essential code to diagnostics plus some other small cleanups.
Since the binder field in RefinedTypes should not be significant for
subtyping, we need to substitute RefinedThis types away before comparing
refinements. But this substitution is only done in the slow path.
The fix falls back to the slow path if a refinement
refers to the refined type via a refined this.
Checks are no longer interesting because we will not to migrate to
RefinedThis(level) scheme after all.
New constraint handling scheme using constraints that distinguish more between
parameter and non-parameter bounds and which track parameter bounds separately.
This allows a co-inductive formulation of satisfiability checking without fishy
cyclicity checks. It should also scale better for long chains of dependent type
variables.
addConstraint contained a special case where a situation like

  P { ... } <: P

was short-pathed to `return true`. But the same was not done
if the constraint was added indirectly by propagation. It's not clear
whether a special treatement of this is needed for correctness. If
it is needed, then it would be needed eberywhere. So wince we do
not want to implement it everywhere wihtout proof of necessity,
it is better to fail fast and drop the special treatment entirely.
SubType check is true anyway, no need to spend work. Also this allows a more
consistent treatment of bounded wildcard types in addConstraint and isSubType. In both cases
we now compare with the outer bound of the wildcard type. Previously addConstraint treated
boundes wildcard types like unbounded ones, which is not consistent.
dropParamsIn extrapolates parameters with Nothing/Any. This has nothing
to do with unification! The dropParamsIn transform could not be eleiminated
previously because it caused faulures. Nice to see that it works now!
They were too sweeping, served essentially as smkoke-screens for debugging until
now. Example:

  checkBound(P, P | T)

would fail even though P | T is a legal upper bound for P. (It's an illegal
lower bound).
GADTs now work again (they stopped workign when we went to the inductive satisfiability checks).
The deep for expression also works, even with some more levels added.
Two named types with same names and NoPrefix prefixes are not necessarily equal!
The fix uncovered an error in tailrec. When run on Decorators.scala, tailrec in its old
position at the end of a group produces not -Ycheckable code. Problem was fixed
by moving TailRec into its own group.
Moved comparisons between ThisType x$.this and NamedType x.type
where x$ is the module class of x. They were uner NamedType, are
now under ThisType. That way NamedType reasoning is a bit uncluttered.
GADT handling goes towards the back. Dealiasing is done early.
Eventual aim: Avoid redoing dealising when adding constraints.
Mostly cosmetic, to make code clearer.
Motivation: Would like to profit from normalizations done before, so that
we do not have to redo them in addConstraint.

Also: eliminate solvedConstraint; it is no longer needed and was always false.
Only run if a config option is set.
Drop unused pattern vars, redundant tests, indentation changes.
unify now does a full `replace` of one parameter with the other. The previous
scheme of just updating the entry of a parameter risks breaking constraint
invariants. In particular, other constraint bounds can still refer to the eliminated
parameter. This might not be a problem, but then we should be systeamtically leaving
these references in everywhere. In any case it seems better to harmonize what unify
and replace are doing.
Allows to merge the functionality of addOneLowerBound and addOneUpperBound in
ConstraintHandling.
This is one both a bit simpler and a faster than TrackingConstraint.
Main change is to replace the 2-d bitmap for ordering with two SimpleMaps
which record for each parameter the smaller and greater parameters.
This is faster in practice because the ordering relation is sparse.
Special cases for comparing Any (and now also Nothing) restricted
to comparing TypeBounds, where they occur most often.
Also, added tests trhat work now.
See comment in OrderingConstraint#replace.
Without it, we get strange error messages like

    found: (implicit X)Y
    requred: Z

when the problem is really that Y is not a subtype of Z.
t3152 shows that Apply projections can also appear in the
lower of two compared types. This patch handles them. It is
necessary, but not sufficient, to fix t3152.
If a PolyParam has an upper bound in the current constraint, this
bound needs to be assumed when selecting members. Final patch to fix t3152.
@smarter
Copy link
Member

smarter commented Jan 28, 2015

This patch LGTM.

odersky added a commit that referenced this pull request Jan 31, 2015
@odersky odersky merged commit 698935a into scala:master Jan 31, 2015
@allanrenucci allanrenucci deleted the fix/t3152-findMember branch December 14, 2017 19:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants