PRIM: fix bug caused by a missing normalization (thank you @refparo)

base/src/main/java/org/aya/core/def/PrimDef.java

@@ -12,6 +12,7 @@
 import org.aya.api.ref.LevelGenVar;
 import org.aya.api.ref.LocalVar;
 import org.aya.api.util.Arg;
+import org.aya.api.util.NormalizeMode;
 import org.aya.concrete.stmt.Decl;
 import org.aya.core.sort.Sort;
 import org.aya.core.term.*;
@@ -77,7 +78,9 @@ private PrimFactory() {
       if (argI instanceof CallTerm.Prim primCall && left.isNotEmpty() && primCall.ref() == left.get().ref)
         return argBase;
       var argA = args.get(0).term();
-      if (argA instanceof IntroTerm.Lambda lambda && lambda.body().findUsages(lambda.param().ref()) == 0)
+      if (argA instanceof IntroTerm.Lambda lambda && lambda.body()
+        .normalize(NormalizeMode.NF)
+        .findUsages(lambda.param().ref()) == 0)
         return argBase;
       return prim;
     }

base/src/test/resources/success/refparo4.aya

@@ -0,0 +1,22 @@
+-- https://github.com/aya-prover/aya-dev/discussions/7
+prim I
+prim left
+prim right
+prim arcoe
+struct Path (A : I -> Type) (a : A left) (b : A right) : Type
+ | at (i : I) : A i {
+   | left => a
+   | right => b
+ }
+def path {A : I -> Type} (p : Pi (i : I) -> A i)
+  => new Path A (p left) (p right) { | at i => p i }
+def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
+def idp {A : Type} (a : A) : a = a => path (\ i => a)
+
+bind application tighter =
+
+open data Unit : Set | unit
+
+def foo
+  : unit = arcoe (idp Unit).at unit right
+  => idp unit