eta-functions-expl typechecks when using Church equality

Author: diode-lang

app/Agda/Core/ToCore.hs

@@ -48,6 +48,7 @@ import Agda.Compiler.Backend (Definition(defType))
 import Control.Exception (throw)
 
 import Debug.Trace
+import Agda.TypeChecking.Pretty (PrettyTCM(prettyTCM))
 
 
 -- TODO(flupe): move this to Agda.Core.Syntax
@@ -137,9 +138,7 @@ instance ToCore I.Term where
   toCore (I.Lit l) = throwError "literals not supported"
 
   -- (diode-lang) Seems like a bug: lookUpDefOrData can return data, but a `TDef` is always constructed
-  -- toCore (I.Def qn es) = tApp <$> (TDef <$> lookupDefOrData qn) <*> toCore es
-
-
+  
   toCore (I.Def qn es) = do
     coreEs <- toCore es
     -- Try looking up as definition first
@@ -257,7 +256,7 @@ toCoreDefn (I.FunctionDefn def) _ =
       , vars      <- I.clausePats cl
       , Just body <- I.clauseBody cl
       -- -> Core.FunctionDefn <$> toCore body
-      -> throwError "only definitions via λ are supported"
+      -> trace ("matched on I.FunctionData with vars=" <> (show (I.clausePats cl))) (throwError "only definitions via λ are supported")
 
     -- case with pattern matching variables
     I.FunctionData{..}
@@ -268,7 +267,7 @@ toCoreDefn (I.FunctionDefn def) _ =
       | isJust (maybeRight _funProjection >>= I.projProper) -- record projections case
       -> throwError "record projections aren't supported"
     I.FunctionData{}
-      -> throwError "unsupported case (shouldn't happens)"
+      -> throwError "unsupported case (shouldn't happen)"
 
 toCoreDefn (I.DatatypeDefn dt) ty =
   withError (\e -> multiLineText $ "datatype definition failure: \n" <> Pretty.render (nest 1 e)) $ do
@@ -349,6 +348,7 @@ instance ToCore a => ToCore (Arg a) where
 -- TODO(flupe): enforce that there are no weird modalities in the arg (e.g: disallow irrelevance)
 instance ToCore a => ToCore (I.Dom a) where
   type CoreOf (I.Dom a) = CoreOf a
+  toCore :: ToCore a => I.Dom a -> ToCoreM (CoreOf (I.Dom a))
   toCore = toCore . unDom
 
 

app/Main.hs

@@ -188,12 +188,6 @@ agdaCorePreModule _ _ tlm _ =
 type ACSyntax = Either String Core.Definition
 
 
-debugIndex :: Index -> TCM ()
-debugIndex index = do
-  let indexAsNat = indexToNat index
-  reportSDoc "agda-core.debug" 10 $ text ("Index of definition being translated: " <> show indexAsNat)
-  reportSDoc "agda-core.debug" 10 $ text ""
-
 agdaCoreCompile :: ACEnv -> ACMEnv -> IsMain -> Internal.Definition -> TCM ACSyntax
 agdaCoreCompile env _ _ def = do
   let ACEnv{toCoreGlobal = ioTcg, toCoreCounterID = ioIndex, toCoreNames = ioNames, toCorePreSignature = ioPreSig } = env
@@ -211,7 +205,6 @@ agdaCoreCompile env _ _ def = do
     -- if a constructor is encontered, skip it to avoid conflict
   (ntcg, nnames)  <-  case theDef of
     Internal.Datatype{dataCons} -> do
-      reportSDoc "agda-core.check" 10 $ text $ "Adding all constructors of datatype " <> name <> " to tcg environment"
       let ntcg_datas  = Map.insert defName index tcg_datas
           nnames_datas = Map.insert  (indexToNat index) name nameData
           tcg_data_cons = Map.fromList (zip dataCons (map (index,) (iterate Suc Zero)))
@@ -247,7 +240,8 @@ agdaCoreCompile env _ _ def = do
       reportSDoc "agda-core.check" 4 $ text $ "  Type: " <> prettyCore nnames ty'
       reportSDoc "agda-core.check" 4 $ text $ "  Definition: " <> prettyCore nnames defn'
 
-      debugIndex index
+      reportSDoc "agda-core.debug" 10 $ text ("Index of definition being translated: " <> show (indexToNat index))
+      reportSDoc "agda-core.debug" 10 $ text ""
 
       case defn' of
         Core.FunctionDefn _  -> liftIO $ writeIORef ioPreSig $

test/EtaFunctions.agda

@@ -8,8 +8,18 @@ data Nat : Set where
   zero : Nat
   suc : Nat → Nat
 
--- data _≡_ {A : Set} (x : A) : A → Set where
---   refl : x ≡ x
+--data _≡_ {A : Set} (x : A) : A → Set where
+--  refl : x ≡ x
+
+--postulate
+--  _≡_ : {A : Set} (x : A) → A → Set
+--  refl : {A : Set} {x : A} → x ≡ x
+
+Id : (A : Set) (x : A) → A → Set₁
+Id = λ A x y → (P : A → Set) → P x → P y
+
+refl : (A : Set) (x : A) → Id A x x
+refl = λ A x P p → p
 
 id_typ : Set → Set
 id_typ = λ A → A
@@ -35,11 +45,14 @@ f = addTwo
 g : Nat → Nat
 g = λ x → addTwo x
 
+z : (A B : Set) (f : A → B) → A → B
+z = λ (A B : Set) h → λ a → (h a)
+
 -- eta-functions : {A B : Set} (f : A → B) → (f ≡ (λ x → f x))
--- eta-functions = λ f → refl
+-- eta-functions = λ h → refl
 
--- eta-functions_expl : (A B : Set) (f : A → B) → (f ≡ (λ x → f x))
--- eta-functions_expl = λ A B → λ f → refl
+eta-functions_expl : (A B : Set) (f : A → B) → (Id (A → B) f (λ x → f x))
+eta-functions_expl = λ A B → λ f → refl (A → B) f
 
 -- test : (A B : Set) (f : A → B) → Set
 -- test = λ A B → λ f → A