fix function η with subsingleton types

golden-tests/tests/eta-singleton/eta-sing.quox

@@ -0,0 +1,33 @@
+-- inspired by https://github.com/agda/agda/issues/2556
+
+postulate0 A : ★
+
+def0 ZZ : ★ = 0 ≡ 0 : ℕ
+
+def reflZ : ZZ = δ _ ⇒ 0
+
+
+namespace erased {
+  def0 ZZA : ★ = 0.ZZ → A
+
+  def propeq : (x : ZZA) → x ≡ (λ _ ⇒ x reflZ) : ZZA =
+    λ x ⇒ δ _ ⇒ x
+
+  def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
+    λ P x p ⇒ p
+}
+
+namespace unrestricted {
+  def0 ZZA : ★ = ω.ZZ → A
+
+  def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
+    λ P x p ⇒ p
+}
+
+namespace linear {
+  def0 ZZA : ★ = 1.ZZ → A
+
+  #[fail]
+  def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
+    λ P x p ⇒ p
+}

golden-tests/tests/eta-singleton/expected

@@ -0,0 +1,9 @@
+0.A : ★
+0.ZZ : ★
+ω.reflZ : ZZ
+0.erased.ZZA : ★
+ω.erased.propeq : 1.(x : erased.ZZA) → x ≡ (λ _ ⇒ x reflZ) : erased.ZZA
+ω.erased.defeq : 0.(P : 1.erased.ZZA → ★) → 0.(x : erased.ZZA) → 1.(P (λ _ ⇒ (x reflZ))) → P x
+0.unrestricted.ZZA : ★
+ω.unrestricted.defeq : 0.(P : 1.unrestricted.ZZA → ★) → 0.(x : unrestricted.ZZA) → 1.(P (λ _ ⇒ (x reflZ))) → P x
+0.linear.ZZA : ★

golden-tests/tests/eta-singleton/run

@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" eta-sing.quox

lib/Quox/Equal.idr

@@ -277,8 +277,16 @@ namespace Term
     toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
 
     eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
-    eta loc e (S _ (N _)) = clashT loc ctx ty s t
-    eta _   e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b
+    eta loc e (S _ (N b)) =
+      if qty /= One then
+        if !(isSubSing defs ctx sg arg) then
+          compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b)
+        else
+          clashT loc ctx ty s t
+      else
+        clashT loc ctx ty s t
+    eta _ e (S _ (Y b)) =
+      compare0 defs ctx' sg res.term (toLamBody e) b
 
   compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = withEqual $
     case (s, t) of