Add support for code auto-generation of records with non-dependent fu…

…nction fields

docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda

@@ -241,6 +241,7 @@ private
   renderHsType (def (quote Pair) (_ ∷ _ ∷ vArg a ∷ vArg b ∷ [])) = printf "(%s, %s)" (renderHsType a) (renderHsType b)
   renderHsType (def d []) = renderHsTypeName d
   renderHsType (def d vs) = printf "(%s %s)" (renderHsTypeName d) (joinStrings " " (renderHsArgs vs))
+  renderHsType (Π[ s ∶ arg _ a ] b) = printf "%s -> %s" (renderHsType a) (renderHsType b)
   renderHsType t = printf "(TODO: renderHsType %s)" (show t)
 
   renderHsArgs [] = []
@@ -269,14 +270,17 @@ private
                   (showName d) con
 
   hsImports : String
-  hsImports = "import GHC.Generics (Generic)"
+  hsImports = "import GHC.Generics (Generic)\nimport Text.Show.Functions\n"
+
+  hsInstances : String
+  hsInstances = "instance Eq (a -> b) where _ == _ = False\n" -- functions are never equal
 
   -- Take the name of a simple data type and generate the COMPILE and
   -- FOREIGN pragmas to bind to Haskell.
   bindHsType : NameEnv → Name → Name → TC ⊤
   bindHsType env agdaName hsName = getDefinition hsName >>= λ where
     (data-type pars cs) → do
-      pragmaForeign "GHC" hsImports
+      pragmaForeign "GHC" (hsImports & "\n" & hsInstances)
       pragmaCompile "GHC" hsName $ compilePragma hsName cs
       getDefinition agdaName >>= λ where
         (data-type _ _)    → pragmaForeign "GHC" =<< foreignPragma hsName cs