-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Unnecessary exhaustivity warning when combining refinement types w/ params #3469
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
Comments
Thanks a lot for reporting @AleksanderBG . This problem doesn't appear in 9166db3 -- I need to send a PR recently. As you observed in #3454, child instantiation is very tricky, with refinement types, it gets even trickier. AFAIK, child instantiation is the first place where we use inference infrastructure to infer Note child instantiation is needed no matter what algorithm we use. For refinement types, I don't yet see a principled way to do it. |
For clarity's sake: refinement types are not needed to trigger this behaviour. Here's a minimized test from #3454 which doesn't use refinement types, but triggers similar warning (missing pattern for object O {
sealed trait Nat
type Zero = Nat
sealed trait Succ[N <: Nat] extends Nat
sealed trait NVec[N <: Nat, +A]
case class NCons[N <: Nat, +A](head: A, tail: NVec[N, A]) extends NVec[Succ[N], A]
def id[N <: Nat, A](v: NVec[N, A]): NVec[N, A] = v match {
case NCons(h, t) => NCons(h, t)
}
} Perhaps I should clarify what I meant when I said that #3454 w/ typechecker integration handles this correctly. In the PoC, all spaces maintain their own |
Thanks for the detailed reply @AleksanderBG , I think we need to resort to some semantic reasoning here. Unconstrained type parameters have nothing to do with GADT, it can happen in normal types, e.g.: sealed trait Animal
case class Dog[T](x: Array[T]) extends Animal
def foo(an: Animal) : Unit = an match {
case Dog(b: Array[Int]) =>
} In child instantiation, if |
Ah, I think I was misunderstanding wildcard semantics! After some experimentation, it appears that for instance However, I'm not sure if I properly explained how or why I want to use TVars: once a TVar was used in a space's type anywhere, its constraints kept in that space's |
Fixed in #3475. |
The following code:
causes the following warning:
@liufengyun - this happens because the refinement type forces usage of
typeParamMap
ininstantiate
. This in turn initializes the param in the pattern space toAny
, so instead ofCaseClass[A]
we getCaseClass[Any]
. This was found when rebasing #3454 - one test had to be ignored. I should also mention that with the POC typechecker integration I've described in #3454, this code is handled correctly.The text was updated successfully, but these errors were encountered: