Fix #169 (#202)

* [ re #169 ] Don't consider data/record modules as qualified imports

* [ fix #169 ] Throw error when minimal record does not use named definition or \where

src/Agda2Hs/AgdaUtils.hs

@@ -2,6 +2,7 @@ module Agda2Hs.AgdaUtils where
 
 import Data.Data
 import Data.Monoid ( Any(..) )
+import qualified Data.Map as Map
 import Data.Maybe ( fromMaybe )
 
 import Agda.Compiler.Backend hiding ( Args )
@@ -10,8 +11,11 @@ import Agda.Interaction.FindFile ( findFile' )
 
 import Agda.Syntax.Common ( Arg, defaultArg )
 import Agda.Syntax.Common.Pretty ( prettyShow )
+import qualified Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal
 import Agda.Syntax.Internal.Names
+import Agda.Syntax.Scope.Base
+import Agda.Syntax.Scope.Monad
 import Agda.Syntax.TopLevelModuleName
 
 import Agda.TypeChecking.Monad ( topLevelModuleName )
@@ -20,6 +24,7 @@ import Agda.TypeChecking.Substitute
 
 import Agda.Utils.Either ( isRight )
 import Agda.Utils.List ( initMaybe )
+import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Monad ( ifM )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
@@ -92,3 +97,7 @@ getTopLevelModuleForModuleName = loop . mnameToList
 
 getTopLevelModuleForQName :: QName -> TCM (Maybe TopLevelModuleName)
 getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule
+
+lookupModuleInCurrentModule :: C.Name -> TCM [AbstractModule]
+lookupModuleInCurrentModule x =
+  List1.toList' . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope

src/Agda2Hs/Compile/ClassInstance.hs

@@ -138,6 +138,10 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do
       -- We want the actual field name, not the instance-opened projection.
       (q, _, _) <- origProjection q
       arg <- fieldArgInfo q
+
+      reportSDoc "agda2hs.compile.instance" 15 $
+        text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q [])
+
       let uf = hsName $ prettyShow $ nameConcrete $ qnameName q
 
       let
@@ -169,25 +173,37 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do
         -- Projection of a primitive field: chase down definition and inline as instance clause.
         | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
         , [(_, f)] <- mapMaybe isProjElim es
-        , f .~ q
-        -> do d <- chaseDef n
-              fc <- compileFun False d
-              let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d
-              let fc' = dropPatterns 1 $ replaceName hd uf fc
-              return (map (Hs.InsDecl ()) fc', [n])
+        , f .~ q -> do
+          reportSDoc "agda2hs.compile.instance" 20 $
+            text "Instance clause is projected from" <+> prettyTCM (Def n [])
+          reportSDoc "agda2hs.compile.instance" 20 $
+            text $ "raw projection:" ++ prettyShow (Def n [])
+          d <- chaseDef n
+          fc <- compileFun False d
+          let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d
+          let fc' = dropPatterns 1 $ replaceName hd uf fc
+          return (map (Hs.InsDecl ()) fc', [n])
 
          -- Projection of a default implementation: drop while making sure these are drawn from the
          -- same (minimal) dictionary as the primitive fields.
-         | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
-         , n .~ q
-         , Just [ Def n' _ ] <- map unArg . filter keepArg <$> allApplyElims es
-         -> do n' <- resolveExtendedLambda n'
-               return ([], [n'])
-
-         -- No minimal dictionary used, proceed with compiling as a regular clause.
-         | otherwise
-         -> do ms <- disableCopatterns $ compileClause curModule uf c'
-               return ([Hs.InsDecl () (Hs.FunBind () (toList ms)) | keepArg arg], [])
+        | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
+        , n .~ q -> do
+          case map unArg . filter keepArg <$> allApplyElims es of
+            Just [ Def f _ ] -> do
+              reportSDoc "agda2hs.compile.instance" 20 $ vcat
+                  [ text "Dropping default instance clause" <+> prettyTCM c'
+                  , text "with minimal dictionary" <+> prettyTCM f
+                  ]
+              reportSDoc "agda2hs.compile.instance" 40 $
+                  text $ "raw dictionary:" ++ prettyShow f
+              return ([], [f])
+            _ -> genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+
+        -- No minimal dictionary used, proceed with compiling as a regular clause.
+        | otherwise -> do
+          reportSDoc "agda2hs.compile.instance" 20 $ text "Compiling instance clause" <+> prettyTCM c'
+          ms <- disableCopatterns $ compileClause curModule uf c'
+          return ([Hs.InsDecl () (Hs.FunBind () (toList ms))], [])
 
 fieldArgInfo :: QName -> C ArgInfo
 fieldArgInfo f = do

src/Agda2Hs/Compile/Name.hs

@@ -3,8 +3,10 @@ module Agda2Hs.Compile.Name where
 import Control.Arrow ( (>>>) )
 import Control.Applicative ( (<|>) )
 import Control.Monad
+import Control.Monad.Except ( catchError )
 import Control.Monad.Reader
 
+import Data.Functor ( (<&>) )
 import Data.List ( intercalate, isPrefixOf )
 import Data.Text ( unpack )
 
@@ -13,20 +15,23 @@ import qualified Language.Haskell.Exts as Hs
 import Agda.Compiler.Backend hiding ( topLevelModuleName )
 import Agda.Compiler.Common ( topLevelModuleName )
 
+import qualified Agda.Syntax.Abstract as A
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Position
 import qualified Agda.Syntax.Concrete as C
-import Agda.Syntax.Scope.Base ( inverseScopeLookupName )
+import Agda.Syntax.Scope.Base ( inverseScopeLookupName, amodName )
+import Agda.Syntax.Scope.Monad ( resolveName, isDatatypeModule )
 import Agda.Syntax.TopLevelModuleName
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import qualified Agda.Syntax.Common.Pretty as P
 
+import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records ( isRecordConstructor )
 
 import qualified Agda.Utils.List1 as List1
-import Agda.Utils.Maybe ( isJust, whenJust, fromMaybe, caseMaybeM )
+import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Rewrites
@@ -140,12 +145,17 @@ compileQName f
 
     getQualifier :: QName -> Hs.ModuleName () -> C Qualifier
     getQualifier f mod =
-      (inverseScopeLookupName f <$> getScope) >>= return . \case
-        (C.Qual as C.QName{} : _)
-          | qual <- hsModuleName $ prettyShow as, qual /= mod
-          -> QualifiedAs (Just qual)
-        (C.Qual{} : _) -> QualifiedAs Nothing
-        _ -> Unqualified
+      (inverseScopeLookupName f <$> getScope) >>= \case
+        (C.QName{} : _) -> return Unqualified
+        (C.Qual as C.QName{} : _) -> liftTCM $ do
+          let qual = hsModuleName $ prettyShow as
+          lookupModuleInCurrentModule as >>= \case
+            (x:_) | qual /= mod -> isDatatypeModule (amodName x) >>= \case
+              Just{} -> return $ QualifiedAs Nothing
+              Nothing -> return $ QualifiedAs $ Just qual
+            _ -> return Nothing
+          `catchError` \_ -> return $ QualifiedAs Nothing
+        _ -> return $ QualifiedAs Nothing
 
     qualify :: Hs.ModuleName () -> Hs.Name () -> Qualifier -> Hs.QName ()
     qualify mod n = \case

test/AllTests.agda

@@ -58,6 +58,7 @@ import TypeOperatorImport
 import IOFile
 import IOInput
 import Issue200
+import Issue169
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -116,4 +117,5 @@ import TypeOperatorImport
 import IOFile
 import IOInput
 import Issue200
+import Issue169
 #-}

test/Fail/Issue169-record.agda

@@ -0,0 +1,25 @@
+-- Using a default method implementation for an instance declaration currently
+-- requires a named definition or an anonymous `λ where` on the Agda side, so a
+-- record is not allowed.
+
+module Fail.Issue169-record where
+
+open import Haskell.Prelude
+
+record Identity (a : Set) : Set where
+    field
+        runIdentity : a
+open Identity public
+
+{-# COMPILE AGDA2HS Identity newtype #-}
+
+showIdentity : ⦃ Show a ⦄ → Identity a → String
+showIdentity record { runIdentity = id } = "Id < " ++ show id ++ " >"
+
+{-# COMPILE AGDA2HS showIdentity #-}
+
+instance
+  iIdentityShow : ⦃ Show a ⦄ → Show (Identity a)
+  iIdentityShow = record {Show₂ record {show = showIdentity}}
+
+{-# COMPILE AGDA2HS iIdentityShow #-}

test/Issue169.agda

@@ -0,0 +1,19 @@
+open import Haskell.Prelude
+
+record Identity (a : Set) : Set where
+    field
+        runIdentity : a
+open Identity public
+
+{-# COMPILE AGDA2HS Identity newtype #-}
+
+showIdentity : ⦃ Show a ⦄ → Identity a → String
+showIdentity record { runIdentity = id } = "Id < " ++ show id ++ " >"
+
+{-# COMPILE AGDA2HS showIdentity #-}
+
+instance
+  iIdentityShow : ⦃ Show a ⦄ → Show (Identity a)
+  iIdentityShow = record {Show₂ (λ where .Show₂.show → showIdentity)}
+
+{-# COMPILE AGDA2HS iIdentityShow #-}

test/golden/AllTests.hs

@@ -56,4 +56,5 @@ import TypeOperatorImport
 import IOFile
 import IOInput
 import Issue200
+import Issue169
 

test/golden/Issue169-record.err

@@ -0,0 +1,2 @@
+test/Fail/Issue169-record.agda:22,3-16
+illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`.

test/golden/Issue169.hs

@@ -0,0 +1,10 @@
+module Issue169 where
+
+newtype Identity a = Identity{runIdentity :: a}
+
+showIdentity :: Show a => Identity a -> String
+showIdentity (Identity id) = "Id < " ++ show id ++ " >"
+
+instance (Show a) => Show (Identity a) where
+    show = showIdentity
+

test/golden/QualifiedImports.hs

@@ -1,15 +1,15 @@
 module QualifiedImports where
 
-import qualified Importee (Foo(MkFoo), foo)
+import Importee (Foo(MkFoo), foo)
 import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
 
 -- ** simple qualification
 
 simpqualBar :: Int
-simpqualBar = Importee.foo
+simpqualBar = foo
 
-simpfoo :: Importee.Foo
-simpfoo = Importee.MkFoo
+simpfoo :: Foo
+simpfoo = MkFoo
 
 -- ** qualified imports