diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index b3251c1d..71e566b6 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -125,8 +125,12 @@ compileType t = do
 
     Sort s -> return (Hs.TyStar ())
 
-    -- This case is only reachable for erased lambdas
-    Lam argInfo restAbs -> underAbstraction_ restAbs compileType
+    -- 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
 
     _ -> fail
   where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t
diff --git a/test/Fail/TypeLambda.agda b/test/Fail/TypeLambda.agda
new file mode 100644
index 00000000..de530cc4
--- /dev/null
+++ b/test/Fail/TypeLambda.agda
@@ -0,0 +1,9 @@
+
+module Fail.TypeLambda where
+
+open import Haskell.Prelude
+
+foo : (f : (Set → Set) → Set) (x : f (λ y → Nat)) (y : f List) → Nat
+foo f x y = 42
+
+{-# COMPILE AGDA2HS foo #-}
diff --git a/test/golden/TypeLambda.err b/test/golden/TypeLambda.err
new file mode 100644
index 00000000..3ccb3eab
--- /dev/null
+++ b/test/golden/TypeLambda.err
@@ -0,0 +1,2 @@
+test/Fail/TypeLambda.agda:6,1-4
+Not supported: type-level lambda λ y → Nat