Skip to content
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

nonconformant bound info sometimes print out full type signature instead of the formatted one, is it deliberate? #71

Closed
tribbloid opened this issue Oct 27, 2021 · 11 comments

Comments

@tribbloid
Copy link
Collaborator

Here is an example when I'm debugging shapesafe:

implicit error;
!I prove:
  Proof[
    On[Literal[Int(1)], On[Literal[Int(2)], Literal[Int(4)]]]
    ,
    Aye[O]
  ]
  ¯\_(ツ)_/¯ 1 != 6
  
  ... when proving arity ░▒▓
  
  1 == 6
  
Op2.unchecked invalid because
!I domain: UncheckedDomain[Literal[Int(1)], On[Literal[Int(2)], Literal[Int(4)]]]
――UncheckedDomain.d2 invalid because
  !I bound1: Proof[Literal[Int(1)], Aye[_$1]]
    [NO PROOF]: org.shapesafe.core.arity.ConstArity.Literal[Int(1)]	 |- 	??? <: org.shapesafe.core.arity.Unchecked
    
――UncheckedDomain.d1 invalid because
  !I bound2: Proof[On[Literal[Int(2)], Literal[Int(4)]], Aye[_$1]]
    [NO PROOF]: org.shapesafe.core.arity.binary.Op2.Impl[[P1, P2]singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,P1,P2,Int(0)],org.shapesafe.core.debugging.Expressions.+]#On[org.shapesafe.core.arity.ConstArity.Literal[Int(2)],org.shapesafe.core.arity.ConstArity.Literal[Int(4)]]	 |- 	??? <: org.shapesafe.core.arity.Unchecked
    
――――Op2.unchecked invalid because
    !I domain: UncheckedDomain[Literal[Int(2)], Literal[Int(4)]]
――――――UncheckedDomain.d2 invalid because
      !I bound1: Proof[Literal[Int(2)], Aye[_$1]]
        [NO PROOF]: org.shapesafe.core.arity.ConstArity.Literal[Int(2)]	 |- 	??? <: org.shapesafe.core.arity.Unchecked
        
――――――UncheckedDomain.d1 invalid because
      !I bound2: Proof[Literal[Int(4)], Aye[_$1]]
        [NO PROOF]: org.shapesafe.core.arity.ConstArity.Literal[Int(4)]	 |- 	??? <: org.shapesafe.core.arity.Unchecked
        
binary.this.Op2.invar[org.shapesafe.core.arity.ConstArity.Literal[Int(1)], org.shapesafe.core.arity.binary.Op2.Impl[[P1, P2]singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,P1,P2,Int(0)],org.shapesafe.core.debugging.Expressions.+]#On[org.shapesafe.core.arity.ConstArity.Literal[Int(2)],org.shapesafe.core.arity.ConstArity.Literal[Int(4)]], Int(1), Int(6), org.shapesafe.core.arity.binary.Require2.Impl[[P1, P2]singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.==,P1,P2,Int(0)],org.shapesafe.core.debugging.Expressions.==]](arity.this.VerifiedArity.endo[org.shapesafe.core.arity.ConstArity.Literal[Int(1)]], binary.this.Op2.invar[org.shapesafe.core.arity.ConstArity.Literal[Int(2)], org.shapesafe.core.arity.ConstArity.Literal[Int(4)], Int(2), Int(4), org.shapesafe.core.arity.binary.Op2.Impl[[P1, P2]singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,P1,P2,Int(0)],org.shapesafe.core.debugging.Expressions.+]](arity.this.VerifiedArity.endo[org.shapesafe.core.arity.ConstArity.Literal[Int(2)]], arity.this.VerifiedArity.endo[org.shapesafe.core.arity.ConstArity.Literal[Int(4)]], {
  final class $anon extends AnyRef with singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,Int(2),Int(4),Int(0)] {
    def <init>(): <$anon: singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,Int(2),Int(4),Int(0)]> = {
      $anon.super.<init>();
      ()
    };
    type OutWide = Int;
    type Out = Int(6);
    type OutInt = Int(6);
    final private[this] val value: Int(6) = 6;
    final <stable> <accessor> def value: Int(6) = $anon.this.value;
    final private[this] val isLiteral: Boolean(true) = true;
    final <stable> <accessor> def isLiteral: Boolean(true) = $anon.this.isLiteral;
    final private[this] val valueWide: Int = 6;
    final <stable> <accessor> def valueWide: Int = $anon.this.valueWide
  };
  new $anon()
}), {
  final class $anon extends AnyRef with singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.==,Int(1),Int(6),Int(0)] {
    def <init>(): <$anon: singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.==,Int(1),Int(6),Int(0)]> = {
      $anon.super.<init>();
      ()
    };
    type OutWide = Boolean;
    type Out = Boolean(false);
    type OutBoolean = Boolean(false);
    final private[this] val value: Boolean(false) = false;
    final <stable> <accessor> def value: Boolean(false) = $anon.this.value;
    final private[this] val isLiteral: Boolean(true) = true;
    final <stable> <accessor> def isLiteral: Boolean(true) = $anon.this.isLiteral;
    final private[this] val valueWide: Boolean = false;
    final <stable> <accessor> def valueWide: Boolean = $anon.this.valueWide
  };
  new $anon()
}) invalid because
nonconformant bounds;
[Literal[Int(1)], On[Literal[Int(2)], Literal[Int(4)]], Int(1), Int(6), Impl[OpMacro[==, ?, ?, Int(0)], ==]]
[A1 <: org.shapesafe.core.arity.Arity, A2 <: org.shapesafe.core.arity.Arity, S1, S2, OP <: org.shapesafe.core.arity.binary.Op2]
...
  

