intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

False positive "X is not a reference to either a definition or a variable"

Open marat-rkh opened this issue 3 years ago • 1 comments

Screen Shot 2021-05-15 at 12 46 29 PM

As you can see, =~ is a record, so it is a reference to a definition. Re-opening the project solves the issue. I encounter it from time to time, but not sure how to reproduce.

marat-rkh avatar May 15 '21 09:05 marat-rkh

There is an exception in the log, but it seems to be unrelated:

2021-05-15 12:44:16,718 [149661538]  ERROR - plication.impl.ApplicationImpl - class org.arend.core.definition.ClassDefinition cannot be cast to class org.arend.core.definition.FunctionDefinition (org.arend.core.definition.ClassDefinition and org.arend.core.definition.FunctionDefinition are in unnamed module of loader com.intellij.ide.plugins.cl.PluginClassLoader @56916bba) 
java.lang.ClassCastException: class org.arend.core.definition.ClassDefinition cannot be cast to class org.arend.core.definition.FunctionDefinition (org.arend.core.definition.ClassDefinition and org.arend.core.definition.FunctionDefinition are in unnamed module of loader com.intellij.ide.plugins.cl.PluginClassLoader @56916bba)
	at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:152)
	at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:66)
	at org.arend.term.concrete.Concrete$BaseFunctionDefinition.accept(Concrete.java:2127)
	at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:221)
	at org.arend.typechecking.order.listener.CollectingOrderingListener$MyUnit.feedTo(CollectingOrderingListener.java:49)
	at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1$1.get(BackgroundTypechecker.kt:86)
	at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1$1.get(BackgroundTypechecker.kt:20)
	at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:37)
	at org.arend.typechecking.computation.BooleanComputationRunner.run(BooleanComputationRunner.java:8)
	at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke(BackgroundTypechecker.kt:85)
	at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke(BackgroundTypechecker.kt:20)
	at org.arend.typechecking.DefinitionBlacklistService.runTimed(DefinitionBlacklistService.kt:25)
	at org.arend.typechecking.BackgroundTypechecker.typecheckDefinition(BackgroundTypechecker.kt:84)
	at org.arend.typechecking.BackgroundTypechecker.runTypechecker(BackgroundTypechecker.kt:64)
	at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:201)
	at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:34)
	at org.arend.typechecking.TypecheckingTaskQueue$addTask$2.run(TypecheckingTaskQueue.kt:43)
	at com.intellij.util.RunnableCallable.call(RunnableCallable.java:20)
	at com.intellij.util.RunnableCallable.call(RunnableCallable.java:11)
	at com.intellij.openapi.application.impl.ApplicationImpl$1.call(ApplicationImpl.java:265)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
	at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
	at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
	at java.base/java.security.AccessController.doPrivileged(Native Method)
	at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
	at java.base/java.lang.Thread.run(Thread.java:834)
2021-05-15 12:44:16,719 [149661539]  ERROR - plication.impl.ApplicationImpl - IntelliJ IDEA 2021.1  Build #IC-211.6693.111 
2021-05-15 12:44:16,722 [149661542]  ERROR - plication.impl.ApplicationImpl - JDK: 11.0.10; VM: Dynamic Code Evolution 64-Bit Server VM; Vendor: JetBrains s.r.o. 
2021-05-15 12:44:16,722 [149661542]  ERROR - plication.impl.ApplicationImpl - OS: Mac OS X 
2021-05-15 12:44:16,722 [149661542]  ERROR - plication.impl.ApplicationImpl - Plugin to blame: Arend version: 1.6.0.3 
2021-05-15 12:44:16,723 [149661543]  ERROR - plication.impl.ApplicationImpl - Last Action: EditorChooseLookupItem 

marat-rkh avatar May 15 '21 09:05 marat-rkh