Skip to content

Check GADT ordering for HKTs in TypeComparer #11910

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

Merged
merged 4 commits into from
Mar 29, 2021

Conversation

Linyxus
Copy link
Contributor

@Linyxus Linyxus commented Mar 26, 2021

Since the current TypeComparer calls GadtConstraint.bounds to check GADT bounds of HKTs, the GADT ordering between two HK type parameters will not be available when comparing them. The following snippet illustrates the issue.

final class HktInv[F[_]]
final class HktVar[+F[_]]

def foo[F[_], G[_], X](m : HktInv[G]) = m match {
  case _ : HktInv[F] =>
    val fx : F[X] = ???
    val gx : G[X] = fx  // pass! `F` has been instantiated to `G` 
                        // and thus the bound F =:= G is accessible from `bounds`.
}

def baz[F[_], G[_], X](m : HktVar[G]) = m match {
  case _ : HktVar[F] =>
    val fx : F[X] = ???
    val gx : G[X] = fx  // error. `F` has only ordering constraints F <:< G 
                        // and such ordering will not be available to TypeComparer via `bounds`.
}

The orderings will be available via fullBounds, but this method may result in dead loops if used in TypeComparer. This PR fixes this issue by checking ordering constraints between HKTs with isLess in TypeComparer.

@abgruszecki

@abgruszecki abgruszecki self-requested a review March 26, 2021 18:25
The condition check on injectivity related to GADT ordering usage is
unnecessary. For any subtyping relation F <:< G here, if the relation relied on
GADT ordering, then both F and G are contained in GADTConstraint, which implies
that both F and G are type parameters; neither `tycon1sym.isClass` nor
`tycon2sym.isClass` will be true.
Copy link
Contributor

@abgruszecki abgruszecki left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Good job with the fix.

@abgruszecki abgruszecki merged commit e7a6e31 into scala:master Mar 29, 2021
@Kordyjan Kordyjan added this to the 3.0.0 milestone Aug 2, 2023
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