Adds additional eta counterexample, which requires a different match case in Converter.agda

Author: diode-lang

src/Agda/Core/Checkers/Converter.agda

@@ -232,6 +232,7 @@ convertWhnf r (TSort s) (TSort t) = convSorts s t
 --let and ann shouldn't appear here since they get reduced away
 convertWhnf r (TVar _) (TLam _ _) = tcError "implement eta-functions 1"
 convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
+convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
 convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"
 
 {-# COMPILE AGDA2HS convertWhnf #-}

src/Agda/Core/Rules/Conversion.agda

@@ -89,6 +89,8 @@ data Conv {α} where
   CRedR  : @0 ReducesTo v v'
          → u  ≅ v'
          → u  ≅ v
+  -- TODO : eta
+  
 
 data ConvBranch {α = α} {c = c} where
   CBBranch :  (cr1 cr2 : Singleton c) (r1 r2 : Singleton (fieldScope c))

test/EtaFunctionsChurchWithConst.agda

@@ -1,3 +1,8 @@
+data Nat : Set where
+  Zero : Nat
+  Suc : Nat → Nat
+
+
 Id : (A : Set) (x : A) → A → Set₁
 Id = λ A x y → (P : A → Set) → P x → P y
 
@@ -19,3 +24,8 @@ eta-functions_three : (A B : Set) (f : A → B) →
 eta-functions_three = λ A B → λ f → refl (A → B) f
 
 
+-- f 0 =?= \x -> f 0 x
+-- f : Nat -> Nat -> Nat
+
+eta-app-1 : (f : Nat -> Nat -> Nat) -> Id (Nat -> Nat) (f Zero) (\x -> (f Zero (const Nat x x)))
+eta-app-1 = λ f → refl (Nat → Nat) (f Zero)