allow erased module arguments

src/Agda2Hs/AgdaUtils.hs

@@ -21,6 +21,7 @@ import Agda.Syntax.TopLevelModuleName
 import Agda.TypeChecking.Monad ( topLevelModuleName )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Reduce ( reduceDefCopy )
 
 import Agda.Utils.Either ( isRight )
 import Agda.Utils.List ( initMaybe )
@@ -104,3 +105,18 @@ getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule
 lookupModuleInCurrentModule :: C.Name -> TCM [AbstractModule]
 lookupModuleInCurrentModule x =
   List1.toList' . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope
+
+-- | Try to unfold a definition if introduced by module application.
+maybeUnfoldCopy
+  :: PureTCM m
+  => QName -- ^ Name of the definition.
+  -> Elims
+  -> (Term -> m a)
+  -- ^ Callback if the definition is indeed a copy.
+  -> (QName -> Elims -> m a)
+  -- ^ Callback if the definition isn't a copy.
+  -> m a
+maybeUnfoldCopy f es onTerm onDef =
+  reduceDefCopy f es >>= \case
+    NoReduction ()   -> onDef f es
+    YesReduction _ t -> onTerm t

src/Agda2Hs/Compile/Function.hs

@@ -100,19 +100,32 @@ compileFun, compileFun' :: Bool -> Definition -> C [Hs.Decl ()]
 compileFun withSig def@Defn{..} = withFunctionLocals defName $ compileFun' withSig def
 -- inherit existing (instantiated) locals
 compileFun' withSig def@(Defn {..}) = do
-  reportSDoc "agda2hs.compile" 6 $ "compiling function: " <+> prettyTCM defName
+  reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
   when withSig $ whenJustM (liftTCM $ isDatatypeModule $ qnameModule defName) $ \_ ->
     genericDocError =<< text "not supported by agda2hs: functions inside a record module"
   let keepClause = maybe False keepArg . clauseType
   withCurrentModule m $ do
-    ifM (endsInSort defType) (ensureNoLocals err >> compileTypeDef x def) $ do
+    ifM (endsInSort defType)
+        -- if the function type ends in Sort, it's a type alias!
+        (ensureNoLocals err >> compileTypeDef x def) 
+        -- otherwise, we have to compile clauses.
+        $ do
       when withSig $ checkValidFunName x
       compileTopLevelType withSig defType $ \ty -> do
-        -- Instantiate the clauses to the current module parameters
+        let filtered = filter keepClause funClauses
+        weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)
         pars <- getContextArgs
-        reportSDoc "agda2hs.compile" 10 $ "applying clauses to parameters: " <+> prettyTCM pars
-        let clauses = filter keepClause funClauses `apply` pars
+        -- We only instantiate the clauses to the current module parameters
+        -- if the current module isn't the toplevel module
+        unless weAreOnTop $
+          reportSDoc "agda2hs.compile.type" 6 $ "Applying module parameters to clauses: " <+> prettyTCM pars
+        let clauses = if weAreOnTop then filtered else filtered `apply` pars
         cs <- mapMaybeM (compileClause (qnameModule defName) x) clauses
+
+        when (null cs) $ genericDocError
+          =<< text "Functions defined with absurd patterns exclusively are not supported."
+          <+> text "Use function `error` from the Haskell.Prelude instead."
+
         return $ [Hs.TypeSig () [x] ty | withSig ] ++ [Hs.FunBind () cs]
   where
     Function{..} = theDef
@@ -128,7 +141,7 @@ compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))
 compileClause mod x c = withClauseLocals mod c $ compileClause' mod x c
 
 compileClause' :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))
-compileClause' curModule x c@Clause{ clauseBody = Nothing} = return Nothing
+compileClause' curModule x c@Clause{clauseBody = Nothing} = pure Nothing
 compileClause' curModule x c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c
   reportSDoc "agda2hs.compile" 17 $ "Old context: " <+> (prettyTCM =<< getContext)

src/Agda2Hs/Compile/Term.hs

@@ -208,6 +208,7 @@ compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s
   where s = Text.unpack t
 compileLiteral l               = genericDocError =<< text "bad term:" <?> prettyTCM (Lit l)
 
