Skip to content

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

Closed
abgruszecki opened this issue Nov 14, 2017 · 5 comments
Closed

Comments

@abgruszecki
Copy link
Contributor

The following code:

object O {
  sealed trait Trait[+A] { type T }
  case class CaseClass[+A](a: A) extends Trait[A] { type T = Nothing }

  def id[TT, A](v: Trait[A] { type T = TT }): Trait[A] { type T = TT } =
    v match {
      case CaseClass(a) => CaseClass(a)
    }
}

causes the following warning:

-- [E028] Pattern Match Exhaustivity Warning: sample/1:6:4 ---------------------
6 |    v match {
  |    ^
  |    match may not be exhaustive.
  |
  |    It would fail on: CaseClass(_)

@liufengyun - this happens because the refinement type forces usage of typeParamMap in instantiate. This in turn initializes the param in the pattern space to Any, so instead of CaseClass[A] we get CaseClass[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.

@liufengyun
Copy link
Contributor

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 prefix and refinement, it's largely unexplored land.

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.

@abgruszecki
Copy link
Contributor Author

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 NCons):

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 Context. This allows leaving uninstantiated TypeVars in the types, which in turn means they get more precise. Consider, for example, that the proper type to which ::[B] should be instantiated when decomposing List[A] is not ::[A], but ::[C] forSome C <: A (this was already described by @smarter here). So far, I haven't seen a way of expressing such a type without using TypeVars. Bounded wildcards are similar, but they don't capture the notion that there is a precise, underlying type. Keeping TypeVars, on the other hand, smoothly handles both examples for this issue. The initial example is handled correctly since A in Trait[A] already starts replaced with a TypeVar, so there's no need for a typeParamMap in instantiate. After I clean up commits in #3454, it should (hopefully) be easier to see what additional changes there are in the PoC and to discuss them.

@liufengyun
Copy link
Contributor

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 T is unconstrained, it means any types are possible, thus a wildcard with appropriate bounds is the best instantiation. The patterns need to handle all possible instantiations of the type. In contrast, putting a TVar to be unified later is incorrect.

@abgruszecki
Copy link
Contributor Author

Ah, I think I was misunderstanding wildcard semantics! After some experimentation, it appears that for instance Dog[_] is precisely what I would denote as Dog[K] forSome K. I understand now why using wildcards is correct here.

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 Context are not adjusted. TVars are only there so that additional constraints can be added to new Contexts created when decomposing spaces. I wanted to highlight that if we go through with typechecker-integrated #3454, this issue would automagically be solved as well.

@liufengyun
Copy link
Contributor

Fixed in #3475.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants