Possible definition which would require eta-conversion in the type checker

Author: diode-lang

.vscode/tasks.json

@@ -0,0 +1,50 @@
+
+{
+  // Automatically created by phoityne-vscode extension.
+
+  "version": "2.0.0",
+  "presentation": {
+    "reveal": "always",
+    "panel": "new"
+  },
+  "tasks": [
+    {
+      // F7
+      "group": {
+        "kind": "build",
+        "isDefault": true
+      },
+      "label": "haskell build",
+      "type": "shell",
+      //"command": "cabal configure && cabal build"
+      "command": "stack build"
+    },
+    {
+      // F6
+      "group": "build",
+      "type": "shell",
+      "label": "haskell clean & build",
+      //"command": "cabal clean && cabal configure && cabal build"
+      "command": "stack clean && stack build"
+      //"command": "stack clean ; stack build"  // for powershell
+    },
+    {
+      // F8
+      "group": {
+        "kind": "test",
+        "isDefault": true
+      },
+      "type": "shell",
+      "label": "haskell test",
+      //"command": "cabal test"
+      "command": "stack test"
+    },
+    {
+      // F6
+      "isBackground": true,
+      "type": "shell",
+      "label": "haskell watch",
+      "command": "stack build --test --no-run-tests --file-watch"
+    }
+  ]
+}

app/Agda/Core/ToCore.hs

@@ -47,9 +47,24 @@ import System.IO (withBinaryFile)
 import Agda.Compiler.Backend (Definition(defType))
 import Control.Exception (throw)
 
-import Debug.Trace
 import Agda.TypeChecking.Pretty (PrettyTCM(prettyTCM))
 
+import Agda.Syntax.Common.Pretty(text, render)
+
+import Debug.Trace
+
+-- Helper to add color
+traceColor :: String -> String -> a -> a
+traceColor color msg = trace (color ++ msg ++ "\x1b[0m")
+
+traceRed, traceGreen, traceYellow, traceBlue, traceMagenta, traceCyan :: String -> a -> a
+traceRed     = traceColor "\x1b[31m"
+traceGreen   = traceColor "\x1b[32m"
+traceYellow  = traceColor "\x1b[33m"
+traceBlue    = traceColor "\x1b[34m"
+traceMagenta = traceColor "\x1b[35m"
+traceCyan    = traceColor "\x1b[36m"
+
 
 -- TODO(flupe): move this to Agda.Core.Syntax
 -- | Apply a core term to elims
@@ -136,8 +151,6 @@ instance ToCore I.Term where
 
   -- TODO(flupe): add literals once they're added to core
   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) = do
     coreEs <- toCore es
@@ -156,19 +169,20 @@ instance ToCore I.Term where
         return (tApp dataRef coreEs)
       )
 
-  toCore (I.Con ch ci es)
+  toCore (I.Con ch _ es)
     | Just args <- allApplyElims es
     = do
         -- @l@ is the amount of arguments missing from the application.
         -- we need to eta-expand manually @l@ times to fully-apply the constructor.
         let l  = length (I.conFields ch) - length es
-        let vs = reverse $ take l $ TVar <$> iterate Scope.inThere Scope.inHere
+        -- Construct @l@ additional deBruijn indices
+        let additionalVars = reverse $ take l $ TVar <$> iterate Scope.inThere Scope.inHere
         (dt , con) <- lookupCon (I.conName ch)
 
-        t <- TCon dt con . toTermS . (++ vs) <$> toCore (raise l args)
+        t <- TCon dt con . toTermS . (++ additionalVars) <$> toCore (raise l args)
 
-        -- in the end, we bind @l@ fresh variables
-        pure (iterate TLam t !! l)
+        -- in the end, we bind @l@ fresh deBruijn indices
+        traceMagenta "Constructed TLam" pure (iterate TLam t !! l)
 
   toCore I.Con{} = throwError "cubical endpoint application to constructors not supported"
 
@@ -248,15 +262,15 @@ toCoreDefn (I.FunctionDefn def) _ =
       , [cl]      <- _funClauses
       , []        <- I.clausePats cl
       , Just body <- I.clauseBody cl
-      -> Core.FunctionDefn <$> toCore body
+      -> Core.FunctionDefn <$> traceMagenta ("calling toCore with body=" <> (render $ pretty body)) toCore body
     -- case with no pattern matching
     I.FunctionData{..}
       | isNothing (maybeRight _funProjection >>= I.projProper) -- discard record projections
       , [cl]      <- _funClauses
       , vars      <- I.clausePats cl
       , Just body <- I.clauseBody cl
       -- -> Core.FunctionDefn <$> toCore body
-      -> trace ("matched on I.FunctionData with vars=" <> (show (I.clausePats cl))) (throwError "only definitions via λ are supported")
+      -> (throwError "only definitions via λ are supported")
 
     -- case with pattern matching variables
     I.FunctionData{..}
@@ -336,6 +350,7 @@ instance ToCore I.Definition where
 -- Others
 instance (Subst a, ToCore a) => ToCore (I.Abs a) where
   type CoreOf (I.Abs a) = CoreOf a
+  toCore :: (Subst a, ToCore a) => I.Abs a -> ToCoreM (CoreOf (I.Abs a))
   toCore = toCore . absBody
 
 

app/Main.hs

@@ -224,9 +224,10 @@ agdaCoreCompile env _ _ def = do
   liftIO $ writeIORef ioNames nnames
   liftIO $ writeIORef ioIndex (Suc index)
 
+  defTypeDoc <- prettyTCM defType
   reportSDoc "agda-core.check" 4 $ text "  Agda type: " <> prettyTCM defType
   reportSDoc "agda-core.check" 5 $ text "  Agda definition: " <> text (show $ Pretty.pretty theDef)
-
+  -- reportSDoc "agda-core.check" 5 $ text "  Agda definition: " <> text (show theDef)
 
 
   case convert ntcg def of
@@ -237,8 +238,8 @@ agdaCoreCompile env _ _ def = do
       return $ throwError name
     Right def'-> do
       let Core.Definition{defType = ty', theDef = defn'} = def'
-      reportSDoc "agda-core.check" 4 $ text $ "  Type: " <> prettyCore nnames ty'
-      reportSDoc "agda-core.check" 4 $ text $ "  Definition: " <> prettyCore nnames defn'
+      reportSDoc "agda-core.check" 4 $ text $ "  Agda Core Type: " <> prettyCore nnames ty'
+      reportSDoc "agda-core.check" 4 $ text $ "  Agda Core Definition: " <> prettyCore nnames defn'
 
       reportSDoc "agda-core.debug" 10 $ text ("Index of definition being translated: " <> show (indexToNat index))
       reportSDoc "agda-core.debug" 10 $ text ""
@@ -309,8 +310,6 @@ agdaCorePostModule ACEnv{toCorePreSignature = ioPreSig} nameMap _ tlm defs = do
       Left n -> reportSDocFailure "agda-core.check" $ text $ "Skiped " <> n <> " :  term not compiled"
       Right Core.Definition{ defName, theDef = Core.FunctionDefn funBody, defType } -> do
         reportSDoc "agda-core.check" 2 $ text $ "Typechecking of " <> defName <> " :"
-        reportSDoc "agda-core.check" 10 $ text $ defName <> " has funBody: " <> show funBody
-        reportSDoc "agda-core.check" 10 $ text $ defName <> " has defType: " <> show defType <> "\n"
         preSig <- liftIO $ readIORef ioPreSig
         let sig = preSignatureToSignature preSig
         let fl  = Core.More fl

test/EtaFunctions.agda

@@ -15,22 +15,22 @@ 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
+
 addOne : Nat -> Nat
-addOne = λ x → suc x
+addOne = suc
 
 addTwo : Nat → Nat
 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 → λ f → refl
 
