Working example for function eta-conversion where TLam is on left and TVar is on right

Author: diode-lang

src/Agda/Core/Checkers/Converter.agda

@@ -239,8 +239,7 @@ convertWhnf r functionTerm (TLam x b) =
   do
     conversionProof <- convertCheck newScope b term
     return (CEtaFunctions x functionTerm b conversionProof)
--- convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
--- convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
+convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
 convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"
 
 {-# COMPILE AGDA2HS convertWhnf #-}

test/EtaFunctions.agda

@@ -15,8 +15,8 @@ data Nat : Set where
 comp : (A B C : Set) → (B → C) → (A → B) → A → C
 comp = λ (A B C : Set) → λ f → λ g → λ x → f (g x)
 
-const : Nat → Nat → Nat
-const = λ x → λ y → x
+const : (A : Set) → A → A → A
+const = λ A → λ x → λ y → x
 
 addOne : Nat -> Nat
 addOne = suc
@@ -27,9 +27,9 @@ addTwo = λ x → (suc (suc x))
 addTwoAfterAddOne : Nat → Nat
 addTwoAfterAddOne = λ x → (comp Nat Nat Nat addTwo addOne x)
 
-eta-higher : (A B C : Set) → (f : A → B → C) → (λ x → λ y → f x y) ≡ f
+eta-higher : (A B C : Set) → (f : A → B → C) → (λ x → λ y → f (const A x x) y) ≡ f
 eta-higher = λ A B C → λ f → refl
 
-eta-counterexample-simple : addOne ≡ (λ x → (suc (const x x)))
+eta-counterexample-simple : addOne ≡ (λ x → (suc (const Nat x x)))
 eta-counterexample-simple = refl