From c28556d0aa2e1b9b67bb55f5309e810eba76716d Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Sat, 7 Sep 2024 16:56:02 +0200
Subject: [PATCH] [ fix #357 ] Check that type arguments are valid Haskell
 types before dropping them

---
 src/Agda2Hs/Compile/Term.hs |  7 ++++++-
 test/AllFailTests.agda      |  2 ++
 test/Fail/Issue357a.agda    | 12 ++++++++++++
 test/Fail/Issue357b.agda    | 16 ++++++++++++++++
 test/golden/Issue357a.err   |  2 ++
 test/golden/Issue357b.err   |  2 ++
 6 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 test/Fail/Issue357a.agda
 create mode 100644 test/Fail/Issue357b.agda
 create mode 100644 test/golden/Issue357a.err
 create mode 100644 test/golden/Issue357b.err

diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index e283d574..88c2d0bb 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/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"
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
index 55dbb733..41173e28 100644
--- a/test/AllFailTests.agda
+++ b/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
diff --git a/test/Fail/Issue357a.agda b/test/Fail/Issue357a.agda
new file mode 100644
index 00000000..9737fb30
--- /dev/null
+++ b/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 #-}
diff --git a/test/Fail/Issue357b.agda b/test/Fail/Issue357b.agda
new file mode 100644
index 00000000..8b132705
--- /dev/null
+++ b/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 #-}
diff --git a/test/golden/Issue357a.err b/test/golden/Issue357a.err
new file mode 100644
index 00000000..eb7dfc0d
--- /dev/null
+++ b/test/golden/Issue357a.err
@@ -0,0 +1,2 @@
+test/Fail/Issue357a.agda:10,1-6
+Bad Haskell type: Level
diff --git a/test/golden/Issue357b.err b/test/golden/Issue357b.err
new file mode 100644
index 00000000..8a7dac2a
--- /dev/null
+++ b/test/golden/Issue357b.err
@@ -0,0 +1,2 @@
+test/Fail/Issue357b.agda:10,1-2
+Bad Haskell type: Level