--- In this case, the type which Agda infers is addTwoAfterAddOne ≡ comp Nat Nat Nat addTwo addOne
--- So the agda-core typechecker would expand `addTwoAfterAddOne`, which expands to λ x → (comp Nat Nat Nat addTwo addOne x)
--- and the remaining equation would need to be solved by either eta-reduction or eta-expansion
-eta-counterexample : addTwoAfterAddOne ≡ (λ x → (comp Nat Nat Nat addTwo addOne) x)
-eta-counterexample = refl
+
+eta-counterexample-simple : addOne ≡ (λ x → (suc (const x x)))
+eta-counterexample-simple = refl
+

test/EtaFunctionsChurch.agda

@@ -1,55 +1,60 @@
 module EtaFunctionsChurch where 
 
-data Bool : Set where
-  true : Bool
-  false : Bool
+-- data Bool : Set where
+--   true : Bool
+--   false : Bool
 
 data Nat : Set where
   zero : Nat
   suc : Nat → Nat
 
-
+-- an x of type A is equal to another element of type A,
+-- if, for all predicates `P : A → Set`, if `P x` holds then `P y` also holds
+-- The result of an `Id A x x` is a `Set₁`, because we are quantifying over all `Set`'s
 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
 
-idbool : Bool → Bool
-idbool = λ b → b
+-- idbool : Bool → Bool
+-- idbool = λ b → b
 
--- Composition operator ∘
-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
 
-addOne : Nat -> Nat
-addOne = λ x → suc x
+addOne : Nat → Nat
+addOne = suc
 
-addTwo : Nat → Nat
-addTwo = λ x → (suc (suc x))
+-- Composition operator ∘
+-- comp : (A B C : Set) → (B → C) → (A → B) → A → C
+-- comp = λ (A B C : Set) → λ f → λ g → λ x → f (g x)
 
-addTwoAfterAddOne : Nat → Nat
-addTwoAfterAddOne = λ x → (comp Nat Nat Nat addTwo addOne x)
+-- addTwo : Nat → Nat
+-- addTwo = λ x → (suc (suc x))
 
-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
+-- addTwoAfterAddOne : Nat → Nat
+-- addTwoAfterAddOne = λ x → (comp Nat Nat Nat addTwo addOne x)
 
-eta-functions_two : (A B C : Set) (f : B → C) → (g : A → B) → (Id (A → C) (comp A B C f g) (λ x → (comp A B C f g) x))
-eta-functions_two = λ A B C → λ f → λ g → refl (A → C) (comp A B C f g)
+-- 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
+
+-- eta-functions_two : (A B C : Set) (f : B → C) → (g : A → B) → (Id (A → C) (comp A B C f g) (λ x → (comp A B C f g) x))
+-- eta-functions_two = λ A B C → λ f → λ g → refl (A → C) (comp A B C f g)
 
 -- apply : (A B : Set) → (A → B) → A → B
 -- apply = λ A B → λ f → λ x → f x
 
 -- eta-apply : (A B : Set) → (f : A → B) → Id (apply f) f
 
+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
 
-eta-counterexample : Id (Nat → Nat) addTwoAfterAddOne (λ x → (comp Nat Nat Nat addTwo addOne) x)
-eta-counterexample = refl (Nat → Nat) addTwoAfterAddOne
-
+-- eta-counterexample : Id (Nat → Nat) addTwoAfterAddOne (λ x → (comp Nat Nat Nat addTwo addOne) x)
+-- eta-counterexample = refl (Nat → Nat) addTwoAfterAddOne
 
-eta-counterexample-simple : Id (Nat → Nat) addOne (λ y → (λ x → (suc x)) y)
+eta-counterexample-simple : Id (Nat → Nat) addOne (λ x → suc (const x x))
 eta-counterexample-simple = refl (Nat → Nat) addOne
 
-
 -- eta-higher : (A B C : Set) → (f : A → B → C) → Id (λ x → λ y → f x y) f
 -- eta-higher = λ A B C → λ f → refl 

test/EtaFunctionsChurchWithConst.agda

@@ -0,0 +1,14 @@
+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
+
+const : (A : Set) → A → A → A
+const = λ A → λ x → λ y → x
+
+eta-functions_expl : (A B : Set) (f : A → B) → (Id (A → B) f (λ x → (f (const A x x))))
+eta-functions_expl = λ A B → λ f → refl (A → B) f
+
+
+