[ fix #119 ] Raise a warning when an unknown name appears in generated Haskell code

src/Agda2Hs/Compile/ClassInstance.hs

@@ -333,7 +333,7 @@ resolveStringName s = do
 lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]
 lookupDefaultImplementations recName fields = do
   let modName = qnameToMName recName
-      isField f _ = (`elem` fields) . unQual <$> compileQName f
+      isField f _ = (`elem` fields) <$> compileName (qnameName f)
   findDefinitions isField modName
 
 classMemberNames :: Definition -> C [Hs.Name ()]

src/Agda2Hs/Compile/Name.hs

@@ -31,8 +31,10 @@ import qualified Agda.Syntax.Common.Pretty as P
 import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records ( isRecordConstructor )
+import Agda.TypeChecking.Warnings ( warning )
 
 import qualified Agda.Utils.List1 as List1
+import Agda.Utils.Monad
 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
 import Agda.Utils.Monad ( whenM )
 
@@ -102,11 +104,28 @@ compileQName f
       Just (r, def) | not (_recNamedCon def) -> r -- use record name for unnamed constructors
       _                                      -> f
     hf0 <- compileName (qnameName f)
-    (hf, mimpBuiltin) <- fromMaybe (hf0, Nothing) <$> isSpecialName f
+    special <- isSpecialName f
+    let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) special
+
     parent <- parentName f
     par <- traverse (compileName . qnameName) parent
     let mod0 = qnameModule $ fromMaybe f parent
     mod <- compileModuleName mod0
+
+    existsInHaskell <- orM
+      [ pure $ isJust special
+      , pure $ isPrimModule mod
+      , hasCompilePragma f
+      , isClassFunction f
+      , isWhereFunction f
+      , maybe (pure False) hasCompilePragma parent
+      ]
+
+    unless existsInHaskell $ do
+      reportSDoc "agda2hs.name" 20 $ text "DOES NOT EXIST IN HASKELL"
+      typeError $ CustomBackendError "agda2hs" $ P.text $
+        "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule"
+
     currMod <- hsTopLevelModuleName <$> asks currModule
     let skipModule = mod == currMod
                   || isJust mimpBuiltin
@@ -185,14 +204,19 @@ compileQName f
 
     mkImport mod qual par hf maybeIsType
       -- make sure the Prelude is properly qualified
-      | any (`isPrefixOf` pp mod) primModules
+      | isPrimModule mod
       = if isQualified qual then
           let mod' = hsModuleName "Prelude"
           in (mod', Just (Import mod' qual Nothing hf maybeIsType))
         else (mod, Nothing)
       | otherwise
       = (mod, Just (Import mod qual par hf maybeIsType))
 
+isWhereFunction :: QName -> C Bool
+isWhereFunction f = do
+  whereMods <- asks whereModules
+  return $ any (qnameModule f `isLeChildModuleOf`) whereMods
+
 hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()
 hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack
                      . List1.toList . moduleNameParts

src/Agda2Hs/Compile/Record.hs

@@ -16,7 +16,7 @@ import Agda.Syntax.Common ( Arg(unArg), defaultArg )
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
-import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM )
+import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM, pretty, prettyList_ )
 import Agda.TypeChecking.Substitute ( TelV(TelV), Apply(apply) )
 import Agda.TypeChecking.Telescope
 
@@ -38,7 +38,10 @@ withMinRecord :: QName -> C a -> C a
 withMinRecord m = local $ \ e -> e { minRecordName = Just (qnameToMName m) }
 
 compileMinRecord :: [Hs.Name ()] -> QName -> C MinRecord
-compileMinRecord fieldNames m = do
+compileMinRecord fieldNames m = withMinRecord m $ do
+  reportSDoc "agda2hs.record.min" 20 $
+    text "Compiling minimal record" <+> pretty m <+>
+    text "with field names" <+> prettyList_ (map (text . pp) fieldNames)
   rdef <- getConstInfo m
   definedFields <- classMemberNames rdef
   let Record{recPars = npars, recTel = tel} = theDef rdef
@@ -48,9 +51,12 @@ compileMinRecord fieldNames m = do
   -- We can't simply compileFun here for two reasons:
   -- * it has an explicit dictionary argument
   -- * it's using the fields and definitions from the minimal record and not the parent record
-  compiled <- withMinRecord m $ addContext (defaultDom rtype) $ compileLocal $
+  compiled <- addContext (defaultDom rtype) $ compileLocal $
     fmap concat $ traverse (compileFun False) defaults
   let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]
+  reportSDoc "agda2hs.record.min" 20 $
+    text "Done compiling minimal record" <+> pretty m <+>
+    text "defined fields: " <+> prettyList_ (map (text . pp) definedFields)
   return (definedFields, declMap)
 
 

src/Agda2Hs/Compile/Types.hs

@@ -22,6 +22,7 @@ import qualified Language.Haskell.Exts.Comments as Hs
 import Agda.Compiler.Backend
 import Agda.Syntax.Position ( Range )
 import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )
+import Agda.TypeChecking.Warnings ( MonadWarning )
 import Agda.Utils.Null
 import Agda.Utils.Impossible
 
