Fix #324: Keep track of instance-only imports

src/Agda2Hs/Compile/ClassInstance.hs

@@ -36,6 +36,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Function
 import Agda2Hs.Compile.Name
+import Agda2Hs.Compile.Term
 import Agda2Hs.Compile.Type
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -65,7 +66,7 @@ compileInstance :: InstanceTarget -> Definition -> C (Hs.Decl ())
 
 compileInstance (ToDerivation strategy) def@Defn{..} =
   setCurrentRangeQ defName $ do
-    reportSDoc "agda2hs.compile.instance" 13 $ 
+    reportSDoc "agda2hs.compile.instance" 13 $
       text "compiling instance" <+> prettyTCM defName <+> text "to standalone deriving"
     tellExtension Hs.StandaloneDeriving
     enableStrategy strategy
@@ -74,7 +75,7 @@ compileInstance (ToDerivation strategy) def@Defn{..} =
 
 compileInstance ToDefinition def@Defn{..} =
   enableCopatterns $ setCurrentRangeQ defName $ do
-    reportSDoc "agda2hs.compile.instance" 13 $ 
+    reportSDoc "agda2hs.compile.instance" 13 $
       text "compiling instance" <+> prettyTCM defName <+> text "to instance definition"
     ir <- compileInstRule [] (unEl defType)
     withFunctionLocals defName $ do
@@ -181,7 +182,7 @@ compileInstanceClause' curModule ty (p:ps) c
   -- reached record projection
   | ProjP _ q <- namedArg p = do
 
-    -- we put back the remaining patterns in the original clause 
+    -- we put back the remaining patterns in the original clause
     let c' = c {namedClausePats = ps}
 
     -- We want the actual field name, not the instance-opened projection.
@@ -198,9 +199,9 @@ compileInstanceClause' curModule ty (p:ps) c
     -- retrieve the type of the projection
     Just (unEl -> Pi a b) <- getDefType q ty
     -- We don't really have the information available to reconstruct the instance
-    -- head. However, all dependencies on the instance head are in erased positions, 
+    -- head. However, all dependencies on the instance head are in erased positions,
     -- so we can just use a dummy term instead
-    let instanceHead = __DUMMY_TERM__ 
+    let instanceHead = __DUMMY_TERM__
         ty' = b `absApp` instanceHead
 
     reportSDoc "agda2hs.compile.instance" 15 $
@@ -245,7 +246,7 @@ compileInstanceClause' curModule ty (p:ps) c
           text $ "raw name: " ++ prettyShow (Def n [])
         d@Defn{..} <- getConstInfo n
         let mod = if isExtendedLambdaName defName then curModule else qnameModule defName
-        (fc, rs) <- withCurrentModule mod $ 
+        (fc, rs) <- withCurrentModule mod $
           concatUnzip <$> mapM (compileInstanceClause mod defType) (funClauses theDef)
         let hd = hsName $ prettyShow $ nameConcrete $ qnameName defName
         let fc' = {- dropPatterns 1 $ -} replaceName hd uf fc

src/Agda2Hs/Compile/Imports.hs

@@ -25,10 +25,12 @@ type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap
 
 compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()]
 compileImports top is0 = do
-  let is = filter (not . (top `isPrefixOf`) . Hs.prettyPrint . importModule) is0
+  let is = filter ((top /=) . Hs.prettyPrint . importModule) is0
   checkClashingImports is
   let imps = Map.toList $ groupModules is
-  return $ map (uncurry $ uncurry makeImportDecl) imps
+  reportSLn "agda2hs.import" 10 $ "All imported modules: " ++ show (map (pp . fst . fst) imps)
+  let decls = map (uncurry $ uncurry makeImportDecl) imps
+  return decls
   where
     mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap
     mergeChildren = Map.unionWith Set.union
@@ -38,18 +40,20 @@ compileImports top is0 = do
     makeSingle (Just p) q = Map.singleton p $ Set.singleton q
 
     groupModules :: [Import] -> ImportDeclMap
-    groupModules = foldr
-      (\(Import mod as p q ns) -> Map.insertWith mergeChildren (mod,as)
-                                                                (makeSingle (parentNN p) (NamespacedName ns q)))
-      Map.empty
-        where
-          parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName
-          parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name
-                                                                        -- ^ for parents, if they are operators, we assume they are type operators
-                                                                        -- but actually, this will get lost anyway because of the structure of ImportSpec
-                                                                        -- the point is that there should not be two tuples with the same name and diffenrent namespaces
-          parentNN (Just name)                 = Just $ NamespacedName (Hs.NoNamespace ())   name
-          parentNN Nothing                     = Nothing
+    groupModules = flip foldr Map.empty $ \case
+        (Import mod as p q ns) ->
+          Map.insertWith mergeChildren (mod,as)
+                         (makeSingle (parentNN p) (NamespacedName ns q))
+        (ImportInstances mod) ->
+          Map.insertWith mergeChildren (mod,Unqualified) Map.empty
+      where
+        parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName
+        parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name
+                                                                      -- ^ for parents, if they are operators, we assume they are type operators
+                                                                      -- but actually, this will get lost anyway because of the structure of ImportSpec
+                                                                      -- the point is that there should not be two tuples with the same name and diffenrent namespaces
+        parentNN (Just name)                 = Just $ NamespacedName (Hs.NoNamespace ())   name
+        parentNN Nothing                     = Nothing
 
     -- TODO: avoid having to do this by having a CName instead of a
     -- Name in the Import datatype