If this goes through proper formatting, I shouldn't even see the "singleton.ops.impl." package part. Is there a reason they have to be printed? Or is it some kind of fall back mechanism when formatting fails?

@tek Thanks a lot for your input

@tek
Copy link
Owner

tek commented Oct 28, 2021

this looks like a message from an annotation in that library

@tribbloid
Copy link
Collaborator Author

don't think so, if it is an annotation it should come after the "invalid because" part.

Plus this annotation seems to be all types, no text. I knew PhD students are undisciplined, but not that undisciplined

@tek
Copy link
Owner

tek commented Oct 28, 2021

well then what is that NO PROOF?

@tribbloid
Copy link
Collaborator Author

Oh sorry that was part of the implicit annotation of shapesafe (the library I worked on)

@tribbloid
Copy link
Collaborator Author

hmmm, looks like this problem can be triggered if the implicit function doesn't have a return type. The compiler has some weird rule in inferring and erasing type automatically in this case

@tribbloid
Copy link
Collaborator Author

I found the cause of the problem, the following 2 types of Tree:

  // TODO remove this class, add a tree attachment to Apply to track whether implicits were involved
  // copying trees will all too easily forget to distinguish subclasses
  class ApplyToImplicitArgs(fun: Tree, args: List[Tree]) extends Apply(fun, args)

  // TODO remove this class, add a tree attachment to Apply to track whether implicits were involved
  // copying trees will all too easily forget to distinguish subclasses
  class ApplyImplicitView(fun: Tree, args: List[Tree]) extends Apply(fun, args)

May be returned as implicit candidate. Their .toString format is also very verbose (at least as verbose as TypeApply, which was replaced with an Apply when the error message is generated). So, the solution should be merely adding these 2 cases into the unapplyCandidate

A patch should be released shortly. But our end goal should be to merge it into scalac

@tribbloid
Copy link
Collaborator Author

@tek do you think it is a good idea to invite @lrytz to be on our advisor board?

@tek
Copy link
Owner

tek commented Nov 5, 2021

if that is something he'd like to do, sure!

@tribbloid
Copy link
Collaborator Author

Sounds good, let's finish the 1.0.0-RC1 for 2.13.6 first

@lrytz
Copy link

lrytz commented Nov 8, 2021

Not sure what your board is, but feel free to ping me on questions / issues :)

@tribbloid
Copy link
Collaborator Author

@tek patch is integrated a few days ago, closing

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

No branches or pull requests

3 participants