allow erased module arguments

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

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,6 +145,7 @@ 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
@@ -127,24 +158,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 -> 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 +195,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,7 @@ import IOInput
 import Issue200
 import Issue169
 import Issue210
+import ModuleParameters
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -120,4 +121,5 @@ import IOInput
 import Issue200
 import Issue169
 import Issue210
+import ModuleParameters
 #-}

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/ScopedTypeVariables.agda

@@ -1,7 +1,7 @@
-module ScopedTypeVariables where
-
 open import Haskell.Prelude
 
+module ScopedTypeVariables (@0 x : Bool) where
+
 -- We can encode explicit `forall` quantification by module parameters in Agda.
 module _ {a : Set} {{_ : Eq a}} where
   foo : a → Bool
@@ -19,3 +19,11 @@ module _ {a b : Set} where
       baz : b → b
       baz z = f (f z)
 {-# COMPILE AGDA2HS bar #-}
+
+data D : Set where
+  MakeD : (y : Bool) → @0 x ≡ y → D
+{-# COMPILE AGDA2HS D #-}
+
+mybool : Bool
+mybool = False
+{-# COMPILE AGDA2HS mybool #-}

test/golden/AllTests.hs

@@ -58,4 +58,5 @@ import IOInput
 import Issue200
 import Issue169
 import Issue210
+import ModuleParameters
 

test/golden/ErasedRecordParameter.err

@@ -1,2 +1,2 @@
 test/Fail/ErasedRecordParameter.agda:4,8-10
-Not supported by agda2hs: erased type variable a
+Cannot use erased variable a

test/golden/Issue223.err

@@ -0,0 +1,2 @@
+test/Fail/Issue223.agda:6,1-5
+Functions defined with absurd patterns exclusively are not supported. Use function `error` from the Haskell.Prelude instead.

test/golden/ModuleParameters.hs

@@ -0,0 +1,24 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module ModuleParameters where
+
+data Scope p = Empty
+             | Bind p (Scope p)
+
+unbind :: Scope p -> Scope p
+unbind Empty = Empty
+unbind (Bind _ s) = s
+
+thing :: forall p a . a -> a
+thing x = y
+  where
+    y :: a
+    y = x
+
+stuff :: forall p a . a -> Scope p -> a
+stuff x Empty = x
+stuff x (Bind _ _) = x
+
+more :: forall p a b . b -> a -> Scope p -> Scope p
+more _ _ Empty = Empty
+more _ _ (Bind _ s) = s
+

test/golden/ScopedTypeVariables.hs

@@ -13,3 +13,8 @@ bar x y f = baz y
     baz :: b -> b
     baz z = f (f z)
 
+data D = MakeD Bool
+
+mybool :: Bool
+mybool = False
+