@@ -81,11 +85,13 @@ compileImports top is0 = do
         []      -> checkClashingImports is
      where
         isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q)
+        isClashing ImportInstances{} = False
         mkErrorMsg (Import _ _ p' q' _) =
              "Clashing import: " ++ pp q ++ " (both from "
           ++ prettyShow (pp <$> p) ++ " and "
           ++ prettyShow (pp <$> p') ++ ")"
         -- TODO: no range information as we only have Haskell names at this point
+    checkClashingImports (ImportInstances mod : is) = checkClashingImports is
 
 
 -- | Generate a prelude import considering prelude config options (hiding, implicit, etc).

src/Agda2Hs/Compile/Name.hs

@@ -230,3 +230,10 @@ compileModuleName m = do
     text "Top-level module name for" <+> prettyTCM m <+>
     text "is" <+> text (pp tlm)
   return tlm
+
+importInstance :: QName -> C ()
+importInstance f = do
+  mod <- compileModuleName $ qnameModule f
+  unless (isPrimModule mod) $ do
+    reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod
+    tellImport $ ImportInstances mod

src/Agda2Hs/Compile/Term.hs

@@ -2,6 +2,7 @@ module Agda2Hs.Compile.Term where
 
 import Control.Arrow ( (>>>), (&&&), second )
 import Control.Monad ( unless, zipWithM )
+import Control.Monad.Except
 import Control.Monad.Reader
 
 import Data.Foldable ( toList )
@@ -19,11 +20,16 @@ import Agda.Syntax.Common
 import Agda.Syntax.Literal
 import Agda.Syntax.Internal
 
+import Agda.TypeChecking.CheckInternal ( infer )
+import Agda.TypeChecking.Constraints ( noConstraints )
+import Agda.TypeChecking.Conversion ( equalTerm )
+import Agda.TypeChecking.InstanceArguments ( findInstance )
+import Agda.TypeChecking.MetaVars ( newInstanceMeta )
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records ( shouldBeProjectible, isRecordType, recordFieldNames )
 import Agda.TypeChecking.Datatypes ( getConType )
-import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate )
+import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate, reduce )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM, flattenTel )
 import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
@@ -35,7 +41,7 @@ import Agda.Utils.Monad
 import Agda.Utils.Size
 
 import Agda2Hs.AgdaUtils
-import Agda2Hs.Compile.Name ( compileQName )
+import Agda2Hs.Compile.Name ( compileQName, importInstance )
 
 import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize )
 import Agda2Hs.Compile.Types
@@ -615,3 +621,42 @@ compileLiteral (LitChar c)   = return $ Hs.charE c
 compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s
   where s = Text.unpack t
 compileLiteral l             = genericDocError =<< text "bad term:" <?> prettyTCM (Lit l)
+
+
+checkInstance :: Term -> C ()
+checkInstance u = do
+  reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
+  reduce u >>= \case
+    Var x es -> do
+      unlessM (isInstance <$> domOfBV x) illegalInstance
+      checkInstanceElims es
+    Def f es -> do
+      unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance
+      importInstance f
+      checkInstanceElims es
+  -- We need to compile applications of `fromNat`, `fromNeg`, and
+  -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally
+  -- this constraint would be marked as erased but this would involve
+  -- changing Agda builtins.
+    Con c _ _
+      | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
+        prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
+        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
+    _ -> illegalInstance
+
+  where
+    illegalInstance :: C ()
+    illegalInstance = do
+      reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u
+      genericDocError =<< text "illegal instance: " <+> prettyTCM u
+
+    checkInstanceElims :: Elims -> C ()
+    checkInstanceElims = mapM_ checkInstanceElim
+
+    checkInstanceElim :: Elim -> C ()
+    checkInstanceElim (Apply v) =
+      when (isInstance v && usableQuantity v) $
+        checkInstance $ unArg v
+    checkInstanceElim IApply{} = illegalInstance
+    checkInstanceElim (Proj _ f) =
+      unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance

src/Agda2Hs/Compile/Types.hs

@@ -108,15 +108,20 @@ qualifiedAs = join
 
 -- | Encoding of a Haskell module import statement.
 data Import = Import