+-- | Compile a variable. If the check is enabled, ensures the variable is usable and visible.
 compileVar :: Nat -> C String
 compileVar x = do
   (d, n) <- (fmap snd &&& fst . unDom) <$> lookupBV x
@@ -229,25 +230,29 @@ compileTerm v = do
       hsVar s `app` es
     -- v currently we assume all record projections are instance
     -- args that need attention
-    Def f es
+    Def f es -> maybeUnfoldCopy f es compileTerm $ \f es -> if
       | Just semantics <- isSpecialTerm f -> do
-        reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
-        semantics f es
+          reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
+          semantics f es
       | otherwise -> isClassFunction f >>= \case
-        True  -> compileClassFunApp f es
-        False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case
-          True  -> compileErasedApp es
-          False -> do
-            reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
-            -- Drop module parameters of local `where` functions
-            moduleArgs <- getDefFreeVars f
-            reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
-            (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
-    Con h i es
-      | Just semantics <- isSpecialCon (conName h) -> semantics h i es
-    Con h i es -> isUnboxConstructor (conName h) >>= \case
-      Just _  -> compileErasedApp es
-      Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)
+          True  -> compileClassFunApp f es
+          False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case
+            True  -> compileErasedApp es
+            False -> do
+              reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
+              -- Drop module parameters of local `where` functions
+              moduleArgs <- getDefFreeVars f
+              reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
+              (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
+    Con h i es -> do
+      reportSDoc "agda2hs.compile" 8 $ text "reached constructor:" <+> prettyTCM (conName h)
+      -- the constructor may be a copy introduced by module application,
+      -- therefore we need to find the original constructor
+      info <- getConstInfo (conName h)
+      if not (defCopy info)
+        then compileCon h i es
+        else let Constructor{conSrcCon = c} = theDef info in
+             compileCon c ConOSystem es
     Lit l -> compileLiteral l
     Lam v b | usableModality v, getOrigin v == UserWritten -> do
       when (patternInTeleName `isPrefixOf` absName b) $ genericDocError =<< do
@@ -271,7 +276,16 @@ compileTerm v = do
     t -> genericDocError =<< text "bad term:" <?> prettyTCM t
   where
     app :: Hs.Exp () -> Elims -> C (Hs.Exp ())
-    app hd es = eApp <$> pure hd <*> compileElims es
+    app hd es = eApp hd <$> compileElims es
+
+    compileCon :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())
+    compileCon h i es
+      | Just semantics <- isSpecialCon (conName h)
+      = semantics h i es
+    compileCon h i es =
+      isUnboxConstructor (conName h) >>= \case
+        Just _  -> compileErasedApp es
+        Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)
 
 -- `compileErasedApp` compiles an application of an erased constructor
 -- or projection.

src/Agda2Hs/Compile/Type.hs

@@ -4,9 +4,10 @@ module Agda2Hs.Compile.Type where
 
 import Control.Arrow ( (>>>) )
 import Control.Monad ( forM, when )
+import Control.Monad.Trans ( lift )
 import Control.Monad.Reader ( asks )
 import Data.List ( find )
-import Data.Maybe ( mapMaybe )
+import Data.Maybe ( mapMaybe, isJust )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
 import qualified Language.Haskell.Exts.Extension as Hs
@@ -68,45 +69,74 @@ tupleType q es = do
   ts <- mapM compileType xs
   return $ Hs.TyTuple () Hs.Boxed ts
 
-constrainType :: Hs.Asst () -> Hs.Type () -> Hs.Type ()
+-- | Add a class constraint to a Haskell type.
+constrainType
+  :: Hs.Asst () -- ^ The class assertion.
+  -> Hs.Type () -- ^ The type to constrain.
+  -> Hs.Type ()
 constrainType c = \case
   Hs.TyForall _ as (Just (Hs.CxTuple _ cs)) t -> Hs.TyForall () as (Just (Hs.CxTuple () (c:cs))) t
   Hs.TyForall _ as (Just (Hs.CxSingle _ c')) t -> Hs.TyForall () as (Just (Hs.CxTuple () [c,c'])) t
   Hs.TyForall _ as _ t -> Hs.TyForall () as (Just (Hs.CxSingle () c)) t
   t -> Hs.TyForall () Nothing (Just (Hs.CxSingle () c)) t
 
