Fix for #357

lib/Haskell/Control/Monad.agda

@@ -4,7 +4,8 @@ open import Haskell.Prim
 open import Haskell.Prim.Bool
 open import Haskell.Prim.Monad
 open import Haskell.Prim.String
+open import Haskell.Extra.Erase
 
-guard : {{ MonadFail m }} → (b : Bool) → m (b ≡ True)
-guard True = return refl
+guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True))
+guard True = return (Erased refl)
 guard False = fail "Guard was not True"

lib/Haskell/Extra/Erase.agda

@@ -14,11 +14,13 @@ module Haskell.Extra.Erase where
     @0 xs  : List a
 
   record Erase (@0 a : Set ℓ) : Set ℓ where
-    constructor Erased
-    field @0 get : a
+    instance constructor iErased
+    field @0 {{get}} : a
   open Erase public
   {-# COMPILE AGDA2HS Erase tuple #-}
 
+  pattern Erased x = iErased {{x}}
+
   infixr 4 ⟨_⟩_
   record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where
     constructor ⟨_⟩_

src/Agda2Hs/Compile.hs

@@ -39,6 +39,7 @@ initCompileEnv tlm rewrites = CompileEnv
   , compilingLocal    = False
   , copatternsEnabled = False
   , rewrites          = rewrites
+  , writeImports      = True
   }
 
 initCompileState :: CompileState

src/Agda2Hs/Compile/Name.hs

@@ -34,6 +34,7 @@ import Agda.TypeChecking.Records ( isRecordConstructor )
 
 import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
+import Agda.Utils.Monad ( whenM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Types
@@ -121,7 +122,8 @@ compileQName f
       qf = qualify mod' hf qual
 
     -- add (possibly qualified) import
-    whenJust (mimpBuiltin <|> mimp) tellImport
+    whenM (asks writeImports) $
+      whenJust (mimpBuiltin <|> mimp) tellImport
 
     reportSDoc "agda2hs.name" 25 $ text
        $ "-------------------------------------------------"

src/Agda2Hs/Compile/Term.hs

@@ -591,9 +591,14 @@ compileArgs' ty (x:xs) = do
   compileDom a >>= \case
     DODropped  -> rest
     DOInstance -> checkInstance x *> rest
-    DOType     -> rest
+    DOType     -> checkValidType x *> rest
     DOTerm     -> second . (:) <$> compileTerm (unDom a) x <*> rest
 
+-- We check that type arguments compile to a valid Haskell type
+-- before dropping them, see issue #357.
+checkValidType :: Term -> C ()
+checkValidType x = noWriteImports (compileType x) *> return ()
+
 clauseToAlt :: Hs.Match () -> C (Hs.Alt ())
 clauseToAlt (Hs.Match _ _ [p] rhs wh) = pure $ Hs.Alt () p rhs wh
 clauseToAlt (Hs.Match _ _ ps _ _)     = genericError "Pattern matching lambdas must take a single argument"

src/Agda2Hs/Compile/Type.hs

@@ -22,14 +22,14 @@ import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep )
+import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep, instantiate )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.List ( downFrom )
 import Agda.Utils.Maybe ( ifJustM, fromMaybe )
-import Agda.Utils.Monad ( ifM, unlessM, and2M, or2M )
+import Agda.Utils.Monad ( ifM, whenM, unlessM, and2M, or2M )
 import Agda.Utils.Size ( Sized(size) )
 import Agda.Utils.Functor ( ($>) )
 
@@ -89,7 +89,9 @@ 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
+  whenM (isErasedBaseType t) fail
+
+  instantiate t >>= \case
     Pi a b -> do
       let compileB = underAbstraction a b (compileType . unEl)
       compileDomType (absName b) a >>= \case
@@ -126,12 +128,21 @@ compileType t = do
 
     Sort s -> return (Hs.TyStar ())
 
-    -- TODO: we should also drop lambdas that can be erased based on their type
-    -- (e.g. argument is of type Level/Size or in a Prop) but currently we do
-    -- not have access to the type of the lambda here.
-    Lam argInfo restAbs
-      | hasQuantity0 argInfo -> underAbstraction_ restAbs compileType
-      | otherwise -> genericDocError =<< text "Not supported: type-level lambda" <+> prettyTCM t
+    Lam argInfo restAbs -> do
+      (body , x0) <- underAbstraction_ restAbs $ \b ->
+        (,) <$> compileType b <*> (hsName <$> compileDBVar 0)
+
+      -- TODO: we should also drop lambdas that can be erased based on their type
+      -- (e.g. argument is of type Level/Size or in a Prop) but currently we do
+      -- not have access to the type of the lambda here.
+      if | hasQuantity0 argInfo -> return body
+         -- Rewrite `\x -> (a -> x)` to `(->) a`
+         | Hs.TyFun _ a (Hs.TyVar _ y) <- body
+         , y == x0 -> return $ Hs.TyApp () (Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()) a
+         -- Rewrite `\x -> ((->) x)` to `(->)`
+         | Hs.TyApp _ (Hs.TyCon _ (Hs.Special _ (Hs.FunCon _))) (Hs.TyVar _ y) <- body
+         , y == x0 -> return $ Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()
+         | otherwise -> genericDocError =<< text "Not supported: type-level lambda" <+> prettyTCM t
 
     _ -> fail
   where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t

