-
Notifications
You must be signed in to change notification settings - Fork 19
Description
Hi @fthomas @soronpo Thanks a lot for the great work, I'm one of the supporting developer of the deep learning library kotlingrad. When we try to integrate singleton-ops for the project on some tensor operations, we encounter some strange compiler behaviours that are hard to isolate or simplify, so we have to post a link to our repository in case others want to reproduce, sorry.
In one of our test cases: https://github.com/tribbloid/shapesafe/blob/59405baedc9048a9cac1fbf2bb7708c917266a6e/core/src/test/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVectorSpec.scala#L167
The compiler / macro misbehave on 2 apparently equivalent code blocks:
val v0 = DoubleVector.random(6)
val v1 = v0.pad(3)
{
val result = v1.reify
val aa = result.arity
{
print_@(WideTyped(result.arity).viz)
// this works
result.arity.internal.dummyImp(3)
result.crossValidate()
result.arity.internal.requireEqual(12)
}
{
print_@(WideTyped(aa).viz)
// this doesn't, how did it happened?
aa.internal.dummyImp(3)
aa.internal.requireEqual(12)
}
}
These are the compilation errors:
[Error] /home/peng/git/shapesafe/core/src/test/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVectorSpec.scala:188: implicit error;
!I proof (Cannot extract value from singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,S,Int(3),Int(0)]
showRaw==> TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.$plus, List()), TypeRef(NoPrefix, TypeName("S"), List()), FoldableConstantType(Constant(3)), FoldableConstantType(Constant(0))))): OpMacro[+, S, Int, Int]
[Error] /home/peng/git/shapesafe/core/src/test/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVectorSpec.scala:189: implicit error;
!I proof (Cannot extract value from singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.Require,singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.==,S,Int(12),Int(0)],String("Cannot prove requirement Require[...]"),singleton.ops.impl.NoSym]
showRaw==> TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.Require, List()), TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.$eq$eq, List()), TypeRef(NoPrefix, TypeName("S"), List()), FoldableConstantType(Constant(12)), FoldableConstantType(Constant(0)))), FoldableConstantType(Constant(Cannot prove requirement Require[...])), TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.NoSym, List())))): OpMacro[Require, OpMacro[==, S, Int, Int], String, NoSym]
two errors found
> Task :core:compileTestScala FAILED
These are the same error if the implicit debugging plugin "splain" (https://github.com/tek/splain) is disabled:
[Error] /home/peng/git/shapesafe/core/src/test/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVectorSpec.scala:188: Cannot extract value from singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.+,S,Int(3),Int(0)]
showRaw==> TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.$plus, List()), TypeRef(NoPrefix, TypeName("S"), List()), FoldableConstantType(Constant(3)), FoldableConstantType(Constant(0))))
[Error] /home/peng/git/shapesafe/core/src/test/scala/edu/umontreal/kotlingrad/shapesafe/core/tensor/DoubleVectorSpec.scala:189: Cannot extract value from singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.Require,singleton.ops.impl.OpMacro[singleton.ops.impl.OpId.==,S,Int(12),Int(0)],String("Cannot prove requirement Require[...]"),singleton.ops.impl.NoSym]
showRaw==> TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.Require, List()), TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.OpMacro, List(TypeRef(SingleType(ThisType(singleton.ops.impl), singleton.ops.impl.OpId), singleton.ops.impl.OpId.$eq$eq, List()), TypeRef(NoPrefix, TypeName("S"), List()), FoldableConstantType(Constant(12)), FoldableConstantType(Constant(0)))), FoldableConstantType(Constant(Cannot prove requirement Require[...])), TypeRef(ThisType(singleton.ops.impl), singleton.ops.impl.NoSym, List())))
two errors found
> Task :core:compileTestScala FAILED
My questions are:
-
What's the cause of this error? It clearly won't be caused by a missing dependent type (variable
aa
has a static path, butresult.arity
doesn't) So how is the macro unable to figure out the type foraa
? -
What should we do for any error that has such message? Should we debug or try to print the stacktrace?