-qualifyType :: String -> Hs.Type () -> Hs.Type ()
+-- | Add explicit quantification over a variable to a Haskell type.
+qualifyType
+  :: String     -- ^ Name of the variable.
+  -> Hs.Type () -- ^ Type to quantify.
+  -> Hs.Type ()
 qualifyType s = \case
     Hs.TyForall _ (Just as) cs t -> Hs.TyForall () (Just (a:as)) cs t
     Hs.TyForall _ Nothing cs t -> Hs.TyForall () (Just [a]) cs t
     t -> Hs.TyForall () (Just [a]) Nothing t
   where
     a = Hs.UnkindedVar () $ Hs.Ident () s
 
--- Compile a top-level type that binds the current module parameters
--- (if any) as explicitly bound type arguments.
--- The continuation is called in an extended context with these type
--- arguments bound.
-compileTopLevelType :: Bool -> Type -> (Hs.Type () -> C a) -> C a
+
+-- | Compile a top-level type, such that:
+--
+--   * erased parameters of the current module are dropped.
+--   * usable hidden type parameters of the current module are explicitely quantified.
+--   * usable instance parameters are added as type constraints.
+--   * usable explicit parameters are forbidden (for now).
+--
+--   The continuation is called in an extended context with these type
+--   arguments bound.
+compileTopLevelType
+    :: Bool
+    -- ^ Whether the generated Haskell type will end up in
+    --   the final output. If so, this functions asks for
+    --   language extension ScopedTypeVariables to be enabled.
+    -> Type
+    -> (Hs.Type () -> C a) -- ^ Continuation with the compiled type.
+    -> C a
 compileTopLevelType keepType t cont = do
     reportSDoc "agda2hs.compile.type" 12 $ text "Compiling top-level type" <+> prettyTCM t
+    -- NOTE(flupe): even though we only quantify variable for definitions inside anonymous modules,
+    --              they will still get quantified over the toplevel module parameters.
+    weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)
     modTel <- moduleParametersToDrop =<< currentModule
-    reportSDoc "agda2hs.compile.type" 19 $ text "Module parameters to drop: " <+> prettyTCM modTel
-    go modTel cont
+    reportSDoc "agda2hs.compile.type" 19 $ text "Module parameters to process: " <+> prettyTCM modTel
+    go weAreOnTop modTel cont
   where
-    go :: Telescope -> (Hs.Type () -> C a) -> C a
-    go EmptyTel cont = do
+    go :: Bool -> Telescope -> (Hs.Type () -> C a) -> C a
+    go _ EmptyTel cont = do
       ctxArgs <- getContextArgs
       ty <- compileType . unEl =<< t `piApplyM` ctxArgs
       cont ty
-    go (ExtendTel a atel) cont
+    go onTop (ExtendTel a atel) cont
+      | not (usableModality a) =
+          underAbstraction a atel $ \tel -> go onTop tel cont
       | isInstance a = do
           c <- Hs.TypeA () <$> compileType (unEl $ unDom a)
           underAbstraction a atel $ \tel ->
-            go tel (cont . constrainType c)
-      | otherwise = underAbstraction a atel $ \tel -> do
-          when keepType $ tellExtension Hs.ScopedTypeVariables
-          go tel (cont . qualifyType (absName atel))
+            go onTop tel (cont . constrainType c)
+      | otherwise = do
+          compileType (unEl $ unDom a)
+          when (keepType && not onTop) $ tellExtension Hs.ScopedTypeVariables
+          let qualifier = if onTop then id else qualifyType (absName atel)
+          underAbstraction a atel $ \tel ->
+            go onTop tel (cont . qualifier)
 
 compileType' :: Term -> C (Strictness, Hs.Type ())
 compileType' t = do
@@ -115,9 +145,12 @@ compileType' t = do
     _        -> return Lazy
   (s,) <$> compileType t
 
+-- | Compile an Agda term into a Haskell type.
 compileType :: Term -> C (Hs.Type ())
 compileType t = do
   reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t
+  reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t
+
   case t of
     Pi a b -> compileDom (absName b) a >>= \case
       DomType _ hsA -> do
@@ -127,24 +160,29 @@ compileType t = do
         hsB <- underAbstraction a b (compileType . unEl)
         return $ constrainType hsA hsB
       DomDropped -> underAbstr a b (compileType . unEl)