@@ -174,6 +175,7 @@ instance MonadStConcreteNames C where
   runStConcreteNames m = rwsT $ \r s -> runStConcreteNames $ StateT $ \ns -> do
     ((x, ns'), s', w) <- runRWST (runStateT m ns) r s
     pure ((x, s', w), ns')
+instance MonadWarning C where
 instance IsString a => IsString (C a) where fromString = pure . fromString
 instance PureTCM C where
 instance Null a => Null (C a) where

src/Agda2Hs/Compile/Utils.hs

@@ -9,6 +9,7 @@ import Control.Monad.State ( put, modify )
 
 import Data.Maybe ( isJust )
 import qualified Data.Map as M
+import Data.List ( isPrefixOf )
 
 import qualified Language.Haskell.Exts as Hs
 
@@ -60,6 +61,8 @@ primModules =
   , "Haskell.Law"
   ]
 
+isPrimModule :: Hs.ModuleName () -> Bool
+isPrimModule mod = any (`isPrefixOf` pp mod) primModules
 
 concatUnzip :: [([a], [b])] -> ([a], [b])
 concatUnzip = (concat *** concat) . unzip
@@ -152,6 +155,18 @@ isErasedBaseType x = orM
   ]
   where b = El __DUMMY_SORT__ x
 
+hasCompilePragma :: QName -> C Bool
+hasCompilePragma q = processPragma q <&> \case
+  NoPragma{} -> False
+  InlinePragma{} -> True
+  DefaultPragma{} -> True
+  ClassPragma{} -> True
+  ExistingClassPragma{} -> True
+  UnboxPragma{} -> True
+  TransparentPragma{} -> True
+  NewTypePragma{} -> True
+  DerivePragma{} -> True
+
 -- Exploits the fact that the name of the record type and the name of the record module are the
 -- same, including the unique name ids.
 isClassFunction :: QName -> C Bool
@@ -267,10 +282,9 @@ checkInstance u = do
     checkInstanceElims = mapM_ checkInstanceElim
 
     checkInstanceElim :: Elim -> C ()
-    checkInstanceElim (Apply v) = case getHiding v of
-      Instance{} -> checkInstance $ unArg v
-      Hidden     -> return ()
-      NotHidden  -> return ()
+    checkInstanceElim (Apply v) =
+      when (isInstance v && usableQuantity v) $
+        checkInstance $ unArg v
     checkInstanceElim IApply{} = illegalInstance
     checkInstanceElim (Proj _ f) =
       unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance

test/Delay.agda

@@ -8,16 +8,21 @@ open import Haskell.Extra.Delay
 open import Agda.Builtin.Size
 
 postulate
-  div : Int → Int → Int
-  mod : Int → Int → Int
+  div' : Int → Int → Int
+  mod' : Int → Int → Int
 
-even : Int → Bool
-even x = mod x 2 == 0
+{-# COMPILE AGDA2HS div' #-}
+{-# COMPILE AGDA2HS mod' #-}
+
+even' : Int → Bool
+even' x = mod' x 2 == 0
+
+{-# COMPILE AGDA2HS even' #-}
 
 collatz : ∀ {@0 j} → Int → Delay Int j
-collatz x = 
+collatz x =
   if x == 0 then now 0
-  else if even x then later (λ where .force → collatz (div x 2))
+  else if even' x then later (λ where .force → collatz (div' x 2))
   else later λ where .force → collatz (3 * x + 1)
 
 {-# COMPILE AGDA2HS collatz #-}

test/Fail/Issue119.agda

@@ -0,0 +1,13 @@
+module Fail.Issue119 where
+
+open import Haskell.Prelude
+
+aaa : Int
+aaa = 21
+
+-- Oops, forgot compile pragma for aaa
+
+bbb : Int
+bbb = aaa + aaa
+
+{-# COMPILE AGDA2HS bbb #-}

test/TypeOperatorImport.agda

@@ -2,15 +2,9 @@ module TypeOperatorImport where
 
 {-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
 
-open import Agda.Builtin.Unit
-open import Agda.Builtin.Bool
-open import Haskell.Prelude using (_∘_)
+open import Haskell.Prelude hiding (_<_)
 open import TypeOperatorExport
 
-not : Bool → Bool
-not true  = false
-not false = true
-
 test1 : ⊤ < Bool
 test1 = tt
 {-# COMPILE AGDA2HS test1 #-}

test/golden/Delay.hs

@@ -1,7 +1,16 @@
 module Delay where
 
+div' :: Int -> Int -> Int
+div' = error "postulate: Int -> Int -> Int"
+
+mod' :: Int -> Int -> Int
+mod' = error "postulate: Int -> Int -> Int"
+
+even' :: Int -> Bool
+even' x = mod' x 2 == 0
+
 collatz :: Int -> Int
 collatz x
   = if x == 0 then 0 else
-      if even x then collatz (div x 2) else collatz (3 * x + 1)
+      if even' x then collatz (div' x 2) else collatz (3 * x + 1)
 

test/golden/Issue119.err

@@ -0,0 +1,2 @@
+test/Fail/Issue119.agda:10,1-4
+agda2hs: Symbol aaa is missing a COMPILE pragma or rewrite rule