diff --git a/compiler/src/dotty/tools/dotc/ast/Trees.scala b/compiler/src/dotty/tools/dotc/ast/Trees.scala index 9f72feb216b9..528392bf203d 100644 --- a/compiler/src/dotty/tools/dotc/ast/Trees.scala +++ b/compiler/src/dotty/tools/dotc/ast/Trees.scala @@ -227,8 +227,9 @@ object Trees { case y: List[_] => x.corresponds(y)(isSame) case _ => false } + case x: Constant => x == y case _ => - false + throw new AssertionError(s"Unexpected Tree in Tree comparison $x (comparing to $y)") } } this.getClass == that.getClass && { @@ -605,7 +606,7 @@ object Trees { */ class TypeVarBinder[-T >: Untyped] extends TypeTree[T] - /** ref.type */ + /** ref.type or { ref } */ case class SingletonTypeTree[-T >: Untyped] private[ast] (ref: Tree[T]) extends DenotingTree[T] with TypTree[T] { type ThisTree[-T >: Untyped] = SingletonTypeTree[T] diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala index a9feeae2da99..324af8d4b711 100644 --- a/compiler/src/dotty/tools/dotc/ast/tpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala @@ -540,7 +540,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo { override def If(tree: Tree)(cond: Tree, thenp: Tree, elsep: Tree)(implicit ctx: Context): If = { val tree1 = untpd.cpy.If(tree)(cond, thenp, elsep) tree match { - case tree: If if (thenp.tpe eq tree.thenp.tpe) && (elsep.tpe eq tree.elsep.tpe) => tree1.withTypeUnchecked(tree.tpe) + case tree: If if (cond.tpe eq tree.cond.tpe) && (thenp.tpe eq tree.thenp.tpe) && (elsep.tpe eq tree.elsep.tpe) => tree1.withTypeUnchecked(tree.tpe) case _ => ta.assignType(tree1, thenp, elsep) } } @@ -557,7 +557,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo { override def Match(tree: Tree)(selector: Tree, cases: List[CaseDef])(implicit ctx: Context): Match = { val tree1 = untpd.cpy.Match(tree)(selector, cases) tree match { - case tree: Match if sameTypes(cases, tree.cases) => tree1.withTypeUnchecked(tree.tpe) + case tree: Match if (selector.tpe eq tree.selector.tpe) && sameTypes(cases, tree.cases) => tree1.withTypeUnchecked(tree.tpe) case _ => ta.assignType(tree1, cases) } } diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 49bb1e4eb26e..a51c20c8fffd 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -752,6 +752,8 @@ class Definitions { def ThrowsAnnot(implicit ctx: Context) = ThrowsAnnotType.symbol.asClass lazy val TransientAnnotType = ctx.requiredClassRef("scala.transient") def TransientAnnot(implicit ctx: Context) = TransientAnnotType.symbol.asClass + lazy val TypeOfAnnotType = ctx.requiredClassRef("scala.annotation.internal.TypeOf") + def TypeOfAnnot(implicit ctx: Context) = TypeOfAnnotType.symbol.asClass lazy val UncheckedAnnotType = ctx.requiredClassRef("scala.unchecked") def UncheckedAnnot(implicit ctx: Context) = UncheckedAnnotType.symbol.asClass lazy val UncheckedStableAnnotType = ctx.requiredClassRef("scala.annotation.unchecked.uncheckedStable") diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala index 95301176d78f..5056b7818392 100644 --- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala +++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala @@ -785,6 +785,15 @@ object SymDenotations { def isTransparentMethod(implicit ctx: Context): Boolean = is(TransparentMethod, butNot = Accessor) + /** Are we in a transparent context? + * Either - this symbol has a transparent owner, itself included + * Or - we are inside a SingletonTypeTree + */ + def isTransitivelyTransparent(implicit ctx: Context): Boolean = { + // Note: Should we use a mode instead? + ownersIterator.exists(_.isTransparentMethod) || ctx.outersIterator.exists(_.tree.isInstanceOf[SingletonTypeTree[_]]) + } + def isInlineableMethod(implicit ctx: Context) = isInlinedMethod || isTransparentMethod /** ()T and => T types should be treated as equivalent for this symbol. diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 4efcb0648c12..a961ce6c994d 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -236,6 +236,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling { compareWild case tp2: LazyRef => !tp2.evaluating && recur(tp1, tp2.ref) + case tp2: TypeOf => + tp2 == tp1 || secondTry case tp2: AnnotatedType if !tp2.isRefining => recur(tp1, tp2.parent) case tp2: ThisType => @@ -567,7 +569,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling { false } compareTypeBounds - case tp2: AnnotatedType if tp2.isRefining => + case tp2: AnnotatedType if tp2.isRefining && !tp2.isInstanceOf[TypeOf] => (tp1.derivesAnnotWith(tp2.annot.sameAnnotation) || defn.isBottomType(tp1)) && recur(tp1, tp2.parent) case ClassInfo(pre2, cls2, _, _, _) => diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index b90a5bde2c98..e8af91ff15a4 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -21,7 +21,7 @@ import util.Stats._ import util.{DotClass, SimpleIdentitySet} import reporting.diagnostic.Message import ast.tpd._ -import ast.TreeTypeMap +import ast.{Trees, TreeTypeMap} import printing.Texts._ import ast.untpd import dotty.tools.dotc.transform.Erasure @@ -3707,7 +3707,7 @@ object Types { override def underlying(implicit ctx: Context): Type = parent - def derivedAnnotatedType(parent: Type, annot: Annotation) = + def derivedAnnotatedType(parent: Type, annot: Annotation)(implicit ctx: Context) = if ((parent eq this.parent) && (annot eq this.annot)) this else AnnotatedType(parent, annot) @@ -3929,6 +3929,100 @@ object Types { else None } + // ----- TypeOf ------------------------------------------------------------------------- + + /** Type that represents the precise type of a given term. + * Precision is only kept for Apply, TypeApply, If and Match trees. + * + * The idea behind this type is to be able to compute more precise types + * when more information is available. + * + * TypeOfs are represented by an underlying type and a tree. The top level + * node of the tree must be one of the nodes mentioned above, and is only + * used as a "marker" node, meaning that we will never look at its type. + * + * In a sense, TypeOf types are isomorphic to the following 4 types: + * + * TypeOf(u, Apply(fun, args)) ~ SuspendedApply(u, fun, args) + * TypeOf(u, TypeApply(fun, args)) ~ SuspendedTypeApply(u, fun, args) + * TypeOf(u, If(cond, thenp, elsep)) ~ SuspendedIf(u, cond, thenp, elsep) + * TypeOf(u, Match(selector, cases)) ~ SuspendedMatch(u, selector, cases) + * + * Where u is the type that the tree would have had otherwise. + * + * It should be the case that whenever two TypeOfs are equal, so are their + * underlying types. + */ + class TypeOf private (val underlyingTp: Type, val tree: Tree, annot: Annotation) extends AnnotatedType(underlyingTp, annot) { + assert(TypeOf.isLegalTopLevelTree(tree), s"Illegal top-level tree in TypeOf: $tree") + + override def equals(that: Any): Boolean = { + that match { + case that: TypeOf => + def compareTree(tree1: Tree, tree2: Tree): Boolean = { + def compareArgs[T <: Tree](args1: List[T], args2: List[T]): Boolean = + args1.zip(args2).forall { case (a,b) => a.tpe == b.tpe } + (tree1, tree2) match { + case (t1: Apply, t2: Apply) => + t1.fun.tpe == t2.fun.tpe && compareArgs(t1.args, t2.args) + case (t1: TypeApply, t2: TypeApply) => + t1.fun.tpe == t2.fun.tpe && compareArgs(t1.args, t2.args) + case (t1: If, t2: If) => + t1.cond.tpe == t2.cond.tpe && t1.thenp.tpe == t2.thenp.tpe && t1.elsep.tpe == t2.elsep.tpe + case (t1: Match, t2: Match) => + t1.selector.tpe == t2.selector.tpe && compareArgs(t1.cases, t2.cases) + case (t1, t2) => + false + } + } + compareTree(this.tree, that.tree) + case _ => false + } + } + + override def derivedAnnotatedType(parent: Type, annot: Annotation)(implicit ctx: Context): AnnotatedType = + if ((parent eq this.parent) && (annot eq this.annot)) this + else TypeOf(parent, annot.arguments.head) + + override def toString(): String = s"TypeOf($underlyingTp, $tree)" + } + + object TypeOf { + def apply(underlyingTp: Type, tree: untpd.Tree)(implicit ctx: Context): TypeOf = { + val tree1 = tree.clone.asInstanceOf[Tree] + // This is a safety net to keep us from touching a TypeOf's tree's type. + // Assuming we never look at this type, it would be safe to simply reuse + // tree without cloning. The invariant is currently enforced in Ycheck. + // To disable this safety net we will also have to update the pickler + // to ignore the type of the TypeOf tree's. + tree1.overwriteType(NoType) + new TypeOf(underlyingTp, tree1, Annotation(defn.TypeOfAnnot, tree1)) + } + def unapply(to: TypeOf): Option[(Type, Tree)] = Some((to.underlyingTp, to.tree)) + + def isLegalTopLevelTree(tree: Tree): Boolean = tree match { + case _: TypeApply | _: Apply | _: If | _: Match => true + case _ => false + } + + object If { + def unapply(to: TypeOf): Option[(Type, Type, Type)] = to.tree match { + case Trees.If(cond, thenb, elseb) => Some((cond.tpe, thenb.tpe, elseb.tpe)) + case _ => None + } + } + + object Match { + def unapply(to: TypeOf): Option[(Type, List[Type])] = to.tree match { + case Trees.Match(cond, cases) => + // TODO: We only look at .body.tpe for now, eventually we should + // also take the guard and the pattern into account. + Some((cond.tpe, cases.map(_.body.tpe))) + case _ => None + } + } + } + // ----- TypeMaps -------------------------------------------------------------------- /** Common base class of TypeMap and TypeAccumulator */ @@ -4069,6 +4163,30 @@ object Types { case tp: SkolemType => tp + case tp: TypeOf => + def copyMapped[ThisTree <: Tree](tree: ThisTree): ThisTree = { + val tp1 = this(tree.tpe) + if (tree.tpe eq tp1) tree else tree.withTypeUnchecked(tp1).asInstanceOf[ThisTree] + } + val tree1 = tp.tree match { + case tree: TypeApply => + cpy.TypeApply(tree)(copyMapped(tree.fun), tree.args.mapConserve(copyMapped)) + case tree: Apply => + cpy.Apply(tree)(copyMapped(tree.fun), tree.args.mapConserve(copyMapped)) + case tree: If => + cpy.If(tree)(copyMapped(tree.cond), copyMapped(tree.thenp), copyMapped(tree.elsep)) + case tree: Match => + cpy.Match(tree)(copyMapped(tree.selector), tree.cases.mapConserve(copyMapped)) + case tree => + throw new AssertionError(s"TypeOf shouldn't contain $tree as top-level node.") + } + if (tp.tree ne tree1) { + assert(!tp.underlyingTp.exists || tree1.tpe.exists, i"Derived TypeOf's type became NoType") + tree1.tpe + } else { + tp + } + case tp @ AnnotatedType(underlying, annot) => val underlying1 = this(underlying) if (underlying1 eq underlying) tp @@ -4333,6 +4451,7 @@ object Types { if (underlying.isBottomType) underlying else tp.derivedAnnotatedType(underlying, annot) } + override protected def derivedWildcardType(tp: WildcardType, bounds: Type) = { tp.derivedWildcardType(rangeToBounds(bounds)) } @@ -4440,6 +4559,25 @@ object Types { case tp: OrType => this(this(x, tp.tp1), tp.tp2) + case tp: TypeOf => + @tailrec def foldTrees(x: T, ts: List[Tree]): T = ts match { + case t :: ts1 => foldTrees(apply(x, t.tpe), ts1) + case nil => x + } + + tp.tree match { + case tree: TypeApply => + foldTrees(this(x, tree.fun.tpe), tree.args) + case tree: Apply => + foldTrees(this(x, tree.fun.tpe), tree.args) + case tree: If => + this(this(this(x, tree.cond.tpe), tree.thenp.tpe), tree.elsep.tpe) + case tree: Match => + foldTrees(this(x, tree.selector.tpe), tree.cases) + case tree => + throw new AssertionError(s"TypeOf shouldn't contain $tree as top-level node.") + } + case AnnotatedType(underlying, annot) => this(applyToAnnot(x, annot), underlying) diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala index 1d659828abfe..3819fbaffb71 100644 --- a/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala +++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala @@ -402,6 +402,7 @@ object TastyFormat { final val ANNOTATION = 172 final val TERMREFin = 173 final val TYPEREFin = 174 + final val TYPEOF = 175 // In binary: 101100EI // I = implicit method type @@ -430,7 +431,7 @@ object TastyFormat { firstNatTreeTag <= tag && tag <= SYMBOLconst || firstASTTreeTag <= tag && tag <= SINGLETONtpt || firstNatASTTreeTag <= tag && tag <= NAMEDARG || - firstLengthTreeTag <= tag && tag <= TYPEREFin || + firstLengthTreeTag <= tag && tag <= ERASEDIMPLICITMETHODtype || tag == HOLE def isParamTag(tag: Int) = tag == PARAM || tag == TYPEPARAM @@ -595,6 +596,7 @@ object TastyFormat { case SUPERtype => "SUPERtype" case TERMREFin => "TERMREFin" case TYPEREFin => "TYPEREFin" + case TYPEOF => "TYPEOF" case REFINEDtype => "REFINEDtype" case REFINEDtpt => "REFINEDtpt" diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala index c4ee8cffcf05..fea38b33aa62 100644 --- a/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala +++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyPrinter.scala @@ -74,6 +74,8 @@ class TastyPrinter(bytes: Array[Byte])(implicit ctx: Context) { until(end) { printName(); printTree() } case PARAMtype => printNat(); printNat() + case TYPEOF => + printTree(); printTree() case _ => printTrees() } diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala index c2b22ade4ed6..95ca507cab49 100644 --- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala +++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala @@ -159,6 +159,9 @@ class TreePickler(pickler: TastyPickler) { withLength { pickleType(tycon); args.foreach(pickleType(_)) } case ConstantType(value) => pickleConstant(value) + case tpe: TypeOf => + writeByte(TYPEOF) + withLength { pickleType(tpe.underlyingTp, richTypes); pickleTree(tpe.tree) } case tpe: NamedType => val sym = tpe.symbol def pickleExternalRef(sym: Symbol) = { diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala index ce955cee96c3..f0e74ffedca4 100644 --- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala +++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala @@ -324,6 +324,8 @@ class TreeUnpickler(reader: TastyReader, TypeBounds(readType(), readType()) case ANNOTATEDtype => AnnotatedType(readType(), Annotation(readTerm())) + case TYPEOF => + TypeOf(readType(), readTerm()) case ANDtype => AndType(readType(), readType()) case ORtype => diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index 9ffa8cf9c52e..193c9625f6e6 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -870,7 +870,7 @@ object Parsers { makeTupleOrParens(inParens(argTypes(namedOK = false, wildOK = true))) } else if (in.token == LBRACE) - atPos(in.offset) { RefinedTypeTree(EmptyTree, refinement()) } + atPos(in.offset) { inBraces(refinementOnEmptyOrSingleton()) } else if (isSimpleLiteral) { SingletonTypeTree(literal()) } else if (in.token == USCORE) { val start = in.skipToken() @@ -884,6 +884,12 @@ object Parsers { } } + /** A refinement on an empty tree or a singleton type tree. */ + def refinementOnEmptyOrSingleton(): Tree = { + if (!isStatSeqEnd && !isDclIntro) SingletonTypeTree(expr1()) + else RefinedTypeTree(EmptyTree, refineStatSeq()) + } + val handleSingletonType: Tree => Tree = t => if (in.token == TYPE) { in.nextToken() diff --git a/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala b/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala index fe03355800e5..927be407ad92 100644 --- a/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/DecompilerPrinter.scala @@ -76,6 +76,6 @@ class DecompilerPrinter(_ctx: Context) extends RefinedPrinter(_ctx) { override protected def typeApplyText[T >: Untyped](tree: TypeApply[T]): Text = { if (tree.symbol eq defn.QuotedExpr_apply) "'" else if (tree.symbol eq defn.QuotedType_apply) "'[" ~ toTextGlobal(tree.args, ", ") ~ "]" - else super.typeApplyText(tree) + else super.typeApplyText(tree.fun, tree.args) } } diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index 79c00e0f9f92..a711823f375b 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -18,6 +18,13 @@ class PlainPrinter(_ctx: Context) extends Printer { protected[this] implicit def ctx: Context = _ctx.addMode(Mode.Printing) private[this] var openRecs: List[RecType] = Nil + protected[this] var isInTypeOf: Boolean = false + + protected final def inTypeOf(op: => Text): Text = { + val saved = isInTypeOf + isInTypeOf = true + try { op } finally { isInTypeOf = saved } + } protected def maxToTextRecursions = 100 @@ -142,7 +149,10 @@ class PlainPrinter(_ctx: Context) extends Printer { case tp: TypeParamRef => ParamRefNameString(tp) ~ lambdaHash(tp.binder) case tp: SingletonType => - toTextLocal(tp.underlying) ~ "(" ~ toTextRef(tp) ~ ")" + if (isInTypeOf) + toTextRef(tp) + else + toTextLocal(tp.underlying) ~ "(" ~ toTextRef(tp) ~ ")" case AppliedType(tycon, args) => (toTextLocal(tycon) ~ "[" ~ Text(args map argText, ", ") ~ "]").close case tp: RefinedType => @@ -183,6 +193,8 @@ class PlainPrinter(_ctx: Context) extends Printer { (Str(" => ") provided !tp.resultType.isInstanceOf[MethodType]) ~ toTextGlobal(tp.resultType) } + case TypeOf(underlyingTp, _) => + "{ ... <: " ~ toText(underlyingTp) ~ " }" case AnnotatedType(tpe, annot) => toTextLocal(tpe) ~ " " ~ toText(annot) case tp: TypeVar => @@ -483,9 +495,12 @@ class PlainPrinter(_ctx: Context) extends Printer { val nodeName = tree.productPrefix val elems = Text(tree.productIterator.map(toTextElem).toList, ", ") - val tpSuffix = - if (ctx.settings.XprintTypes.value && tree.hasType) - " | " ~ toText(tree.typeOpt) + val tpSuffix: Text = + if (ctx.settings.XprintTypes.value && tree.hasType && !isInTypeOf) + tree.typeOpt match { + case tp: TypeOf => " | " + case tp => " | " ~ toText(tree.typeOpt) + } else Text() diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index f1cf87ad9c1f..708474aed25e 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -196,6 +196,21 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { return toTextParents(tp.parents) ~ "{...}" case JavaArrayType(elemtp) => return toText(elemtp) ~ "[]" + case TypeOf(underlyingTp, tree) => + import tpd._ + val underlying: Text = " <: " ~ toText(underlyingTp) provided ctx.settings.XprintTypes.value + def treeText = tree match { + case TypeApply(fun, args) => + typeApplyText(fun.tpe, args.tpes) + case Apply(fun, args) => + applyText(fun.tpe, args.tpes) + case If(cond, thenp, elsep) => + val elze = if (elsep.isEmpty) None else Some(elsep.tpe) + ifText(cond.tpe, thenp.tpe, elze) + case Match(sel, cases) => + matchText(sel, cases, showType = true) + } + return typeText("{ ") ~ inTypeOf { treeText } ~ underlying ~ typeText(" }") case tp: AnnotatedType if homogenizedView => // Positions of annotations in types are not serialized // (they don't need to because we keep the original type tree with @@ -233,7 +248,40 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { ("{" ~ toText(trees, "\n") ~ "}").close protected def typeApplyText[T >: Untyped](tree: TypeApply[T]): Text = - toTextLocal(tree.fun) ~ "[" ~ toTextGlobal(tree.args, ", ") ~ "]" + typeApplyText(tree.fun, tree.args) + + protected def typeApplyText(fun: Showable, args: List[Showable]): Text = + toTextLocal(fun) ~ "[" ~ toTextGlobal(args, ", ") ~ "]" + + protected def applyText(fun: Showable, args: List[Showable]): Text = + toTextLocal(fun) ~ "(" ~ toTextGlobal(args, ", ") ~ ")" + + protected def ifText(cond: Showable, thenp: Showable, elsep: Option[Showable]): Text = + changePrec(GlobalPrec) ( + keywordStr("if ") + ~ cond.toText(this) + ~ (keywordText(" then") provided !cond.isInstanceOf[untpd.Parens]) + ~~ thenp.toText(this) + ~ elsep.map(keywordStr(" else ") ~ _.toText(this)).getOrElse("") + ) + + protected def caseDefText[T >: Untyped](cd: CaseDef[T], showType: Boolean): Text = { + val CaseDef(pat, guard, body) = cd + val bodyText = body match { + case body if showType => toText(List(body.asInstanceOf[tpd.Tree].tpe), "\n") + case Block(stats, expr) => toText(stats :+ expr, "\n") + case expr => toText(expr) + } + keywordStr("case ") ~ inPattern(toText(pat)) ~ optText(guard)(keywordStr(" if ") ~ _) ~ " => " ~ bodyText + } + + protected def matchText[T >: Untyped](sel: Tree[T], cases: List[CaseDef[T]], showType: Boolean): Text = { + val selText = if (showType) toText(sel.asInstanceOf[tpd.Tree].tpe) else toText(sel) + if (sel.isEmpty) blockText(cases) + else changePrec(GlobalPrec) { selText ~ keywordStr(" match ") ~ + ("{" ~ Text(cases.map(c => caseDefText(c, showType)), "\n") ~ "}").close + } + } protected def toTextCore[T >: Untyped](tree: Tree[T]): Text = { import untpd.{modsDeco => _, _} @@ -245,11 +293,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { def optDotPrefix(tree: This) = optText(tree.qual)(_ ~ ".") provided !isLocalThis(tree) - def caseBlockText(tree: Tree): Text = tree match { - case Block(stats, expr) => toText(stats :+ expr, "\n") - case expr => toText(expr) - } - // Dotty deviation: called with an untpd.Tree, so cannot be a untpd.Tree[T] (seems to be a Scala2 problem to allow this) // More deviations marked below as // DD def enumText(tree: untpd.Tree) = tree match { // DD @@ -313,7 +356,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { keywordStr("throw ") ~ toText(args.head) } else - toTextLocal(fun) ~ "(" ~ toTextGlobal(args, ", ") ~ ")" + applyText(fun, args) case tree: TypeApply => typeApplyText(tree) case Literal(c) => @@ -341,17 +384,15 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { case block: Block => blockToText(block) case If(cond, thenp, elsep) => - changePrec(GlobalPrec) { - keywordStr("if ") ~ toText(cond) ~ (keywordText(" then") provided !cond.isInstanceOf[Parens]) ~~ toText(thenp) ~ optText(elsep)(keywordStr(" else ") ~ _) - } + val elze = if (elsep.isEmpty) None else Some(elsep) + ifText(cond, thenp, elze) case Closure(env, ref, target) => "closure(" ~ (toTextGlobal(env, ", ") ~ " | " provided env.nonEmpty) ~ toTextGlobal(ref) ~ (":" ~ toText(target) provided !target.isEmpty) ~ ")" case Match(sel, cases) => - if (sel.isEmpty) blockText(cases) - else changePrec(GlobalPrec) { toText(sel) ~ keywordStr(" match ") ~ blockText(cases) } - case CaseDef(pat, guard, body) => - keywordStr("case ") ~ inPattern(toText(pat)) ~ optText(guard)(keywordStr(" if ") ~ _) ~ " => " ~ caseBlockText(body) + matchText(sel, cases, showType = false) + case cd: CaseDef => + caseDefText(cd, showType = false) case Return(expr, from) => changePrec(GlobalPrec) { keywordStr("return") ~ optText(expr)(" " ~ _) } case Try(expr, cases, finalizer) => @@ -372,7 +413,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { case TypeTree() => typeText(toText(tree.typeOpt)) case SingletonTypeTree(ref) => - toTextLocal(ref) ~ "." ~ keywordStr("type") + typeText("{") ~~ toTextLocal(ref) ~~ typeText("}") case AndTypeTree(l, r) => changePrec(AndPrec) { toText(l) ~ " & " ~ toText(r) } case OrTypeTree(l, r) => @@ -526,7 +567,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { var txt = toTextCore(tree) def suppressTypes = - tree.isType || tree.isDef || // don't print types of types or defs + tree.isType || isInTypeOf || tree.isDef || // don't print types of types or defs homogenizedView && ctx.mode.is(Mode.Pattern) // When comparing pickled info, disregard types of patterns. // The reason is that GADT matching can rewrite types of pattern trees @@ -541,23 +582,24 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { if (ctx.settings.XprintTypes.value && tree.hasType) { // add type to term nodes; replace type nodes with their types unless -Yprint-pos is also set. - def tp = tree.typeOpt match { - case tp: TermRef if tree.isInstanceOf[RefTree] && !tp.denot.isOverloaded => tp.underlying + def tpText: Text = tree.typeOpt match { + case tp: TermRef if tree.isInstanceOf[RefTree] && !tp.denot.isOverloaded => toText(tp.underlying) case tp: ConstantType if homogenizedView => // constant folded types are forgotten in Tasty, are reconstituted subsequently in FirstTransform. // Therefore we have to gloss over this when comparing before/after pickling by widening to // underlying type `T`, or, if expression is a unary primitive operation, to `=> T`. - tree match { + toText(tree match { case Select(qual, _) if qual.typeOpt.widen.typeSymbol.isPrimitiveValueClass => ExprType(tp.widen) case _ => tp.widen - } - case tp => tp + }) + case tp: TypeOf => "" + case tp => toText(tp) } if (!suppressTypes) - txt = ("<" ~ txt ~ ":" ~ toText(tp) ~ ">").close + txt = ("<" ~ txt ~ ":" ~ tpText ~ ">").close else if (tree.isType && !homogenizedView) - txt = toText(tp) + txt = tpText } if (!suppressPositions) { if (printPos) { @@ -726,8 +768,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { def optText[T >: Untyped](tree: Tree[T])(encl: Text => Text): Text = if (tree.isEmpty) "" else encl(toText(tree)) - def optText[T >: Untyped](tree: List[Tree[T]])(encl: Text => Text): Text = - if (tree.exists(!_.isEmpty)) encl(blockText(tree)) else "" + def optText[T >: Untyped](trees: List[Tree[T]])(encl: Text => Text): Text = + if (trees.exists(!_.isEmpty)) encl(blockText(trees)) else "" override protected def ParamRefNameString(name: Name): String = name.invariantName.toString diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala index 918d85afeca6..03856f5ec6d5 100644 --- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala +++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala @@ -273,7 +273,7 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase case tree: TypeTree => tree.withType( tree.tpe match { - case AnnotatedType(tpe, annot) => AnnotatedType(tpe, transformAnnot(annot)) + case tpe: AnnotatedType => tpe.derivedAnnotatedType(tpe.parent, transformAnnot(tpe.annot)) case tpe => tpe } ) diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala index e1c36b9395c3..c2874d8a36b4 100644 --- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala +++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala @@ -486,7 +486,7 @@ object TreeChecker { /** - Check that TypeParamRefs and MethodParams refer to an enclosing type. * - Check that all type variables are instantiated. */ - def checkNoOrphans(tp0: Type, tree: untpd.Tree = untpd.EmptyTree)(implicit ctx: Context) = new TypeMap() { + def checkNoOrphans(tp0: Type)(implicit ctx: Context) = new TypeMap() { val definedBinders = new java.util.IdentityHashMap[Type, Any] def apply(tp: Type): Type = { tp match { @@ -495,10 +495,14 @@ object TreeChecker { mapOver(tp) definedBinders.remove(tp) case tp: ParamRef => - assert(definedBinders.get(tp.binder) != null, s"orphan param: ${tp.show}, hash of binder = ${System.identityHashCode(tp.binder)}, tree = ${tree.show}, type = $tp0") + assert(definedBinders.get(tp.binder) != null, s"orphan param: ${tp.show}, hash of binder = ${System.identityHashCode(tp.binder)}, type = $tp0") case tp: TypeVar => - assert(tp.isInstantiated, s"Uninstantiated type variable: ${tp.show}, tree = ${tree.show}") + assert(tp.isInstantiated, s"Uninstantiated type variable: ${tp.show}") apply(tp.underlying) + case tp: TypeOf => + assert(tp.tree.tpe eq NoType, s"See note in TypeOf.apply") + apply(tp.underlyingTp) + mapOver(tp) case _ => mapOver(tp) } diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala index afc4e83439e1..0c6454bf7f6f 100644 --- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala +++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala @@ -364,10 +364,13 @@ trait TypeAssigner { def assignType(tree: untpd.Apply, fn: Tree, args: List[Tree])(implicit ctx: Context) = { val ownType = fn.tpe.widen match { case fntpe: MethodType => - if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping) - if (fntpe.isResultDependent) safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes) - else fntpe.resultType - else + if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping) { + val tpe = + if (fntpe.isResultDependent) safeSubstParams(fntpe.resultType, fntpe.paramRefs, args.tpes) + else fntpe.resultType + if (fn.symbol.isTransparentMethod) TypeOf(tpe, tree) + else tpe + } else errorType(i"wrong number of arguments at ${ctx.phase.prev} for $fntpe: ${fn.tpe}, expected: ${fntpe.paramInfos.length}, found: ${args.length}", tree.pos) case t => errorType(err.takesNoParamsStr(fn, ""), tree.pos) @@ -424,7 +427,11 @@ trait TypeAssigner { } else { val argTypes = args.tpes - if (sameLength(argTypes, paramNames)) pt.instantiate(argTypes) + if (sameLength(argTypes, paramNames)) { + val tpe = pt.instantiate(argTypes) + if (fn.symbol.isTransparentMethod) TypeOf(tpe, tree) + else tpe + } else wrongNumberOfTypeArgs(fn.tpe, pt.typeParams, args, tree.pos) } case err: ErrorType => @@ -452,8 +459,13 @@ trait TypeAssigner { def assignType(tree: untpd.Inlined, bindings: List[Tree], expansion: Tree)(implicit ctx: Context) = tree.withType(avoidingType(expansion, bindings)) - def assignType(tree: untpd.If, thenp: Tree, elsep: Tree)(implicit ctx: Context) = - tree.withType(thenp.tpe | elsep.tpe) + def assignType(tree: untpd.If, thenp: Tree, elsep: Tree)(implicit ctx: Context) = { + val underlying = thenp.tpe | elsep.tpe + if (ctx.owner.isTransitivelyTransparent) + tree.withType(TypeOf(underlying, tree)) + else + tree.withType(underlying) + } def assignType(tree: untpd.Closure, meth: Tree, target: Tree)(implicit ctx: Context) = tree.withType( @@ -463,8 +475,13 @@ trait TypeAssigner { def assignType(tree: untpd.CaseDef, body: Tree)(implicit ctx: Context) = tree.withType(body.tpe) - def assignType(tree: untpd.Match, cases: List[CaseDef])(implicit ctx: Context) = - tree.withType(ctx.typeComparer.lub(cases.tpes)) + def assignType(tree: untpd.Match, cases: List[CaseDef])(implicit ctx: Context) = { + val underlying = ctx.typeComparer.lub(cases.tpes) + if (ctx.owner.isTransitivelyTransparent) + tree.withType(TypeOf(underlying, tree)) + else + tree.withType(underlying) + } def assignType(tree: untpd.Return)(implicit ctx: Context) = tree.withType(defn.NothingType) @@ -481,8 +498,20 @@ trait TypeAssigner { tree.withType(ownType) } - def assignType(tree: untpd.SingletonTypeTree, ref: Tree)(implicit ctx: Context) = - tree.withType(ref.tpe) + def assignType(tree: untpd.SingletonTypeTree, ref: Tree)(implicit ctx: Context) = { + val tp = ref match { + case _: Literal | _: Ident | _: Select | _: Block | _: This | _: Super => ref.tpe + case _ => + if (TypeOf.isLegalTopLevelTree(ref)) + if (ref.tpe.isInstanceOf[TypeOf]) + ref.tpe + else + errorType(i"Non-sensical singleton-type expression: $ref", ref.pos) + else + throw new AssertionError(i"Tree $ref is not a valid reference for a singleton type tree.") + } + tree.withType(tp) + } def assignType(tree: untpd.AndTypeTree, left: Tree, right: Tree)(implicit ctx: Context) = tree.withType(AndType(left.tpe, right.tpe)) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index fa48b6315a63..d1c1971a557a 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -707,10 +707,16 @@ class Typer extends Namer } def typedIf(tree: untpd.If, pt: Type)(implicit ctx: Context): Tree = track("typedIf") { - val cond1 = typed(tree.cond, defn.BooleanType) + val (condProto, thenProto, elseProto) = + pt match { + case TypeOf.If(c, t ,e) => (c, t, e) + case _ => (defn.BooleanType, pt.notApplied, pt.notApplied) + } + + val cond1 = typed(tree.cond, condProto) val thenp2 :: elsep2 :: Nil = harmonic(harmonize) { - val thenp1 = typed(tree.thenp, pt.notApplied) - val elsep1 = typed(tree.elsep orElse (untpd.unitLiteral withPos tree.pos), pt.notApplied) + val thenp1 = typed(tree.thenp, thenProto) + val elsep1 = typed(tree.elsep orElse (untpd.unitLiteral withPos tree.pos), elseProto) thenp1 :: elsep1 :: Nil } assignType(cpy.If(tree)(cond1, thenp2, elsep2), thenp2, elsep2) @@ -972,6 +978,11 @@ class Typer extends Namer val unchecked = pt.isRef(defn.PartialFunctionClass) typed(desugar.makeCaseLambda(tree.cases, protoFormals.length, unchecked) withPos tree.pos, pt) case _ => + val selectProto = pt match { + case TypeOf.Match(s, _) => s + case _ => WildcardType + } + val sel1 = typedExpr(tree.selector) val selType = fullyDefinedType(sel1.tpe, "pattern selector", tree.pos).widen @@ -981,7 +992,7 @@ class Typer extends Namer } } - def typedCases(cases: List[untpd.CaseDef], selType: Type, pt: Type)(implicit ctx: Context) = { + def typedCases(cases: List[untpd.CaseDef], selType: Type, pt: Type)(implicit ctx: Context): List[CaseDef] = { /** gadtSyms = "all type parameters of enclosing methods that appear * non-variantly in the selector type" todo: should typevars @@ -1003,7 +1014,12 @@ class Typer extends Namer accu(Set.empty, selType) } - cases mapconserve (typedCase(_, pt, selType, gadtSyms)) + pt match { + case TypeOf.Match(_, cs) if cs.length == cases.length => + cases.zip(cs).mapconserve { case (c, p) => typedCase(c, p, selType, gadtSyms) } + case _ => + cases.mapconserve(typedCase(_, pt, selType, gadtSyms)) + } } /** Type a case. */ @@ -1170,8 +1186,9 @@ class Typer extends Namer } def typedSingletonTypeTree(tree: untpd.SingletonTypeTree)(implicit ctx: Context): SingletonTypeTree = track("typedSingletonTypeTree") { - val ref1 = typedExpr(tree.ref) - checkStable(ref1.tpe, tree.pos) + val ref1 = typedExpr(tree.ref)(ctx.fresh.setTree(tree)) + // TODO: Discuss stability requirements of singleton type trees and potentially reenable check + // checkStable(ref1.tpe, tree.pos) assignType(cpy.SingletonTypeTree(tree)(ref1), ref1) } diff --git a/compiler/src/dotty/tools/repl/ReplDriver.scala b/compiler/src/dotty/tools/repl/ReplDriver.scala index f279d44b7f8a..d7d58f965349 100644 --- a/compiler/src/dotty/tools/repl/ReplDriver.scala +++ b/compiler/src/dotty/tools/repl/ReplDriver.scala @@ -14,7 +14,7 @@ import dotc.core.Contexts.Context import dotc.{ CompilationUnit, Run } import dotc.core.Mode import dotc.core.Flags._ -import dotc.core.Types._ +import dotc.core.Types.{TypeOf => _, _} import dotc.core.StdNames._ import dotc.core.Names.Name import dotc.core.NameOps._ diff --git a/docs/docs/internals/syntax.md b/docs/docs/internals/syntax.md index f275cbcd497d..498c0ebe3d0d 100644 --- a/docs/docs/internals/syntax.md +++ b/docs/docs/internals/syntax.md @@ -137,6 +137,7 @@ SimpleType ::= SimpleType TypeArgs | ‘(’ ArgTypes ‘)’ Tuple(ts) | ‘_’ TypeBounds | Refinement RefinedTypeTree(EmptyTree, refinement) + | TypeOf TypeOfTypeTree(expr) | SimpleLiteral SingletonTypeTree(l) ArgTypes ::= Type {‘,’ Type} | NamedTypeArg {‘,’ NamedTypeArg} @@ -148,6 +149,7 @@ TypeArgs ::= ‘[’ ArgTypes ‘]’ NamedTypeArg ::= id ‘=’ Type NamedArg(id, t) NamedTypeArgs ::= ‘[’ NamedTypeArg {‘,’ NamedTypeArg} ‘]’ nts Refinement ::= ‘{’ [RefineDcl] {semi [RefineDcl]} ‘}’ ds +TypeOf ::= ‘{’ Expr1 ‘}’ expr TypeBounds ::= [‘>:’ Type] [‘<:’ Type] | INT TypeBoundsTree(lo, hi) TypeParamBounds ::= TypeBounds {‘<%’ Type} {‘:’ Type} ContextBounds(typeBounds, tps) ``` diff --git a/library/src/scala/annotation/internal/TypeOf.scala b/library/src/scala/annotation/internal/TypeOf.scala new file mode 100644 index 000000000000..c9307c26ffae --- /dev/null +++ b/library/src/scala/annotation/internal/TypeOf.scala @@ -0,0 +1,9 @@ +package scala.annotation.internal + +import scala.annotation.RefiningAnnotation + +/** An annotation used with AnnotatedTypes to capture a term-level expression's + * type precisely. + * @param tree A typed Tree. + */ +final class TypeOf(tree: Any) extends RefiningAnnotation diff --git a/tests/neg/transparent.scala b/tests/neg/transparent.scala new file mode 100644 index 000000000000..f04a251061ae --- /dev/null +++ b/tests/neg/transparent.scala @@ -0,0 +1,43 @@ +object Invalid { + transparent def f(x: Int) = x + 1 + f(1): String // error + f(1): {0} // error + + val y: Int = ??? + type YPlusOne = {y + 1} // error: Non-sensical singleton-type expression: ... +} + +object PrivateLeaks { + transparent def foo(x: Any): { x } = x + class A { + private transparent def bar(i: Int): Int = i + 1 + val a: { foo(bar(1)) } = foo(bar(1)) // error: non-private value a refers to private method bar + // in its type signature { PrivateLeaks.foo({ A.this.bar(1) }) } + } +} + +// object SimpleEqs { +// val x = 1 +// val y: {x} = x +// implicitly[{x + 1} =:= {y}] // errror +// implicitly[{x + 1} =:= {y + 2}] // errror +// implicitly[{x + 1} =:= {1 + y}] // errror: TypeComparer doesn't know about commutativity + +// val b = true +// implicitly[{b} =:= {b}] +// implicitly[{!b} =:= {!b}] +// implicitly[{!b} =:= {b}] // errror +// } + + +// object Stability { +// def f1(x: Int): Int = x +// def f2(x: Int): {x} = x + +// val x = 1 +// implicitly[{f1(x)} =:= {x}] // errror: f1 is not considered stable // errror: f1's result type is not precise enough +// implicitly[{f1(x)} =:= {f1(x)}] // errror: f1 is not considered stable // errror: f1 is not considered stable +// implicitly[{f2(x)} =:= {x}] +// implicitly[{f2(x)} =:= {f2(x)}] +// implicitly[{f1(x)} =:= {f2(x)}] // errror: f1 is not considered stable // errror: f1's result type is not precise enough +// } diff --git a/tests/pos/transparent.scala b/tests/pos/transparent.scala new file mode 100644 index 000000000000..0a36bfebc63b --- /dev/null +++ b/tests/pos/transparent.scala @@ -0,0 +1,153 @@ +object SimpleEqs { + val x = 1 + val y: {x} = x + // val z: {y + 1} = y + 1 +} + +object Call { + transparent def foo(x: Int) = 123 + foo(1): { foo(1) } + foo(1): Int +} + +object ITE { + transparent def foo1(b: Boolean) = { + val res = if (b) + 1 + else + 2 + identity[{ if (b) 1 else 2 }](res) + res + } + + transparent def foo2(b: Boolean): { if (b) 1 else 2 } = + if (b) 1 else 2 + + // Postponed until we can beta reduce + // foo(true): { if(true) 1 else 2 } + // foo(false): { if(false) 1 else 2 } + // var b: Boolean = true + // foo(b): { if(b) 1 else 2 } +} + +object Match { + transparent def foo1(b: Boolean) = { + val res = b match { + case true => 1 + case false => 2 + } + identity[{ b match { case true => 1; case false => 2 } }](res) + res + } + + transparent def foo(b: Boolean): { b match { case true => 1; case false => 2 } } = + b match { case true => 1; case false => 2 } +} + +object Applied { + transparent def foo1(b: Boolean) = ??? + transparent def foo2(b: Boolean): { foo1(b) } = foo1(b) + val a: { foo2(true) } = foo2(true) +} + +object Approx1 { + transparent def foo(x: Any): { x } = x + class A { + transparent def bar(i: Int): Int = i + 1 + val v: { bar(foo(1)) } = bar(foo(1)) + } + + val a = new A {} + val b: { a.bar(foo(1)) } = a.v + + var c = new A {} + val d: { c.bar(foo(1)) } = c.v +} + +object Approx2 { + transparent def foo(x: Any): { x } = x + class A { + transparent def bar(i: Int): Int = i + 1 + val v: { foo(bar(1)) } = foo(bar(1)) + } + + val a = new A {} + val b: { foo(a.bar(1)) }= a.v + + val c = new A {} + val d: { foo(c.bar(1)) }= c.v +} + +// object AvoidLocalRefs { +// type Id[T] = T + +// val x = 1 +// def y = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t } +// def z: {x + 1} = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t } + +// { val a = 0; a + 1 } +// { val a = 0; 1 + a } +// } + + +// object Bounds { +// @annotation.implicitNotFound(msg = "Cannot prove that ${B} holds.") +// sealed abstract class P[B <: Boolean](val b: B) +// private[this] val prop_singleton = new P[true](true) {} +// object P { +// def assume(b: Boolean): P[b.type] = prop_singleton.asInstanceOf[P[b.type]] +// } + +// def if_(cond: Boolean): (implicit (ev: P[cond.type]) => Unit) => Unit = +// thn => if (cond) thn(P.assume(cond)) + + +// // Bounds-checked + +// def index(k: Int)(implicit ev: P[{k >= 0}]): Int = k + +// def run(i: Int) = +// if_(i >= 0) { +// index(i) +// } + + +// // Boxed value with a predicate + +// class PredBox[T, B <: Boolean](val v: T)(val p: P[B]) +// object PredBox { +// def apply[T, B <: Boolean](v: T)(implicit ev: P[B]) = new PredBox[T, B](v)(ev) +// } + +// def run2(i: Int) = +// if_(i != 0) { +// PredBox[Int, {i != 0}](i) +// } +// } + + +// object ArithmeticIdentities { +// type SInt = Int & Singleton + +// class DecomposeHelper[V <: SInt](val v: V) { +// import DecomposeHelper._ +// def asSumOf[X <: SInt, Y <: SInt](x: X, y: Y)(implicit ev: {v} =:= {x + y}): SumOf[{x}, {y}] = SumOf(x, y)(ev(v)) +// } + +// object DecomposeHelper { +// /* Axioms */ +// sealed trait Decomposition[V <: SInt] +// case class SumOf[X <: SInt, Y <: SInt](x: X, y: Y)(val v: {x + y}) extends Decomposition[{v}] { +// def commuted: SumOf[Y, X] = SumOf(y, x)(v.asInstanceOf[{y + x}]) +// } +// } + +// implicit def toDecomposeHelper[V <: Int](v: V): DecomposeHelper[v.type] = new DecomposeHelper(v) + + +// // Let's "show" that x + 1 == 1 + x + +// val x = 123 +// (x + 1).asSumOf(x, 1).v: {x + 1} +// (x + 1).asSumOf(x, 1).commuted.v: {1 + x} +// }