-    Def f es
-      | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es
-      | Just args <- allApplyElims es ->
-        ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
-        ifM (isTransparentFunction f) (compileTransparentType args) $ do
-          vs <- compileTypeArgs args
-          f <- compileQName f
-          return $ tApp (Hs.TyCon () f) vs
+    Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do
+      def <- getConstInfo f
+      if | not (usableModality def) ->
+            genericDocError
+              =<< text "Cannot use erased definition" <+> prettyTCM f
+              <+> text "in Haskell type"
+         | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es
+         | Just args <- allApplyElims es ->
+             ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
+             ifM (isTransparentFunction f) (compileTransparentType args) $ do
+               vs <- compileTypeArgs args
+               f <- compileQName f
+               return $ tApp (Hs.TyCon () f) vs
+         | otherwise -> fail
     Var x es | Just args <- allApplyElims es -> do
-      unlessM (usableModality <$> lookupBV x) $ genericDocError =<<
-        text "Not supported by agda2hs: erased type variable" <+> prettyTCM (var x)
       vs <- compileTypeArgs args
       x  <- hsName <$> compileVar x
       return $ tApp (Hs.TyVar () x) vs
     Sort s -> return (Hs.TyStar ())
     Lam argInfo restAbs
-      | not (keepArg argInfo)   -> underAbstraction_ restAbs compileType
-    _ -> genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t
+      | not (keepArg argInfo) -> underAbstraction_ restAbs compileType
+    _ -> fail
+  where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t
 
 compileTypeArgs :: Args -> C [Hs.Type ()]
 compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args
@@ -159,7 +197,7 @@ compileUnboxType r pars = do
 
 compileTransparentType :: Args -> C (Hs.Type ())
 compileTransparentType args = compileTypeArgs args >>= \case
-  [] -> genericError "Not supported: underapplied type synonyms"
+  []     -> __IMPOSSIBLE__
   (v:vs) -> return $ v `tApp` vs
 
 compileDom :: ArgName -> Dom Type -> C CompiledDom

test/AllTests.agda

@@ -60,6 +60,8 @@ import IOInput
 import Issue200
 import Issue169
 import Issue210
+import ModuleParameters
+import ModuleParametersImports
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -120,4 +122,6 @@ import IOInput
 import Issue200
 import Issue169
 import Issue210
+import ModuleParameters
+import ModuleParametersImports
 #-}

test/Fail/Issue223.agda

@@ -0,0 +1,8 @@
+module Fail.Issue223 where
+
+data Void : Set where
+{-# COMPILE AGDA2HS Void #-}
+
+test : {a : Set} → Void → a
+test ()
+{-# COMPILE AGDA2HS test #-}

test/ModuleParameters.agda

@@ -0,0 +1,33 @@
+open import Haskell.Prelude hiding (a)
+
+module ModuleParameters
+  (@0 name : Set)
+  (p : @0 name → Set) where
+
+data Scope : Set where
+  Empty : Scope
+  Bind  : (@0 x : name) → p x → Scope → Scope
+{-# COMPILE AGDA2HS Scope #-}
+
+unbind : Scope → Scope
+unbind Empty = Empty
+unbind (Bind _ _ s) = s
+{-# COMPILE AGDA2HS unbind #-}
+
+module _ {a : Set} where
+  thing : a → a
+  thing x = y
+    where y : a
+          y = x
+  {-# COMPILE AGDA2HS thing #-}
+
+  stuff : a → Scope → a
+  stuff x Empty = x
+  stuff x (Bind _ _ _) = x
+  {-# COMPILE AGDA2HS stuff #-}
+
+  module _ {b : Set} where
+    more : b → a → Scope → Scope
+    more _ _ Empty = Empty
+    more _ _ (Bind _ _ s) = s
+    {-# COMPILE AGDA2HS more #-}

test/ModuleParametersImports.agda

@@ -0,0 +1,10 @@
+module ModuleParametersImports where
+
+open import Haskell.Prelude
+open import ModuleParameters Bool (λ _ → Nat)
+
+scope : Scope
+scope = unbind (Bind True 3 (Bind False 2 Empty))
+{-# COMPILE AGDA2HS scope #-}
+
+