-  { importModule    :: Hs.ModuleName ()
-  , importQualified :: Qualifier
-  , importParent    :: Maybe (Hs.Name ())
-  , importName      :: Hs.Name ()
-  , importNamespace :: Hs.Namespace ()
+  { _importModule    :: Hs.ModuleName ()
+  , _importQualified :: Qualifier
+  , _importParent    :: Maybe (Hs.Name ())
+  , _importName      :: Hs.Name ()
+  , _importNamespace :: Hs.Namespace ()
                     -- ^^ if this is a type or something like that, we can add a namespace qualifier to the import spec
                     -- now it's only useful for differentiating type operators; so for others we always put Hs.NoNamespace () here
                     -- (we don't calculate it if it's not necessary)
   }
+  | ImportInstances (Hs.ModuleName ())
+
+importModule :: Import -> Hs.ModuleName ()
+importModule (Import{ _importModule = mod }) = mod
+importModule (ImportInstances mod) = mod
 
 type Imports = [Import]
 

src/Agda2Hs/Compile/Utils.hs

@@ -7,6 +7,7 @@ import Control.Monad.Reader
 import Control.Monad.Writer ( tell )
 import Control.Monad.State ( put, modify )
 
+import Data.List ( isPrefixOf )
 import Data.Maybe ( isJust )
 import qualified Data.Map as M
 import Data.List ( isPrefixOf )
@@ -252,43 +253,6 @@ isInlinedFunction q = do
       (InlinePragma ==) <$> processPragma r
     _ -> return False
 
-checkInstance :: Term -> C ()
-checkInstance u = do
-  reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
-  reduce u >>= \case
-    Var x es -> do
-      unlessM (isInstance <$> domOfBV x) illegalInstance
-      checkInstanceElims es
-    Def f es -> do
-      unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance
-      checkInstanceElims es
-  -- We need to compile applications of `fromNat`, `fromNeg`, and
-  -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally
-  -- this constraint would be marked as erased but this would involve
-  -- changing Agda builtins.
-    Con c _ _
-      | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
-        prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
-        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
-    _ -> illegalInstance
-
-  where
-    illegalInstance :: C ()
-    illegalInstance = do
-      reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u
-      genericDocError =<< text "illegal instance: " <+> prettyTCM u
-
-    checkInstanceElims :: Elims -> C ()
-    checkInstanceElims = mapM_ checkInstanceElim
-
-    checkInstanceElim :: Elim -> C ()
-    checkInstanceElim (Apply v) =
-      when (isInstance v && usableQuantity v) $
-        checkInstance $ unArg v
-    checkInstanceElim IApply{} = illegalInstance
-    checkInstanceElim (Proj _ f) =
-      unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance
-
 withNestedType :: C a -> C a
 withNestedType = local $ \e -> e { isNestedInType = True }
 

src/Agda2Hs/Render.hs

@@ -104,7 +104,7 @@ prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) =
                 ++ parenList (map prettyShowSpec ispecs)
 
       parenList :: [String] -> String
-      parenList [] = ""
+      parenList [] = "()"
       parenList (x:xs) = '(' : (x ++ go xs)
         where
           go :: [String] -> String

test/AllTests.agda

@@ -92,6 +92,7 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue324
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -181,4 +182,5 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue324
 #-}

test/Issue324.agda

@@ -0,0 +1,8 @@
+
+open import Haskell.Prelude
+open import Issue324instance
+
+test : Bool
+test = not == id
+
+{-# COMPILE AGDA2HS test #-}

test/Issue324instance.agda

@@ -0,0 +1,9 @@
+
+open import Haskell.Prelude
+
+instance
+  eqBoolFun : Eq (Bool → Bool)
+  eqBoolFun ._==_ x y = x True == y True && x False == y False
+
+{-# COMPILE AGDA2HS eqBoolFun #-}
+

test/golden/AllTests.hs

@@ -87,4 +87,5 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+import Issue324
 

test/golden/Issue324.hs

@@ -0,0 +1,7 @@
+module Issue324 where
+
+import Issue324instance ()
+
+test :: Bool
+test = not == id
+

test/golden/Issue324instance.hs

@@ -0,0 +1,5 @@
+module Issue324instance where
+
+instance Eq (Bool -> Bool) where
+    x == y = x True == y True && x False == y False
+

test/golden/QualifiedImports.hs

@@ -1,6 +1,7 @@
 module QualifiedImports where
 
 import qualified Importee (Foo(MkFoo), foo)
+import QualifiedImportee ()
 import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
 
 -- ** simple qualification

test/golden/RequalifiedImports.hs

@@ -1,6 +1,7 @@
 module RequalifiedImports where
 
 import OtherImportee (OtherFoo(MkFoo))
+import QualifiedImportee ()
 import qualified QualifiedImportee as A (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
 
 -- ** conflicting imports are all replaced with the "smallest" qualifier