Scala implementation of space logic
expose abstract type references to their bounds or tvars according to variance
Abstract sealed types, or-types, Boolean and Java enums can be decomposed
Decompose a type into subspaces -- assume the type can be decomposed
Can this type be inhabited by a value?
Check is based on the following facts:
- single inheritance of classes
- final class cannot be extended
- intersection of a singleton type with another irrelevant type (patmat/i3574.scala)
tp1 to be a subtype of
Return the instantiated type if type parameters and this type
tp1 can be instantiated such that
tp1 <:< tp2.
Otherwise, return NoType.
Whether the extractor is irrefutable
Refine child based on parent
In child class definition, we have:
class Child[Ts] extends path.Parent[Us] with Es object Child extends path.Parent[Us] with Es val child = new path.Parent[Us] with Es // enum values
Given a parent type
parent and a child symbol
child, we infer the prefix
and type parameters for the child:
prefix.child[Vs] <:< parent
Vs are fresh type variables and
prefix is the symbol prefix with all
non-module and non-package
ThisType replaced by fresh type variables.
If the subtyping is true, the instantiated type
NoType is returned.
Whether the counterexample is satisfiable. The space is flattened and non-empty.
Whehter counter-examples should be further checked? True for GADTs.
Show friendly type name with current scope in mind
E.g. C.this.B --> B if current owner is C C.this.x.T --> x.T if current owner is C X[T] --> X C --> C if current owner is C !!!