src/Agda2Hs/Compile/Types.hs

@@ -86,6 +86,8 @@ data CompileEnv = CompileEnv
   -- ^ whether copatterns should be allowed when compiling patterns
   , rewrites :: SpecialRules
   -- ^ Special compilation rules.
+  , writeImports :: Bool
+  -- ^ whether we should add imports of compiled names
   }
 
 type Qualifier = Maybe (Maybe (Hs.ModuleName ()))

src/Agda2Hs/Compile/Utils.hs

@@ -141,11 +141,17 @@ canErase :: Type -> C Bool
 canErase a = do
   TelV tel b <- telView a
   addContext tel $ orM
-    [ isLevelType b                       -- Level
-    , isJust <$> isSizeType b             -- Size
-    , isPropSort (getSort b)              -- _ : Prop
+    [ isErasedBaseType (unEl b)
+    , isPropSort (getSort b)            -- _ : Prop
     ]
 
+isErasedBaseType :: Term -> C Bool
+isErasedBaseType x = orM
+  [ isLevelType b                       -- Level
+  , isJust <$> isSizeType b             -- Size
+  ]
+  where b = El __DUMMY_SORT__ x
+
 -- 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
@@ -374,3 +380,6 @@ checkNoAsPatterns = \case
     checkPatternInfo :: PatternInfo -> C ()
     checkPatternInfo i = unless (null $ patAsNames i) $
       genericDocError =<< text "not supported by agda2hs: as patterns"
+
+noWriteImports :: C a -> C a
+noWriteImports = local $ \e -> e { writeImports = False }

test/AllFailTests.agda

@@ -37,3 +37,5 @@ import Fail.NonCanonicalSpecialFunction
 import Fail.TypeLambda
 import Fail.NonCanonicalSuperclass
 import Fail.Issue125
+import Fail.Issue357a
+import Fail.Issue357b

test/AllTests.agda

@@ -88,6 +88,7 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -173,4 +174,5 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 #-}

test/Fail/Issue357a.agda

@@ -0,0 +1,12 @@
+open import Haskell.Prelude
+open import Agda.Primitive
+
+module Fail.Issue357a where
+
+k : a → b → a
+k x _ = x
+{-# COMPILE AGDA2HS k #-}
+
+testK : Nat
+testK = k 42 lzero
+{-# COMPILE AGDA2HS testK #-}

test/Fail/Issue357b.agda

@@ -0,0 +1,16 @@
+open import Haskell.Prelude
+open import Agda.Primitive
+
+module Fail.Issue357b where
+
+k : a → b → a
+k x _ = x
+{-# COMPILE AGDA2HS k #-}
+
+l : Level → Nat
+l = k 42
+{-# COMPILE AGDA2HS l #-}
+
+testK : Nat
+testK = l lzero
+{-# COMPILE AGDA2HS testK #-}

test/FunCon.agda

@@ -0,0 +1,22 @@
+
+open import Haskell.Prelude
+
+data D1 (t : Set → Set) : Set where
+  C1 : t Bool → D1 t
+
+{-# COMPILE AGDA2HS D1 #-}
+
+f1 : D1 (λ a → Int → a)
+f1 = C1 (_== 0)
+
+{-# COMPILE AGDA2HS f1 #-}
+
+data D2 (t : Set → Set → Set) : Set where
+  C2 : t Int Int → D2 t
+
+{-# COMPILE AGDA2HS D2 #-}
+
+f2 : D2 (λ a b → a → b)
+f2 = C2 (_+ 1)
+
+{-# COMPILE AGDA2HS f2 #-}

test/golden/AllTests.hs

@@ -83,4 +83,5 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 

test/golden/FunCon.hs

@@ -0,0 +1,12 @@
+module FunCon where
+
+data D1 t = C1 (t Bool)
+
+f1 :: D1 ((->) Int)
+f1 = C1 (== 0)
+
+data D2 t = C2 (t Int Int)
+
+f2 :: D2 (->)
+f2 = C2 (+ 1)
+

test/golden/Issue357a.err

@@ -0,0 +1,2 @@
+test/Fail/Issue357a.agda:10,1-6
+Bad Haskell type: Level

test/golden/Issue357b.err

@@ -0,0 +1,2 @@
+test/Fail/Issue357b.agda:10,1-2
+Bad Haskell type: Level