[ fix #357 ] Check that type arguments are valid Haskell types before…

… dropping them

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"

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/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/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