diff --git a/src/Agda2Hs/AgdaUtils.hs b/src/Agda2Hs/AgdaUtils.hs
index 431568ae..87347107 100644
--- a/src/Agda2Hs/AgdaUtils.hs
+++ b/src/Agda2Hs/AgdaUtils.hs
@@ -20,7 +20,9 @@ import Agda.Syntax.TopLevelModuleName
 
 import Agda.TypeChecking.Monad ( topLevelModuleName )
 import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Sort
 import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Reduce ( reduceDefCopy )
 
 import Agda.Utils.Either ( isRight )
@@ -136,3 +138,8 @@ isForcedPat = \case
   ProjP{}       -> False
   IApplyP{}     -> False
   DefP{}        -> False
+
+endsInSort :: (PureTCM m, MonadBlock m) => Type -> m Bool
+endsInSort t = do
+  TelV tel b <- telView t
+  addContext tel $ ifIsSort b (\_ -> return True) (return False)
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index 7039d62c..9731f6df 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -34,8 +34,8 @@ initCompileEnv tlm rewrites = CompileEnv
   { currModule        = tlm
   , minRecordName     = Nothing
   , locals            = []
+  , compilingLocal    = False
   , copatternsEnabled = False
-  , checkVar          = False
   , rewrites          = rewrites
   }
 
@@ -85,7 +85,7 @@ compile opts tlm _ def =
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
         (ExistingClassPragma , _         ) -> return []
-        (UnboxPragma s       , defn      ) -> [] <$ checkUnboxPragma defn
+        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
 
diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 44cecd84..34ce73de 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -30,6 +30,7 @@ import Agda.TypeChecking.Records
 import Agda.TypeChecking.Telescope ( mustBePi )
 
 import Agda.Utils.Lens
+import Agda.Utils.Monad ( ifNotM )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
 import Agda2Hs.AgdaUtils
@@ -84,7 +85,8 @@ compileInstance ToDefinition def@Defn{..} =
 compileInstRule :: [Hs.Asst ()] -> Term -> C (Hs.InstRule ())
 compileInstRule cs ty = case unSpine1 ty of
   Def f es | Just args <- allApplyElims es -> do
-    vs <- mapM (compileType . unArg) $ filter keepArg args
+    fty <- defType <$> getConstInfo f
+    vs <- compileTypeArgs fty args
     f <- compileQName f
     return $
       Hs.IRule () Nothing (ctx cs) $ foldl (Hs.IHApp ()) (Hs.IHCon () f) (map pars vs)
@@ -100,6 +102,7 @@ compileInstRule cs ty = case unSpine1 ty of
     DomConstraint hsA ->
       underAbstraction a b (compileInstRule (cs ++ [hsA]) . unEl)
     DomType _ t -> __IMPOSSIBLE__
+    DomForall _ -> __IMPOSSIBLE__
   _ -> __IMPOSSIBLE__
 
 
@@ -131,7 +134,8 @@ etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do
 
 
 compileInstanceClause :: ModuleName -> Type -> Clause -> C ([Hs.InstDecl ()], [QName])
-compileInstanceClause curModule ty c = do
+compileInstanceClause curModule ty c = ifNotM (keepClause c) (return ([], [])) $ do
+
   let naps = namedClausePats c
 
   -- there are no projection patterns: we need to eta-expand the clause
@@ -162,7 +166,11 @@ compileInstanceClause' curModule ty (p:ps) c
 
     -- retrieve the type of the projection
     Just (unEl -> Pi a b) <- getDefType q ty
-    let ty' = absBody b
+    -- We don't really have the information available to reconstruct the instance
+    -- head. However, all dependencies on the instance head are in erased positions, 
+    -- so we can just use a dummy term instead
+    let instanceHead = __DUMMY_TERM__ 
+        ty' = b `absApp` instanceHead
 
     reportSDoc "agda2hs.compile.instance" 15 $
       text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q [])
@@ -193,14 +201,15 @@ compileInstanceClause' curModule ty (p:ps) c
           _ -> return d
 
     if
-      | isInstance arg, usableModality arg -> do
+      -- Instance field: check canonicity.
+      | isInstance arg -> do
           unless (null ps) $ genericDocError =<< text "not allowed: explicitly giving superclass"
           body <- case clauseBody c' of
             Nothing -> genericDocError =<< text "not allowed: absurd clause for superclass"
             Just b  -> return b
           checkInstance body
           return ([], [])
-      | not (keepArg arg) -> return ([], [])
+
       -- Projection of a primitive field: chase down definition and inline as instance clause.
       | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
       , [(_, f)] <- mapMaybe isProjElim es
@@ -210,7 +219,7 @@ compileInstanceClause' curModule ty (p:ps) c
         reportSDoc "agda2hs.compile.instance" 20 $
           text $ "raw projection:" ++ prettyShow (Def n [])
         d <- chaseDef n
-        fc <- compileFun False d
+        fc <- compileLocal $ compileFun False d
         let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d
         let fc' = {- dropPatterns 1 $ -} replaceName hd uf fc
         return (map (Hs.InsDecl ()) fc', [n])
@@ -219,7 +228,21 @@ compileInstanceClause' curModule ty (p:ps) c
        -- same (minimal) dictionary as the primitive fields.
       | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
       , n .~ q -> do
-        case map unArg . filter keepArg <$> allApplyElims es of
+        let err = genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+            filterArgs :: Type -> [Term] -> C [Term]
+            filterArgs ty [] = return []
+            filterArgs ty (v:vs) = do
+              reportSDoc "agda2hs.compile.instance" 25 $ text "filterArgs: v =" <+> prettyTCM v
+              (a,b) <- mustBePi ty
+              reportSDoc "agda2hs.compile.instance" 25 $ text "filterArgs: a =" <+> prettyTCM a
+              let rest = underAbstraction a b $ \b' -> filterArgs b' vs
+              compileDom a >>= \case
+                DODropped -> rest
+                DOType -> rest
+                DOTerm -> (v:) <$> rest
+                DOInstance -> err
+        ty <- defType <$> getConstInfo n
+        traverse (filterArgs ty) (map unArg <$> allApplyElims es) >>= \case
           Just [ Def f _ ] -> do
             reportSDoc "agda2hs.compile.instance" 20 $ vcat
                 [ text "Dropping default instance clause" <+> prettyTCM c'
@@ -228,8 +251,7 @@ compileInstanceClause' curModule ty (p:ps) c
             reportSDoc "agda2hs.compile.instance" 40 $
                 text $ "raw dictionary:" ++ prettyShow f
             return ([], [f])
-
-          _ -> genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+          _ -> err
 
       -- No minimal dictionary used, proceed with compiling as a regular clause.
       | otherwise -> do
diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs
index 3dae6ee5..d205102d 100644
--- a/src/Agda2Hs/Compile/Data.hs
+++ b/src/Agda2Hs/Compile/Data.hs
@@ -52,10 +52,11 @@ compileData newtyp ds def = do
         DomDropped      -> allIndicesErased (unAbs t)
         DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
         DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
+        DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
       _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
-compileConstructor params c = checkingVars $ do
+compileConstructor params c = do
   reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c
   reportSDoc "agda2hs.data.con" 20 $ text "  params = " <+> prettyTCM params
   ty <- (`piApplyM` params) . defType =<< getConstInfo c
@@ -74,3 +75,4 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
     (ty :) <$> underAbstraction a tel compileConstructorArgs
   DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
+  DomForall{}       -> __IMPOSSIBLE__
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index e4c5e941..52a7a727 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -2,15 +2,14 @@
 module Agda2Hs.Compile.Function where
 
 import Control.Monad ( (>=>), filterM, forM_ )
-import Control.Monad.Reader ( asks )
+import Control.Monad.Reader ( asks, local )
 
 import Data.Generics
 import Data.List
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Build as Hs
+import qualified Language.Haskell.Exts as Hs
 
 import Agda.Compiler.Backend
 import Agda.Compiler.Common
@@ -41,7 +40,7 @@ import Agda.Utils.Size ( Sized(size) )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 import Agda2Hs.Compile.Term ( compileTerm, usableDom )
-import Agda2Hs.Compile.Type ( compileTopLevelType, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -116,50 +115,50 @@ compileFun withSig def@Defn{..} =
     $ compileFun' withSig def
 
 -- inherit existing (instantiated) locals
-compileFun' withSig def@Defn{..} = do
+compileFun' withSig def@Defn{..} = inTopContext $ do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 
   whenM ((withSig &&) <$> inRecordMod defName) $
     genericDocError =<< text "not supported by agda2hs: functions inside a record module"
 
-  withCurrentModule m $ do
+  -- We add the module parameters to the context
+  -- if we are compiling a local function (e.g. a where declaration or pattern-matching lambda)
+  isLocalFun <- asks compilingLocal
+  tel <- if isLocalFun then lookupSection m else return EmptyTel
+
+  withCurrentModule m $ addContext tel $ 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
+          
+      pars <- getContextArgs
+      reportSDoc "agda2hs.compile.type" 8 $ "Function module parameters: " <+> prettyTCM pars
 
-      when withSig $ checkValidFunName x
-
-      compileTopLevelType withSig defType $ \ty -> do
-
-        let filtered = filter keepClause funClauses
-        weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)
-        pars <- getContextArgs
+      reportSDoc "agda2hs.compile.type" 8 $ "Function type (before instantiation): " <+> inTopContext (prettyTCM defType)
+      typ <- piApplyM defType pars
+      reportSDoc "agda2hs.compile.type" 8 $ "Function type (after instantiation): " <+> prettyTCM typ 
 
-        -- 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" 8 $ "Applying module parameters to clauses: " <+> prettyTCM pars
-        let clauses = if weAreOnTop then filtered else filtered `apply` pars
+      sig <- if not withSig then return [] else do
+        checkValidFunName x
+        ty <- compileType $ unEl typ
+        reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty) 
+        return [Hs.TypeSig () [x] ty]
 
-        typ <- if weAreOnTop then pure defType else piApplyM defType pars
+      let clauses = funClauses `apply` pars
+      cs  <- mapMaybeM (compileClause m (Just defName) x typ) clauses
 
-        cs  <- mapMaybeM (compileClause m (Just defName) x typ) clauses
+      when (null cs) $ genericDocError
+        =<< text "Functions defined with absurd patterns exclusively are not supported."
+        <+> text "Use function `error` from the Haskell.Prelude instead."
 
-        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]
+      return $ sig ++ [Hs.FunBind () cs]
   where
     Function{..} = theDef
     m = qnameModule defName
     n = qnameName defName
     x = hsName $ prettyShow n
-    endsInSort t = do
-      TelV tel b <- telView t
-      addContext tel $ ifIsSort b (\_ -> return True) (return False)
     err = "Not supported: type definition with `where` clauses"
 
 
@@ -169,16 +168,15 @@ compileClause curModule mproj x t c =
     compileClause' curModule mproj x t c
 
 compileClause' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause' curModule projName x _  c@Clause{clauseBody = Nothing} = pure Nothing
 compileClause' curModule projName x ty c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7  $ "compiling clause: " <+> prettyTCM c
-  reportSDoc "agda2hs.compile" 17 $ "Old context: "      <+> (prettyTCM =<< getContext)
-  reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> prettyTCM clauseTel
-  reportSDoc "agda2hs.compile" 17 $ "Clause type:      " <+> prettyTCM clauseType
-  reportSDoc "agda2hs.compile" 17 $ "Function type:    " <+> prettyTCM ty
-  reportSDoc "agda2hs.compile" 17 $ "Clause patterns:  " <+> text (prettyShow namedClausePats)
 
-  addContext (KeepNames clauseTel) $ do
+  ifNotM (keepClause c) (pure Nothing) $ addContext (KeepNames clauseTel) $ do
+    reportSDoc "agda2hs.compile" 17 $ "Old context: "      <+> (inTopContext . prettyTCM =<< getContext)
+    reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> inTopContext (prettyTCM clauseTel)
+    reportSDoc "agda2hs.compile" 17 $ "Clause type:      " <+> prettyTCM clauseType
+    reportSDoc "agda2hs.compile" 17 $ "Function type:    " <+> prettyTCM ty
+    reportSDoc "agda2hs.compile" 17 $ "Clause patterns:  " <+> text (prettyShow namedClausePats)
 
     toDrop <- case projName of
       Nothing -> pure 0
@@ -198,7 +196,7 @@ compileClause' curModule projName x ty c@Clause{..} = do
           /\ (curModule `isFatherModuleOf`) . qnameModule
 
     children   <- filter isWhereDecl <$> asks locals
-    whereDecls <- mapM (getConstInfo >=> compileFun' True) children
+    whereDecls <- compileLocal $ mapM (getConstInfo >=> compileFun' True) children
 
     -- Jesper, 2023-10-30: We should compile the body in the module of the
     -- `where` declarations (if there are any) in order to drop the arguments
@@ -221,6 +219,16 @@ compileClause' curModule projName x ty c@Clause{..} = do
           _                         -> Hs.Match () x ps rhs whereBinds
     return $ Just match
 
+keepClause :: Clause -> C Bool
+keepClause c@Clause{..} = case (clauseBody, clauseType) of
+  (Nothing, _) -> pure False
+  (_, Nothing) -> pure False
+  (Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
+    DODropped  -> False
+    DOInstance -> False -- not __IMPOSSIBLE__ because of current hacky implementation of `compileInstanceClause`
+    DOType     -> __IMPOSSIBLE__
+    DOTerm     -> True
+
 
 -- TODO(flupe): projection-like definitions are missing the first (variable) patterns
 --             (that are however present in the type)
@@ -241,11 +249,12 @@ compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
+  when (usableDom a) checkForced
   compileDom a >>= \case
     DOInstance -> rest
-    DODropped  -> rest <* when (usableDom a) checkForced
-    DOKept     -> do
-      checkForced
+    DODropped  -> rest
+    DOType     -> rest
+    DOTerm     -> do
       checkNoAsPatterns pat
       (:) <$> compilePat (unDom a) pat <*> rest
   where checkForced  = when (isForcedPat pat) $ genericDocError =<< "not supported by agda2hs: forced (dot) patterns in non-erased positions"
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index 70f6a4a5..d85ac11e 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -16,16 +16,17 @@ import Agda.Syntax.Common ( Arg(unArg), defaultArg )
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
-import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat )
+import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM )
 import Agda.TypeChecking.Substitute ( TelV(TelV), Apply(apply) )
 import Agda.TypeChecking.Telescope
 
+import Agda.Utils.Singleton
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.ClassInstance
 import Agda2Hs.Compile.Function ( compileFun )
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
@@ -47,7 +48,7 @@ compileMinRecord fieldNames m = do
   -- We can't simply compileFun here for two reasons:
   -- * it has an explicit dictionary argument
   -- * it's using the fields and definitions from the minimal record and not the parent record
-  compiled <- withMinRecord m $ addContext (defaultDom rtype) $
+  compiled <- withMinRecord m $ addContext (defaultDom rtype) $ compileLocal $
     fmap concat $ traverse (compileFun False) defaults
   let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]
   return (definedFields, declMap)
@@ -92,7 +93,7 @@ compileMinRecords def sls = do
 compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ())
 compileRecord target def = do
   TelV tel _ <- telViewUpTo recPars (defType def)
-  addContext tel $ checkingVars $ do
+  addContext tel $ do
     checkValidTypeName rName
     binds <- compileTeleBinds tel
     let hd = foldl (Hs.DHApp ()) (Hs.DHead () rName) binds
@@ -153,6 +154,7 @@ compileRecord target def = do
             ToRecord{} -> genericError $
               "Not supported: record/class with constraint fields"
           DomDropped -> return (hsAssts , hsFields)
+          DomForall{} -> __IMPOSSIBLE__
       (_, _) -> __IMPOSSIBLE__
 
     compileDataRecord
@@ -168,16 +170,30 @@ compileRecord target def = do
       let conDecl = Hs.QualConDecl () Nothing Nothing $ Hs.RecDecl () cName fieldDecls
       return $ Hs.DataDecl () don Nothing hd [conDecl] ds
 
+checkUnboxPragma :: Definition -> C ()
+checkUnboxPragma def = do
+  let Record{..} = theDef def
 
--- | Check if record can be defined as unboxed.
-checkUnboxPragma :: Defn -> C ()
-checkUnboxPragma def
-  | Record{recFields, recMutual} <- def
-  , length (filter keepArg recFields) == 1
-  -- , not (recRecursive def)
-  --     can be used again after agda 2.6.4.2 is released
-  --     see: agda/agda#7042
-  , all null recMutual -- see agda/agda#7042
-  = return ()
-  | otherwise
-  = genericError "An unboxed type must be a non-recursive record type with exactly one non-erased field."
+  -- recRecursive can be used again after agda 2.6.4.2 is released
+  -- see agda/agda#7042
+  unless (all null recMutual) $ genericDocError
+    =<< text "Unboxed record" <+> prettyTCM (defName def) 
+    <+> text "cannot be recursive"
+
+  TelV tel _ <- telViewUpTo recPars (defType def)
+  addContext tel $ do
+    pars <- getContextArgs
+    let fieldTel = recTel `apply` pars
+    fields <- nonErasedFields fieldTel
+    unless (length fields == 1) $ genericDocError
+      =<< text "Unboxed record" <+> prettyTCM (defName def)
+      <+> text "should have exactly one non-erased field"
+
+  where
+    nonErasedFields :: Telescope -> C [String]
+    nonErasedFields EmptyTel = return []
+    nonErasedFields (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel nonErasedFields
+      DOType -> genericDocError =<< text "Type field in unboxed record not supported"
+      DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
+      DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 19e19ef3..f8bc3540 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -62,7 +62,7 @@ isSpecialDef q = case prettyShow q of
 
 -- | Compile a @\where@ to the equivalent @\case@ expression.
 lambdaCase :: QName -> DefCompileRule
-lambdaCase q ty args = setCurrentRangeQ q $ do
+lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
   Function
     { funClauses = cls
     , funExtLam  = Just ExtLamInfo {extLamModule = mname}
@@ -125,7 +125,6 @@ primWord64FromNat ty args = compileArgs ty args >>= \case
   _ -> genericError "primWord64FromNat must be applied to a literal"
 
 
--- should really be named compileVar, TODO: rename compileVar
 compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
 compileVar i ty es = do
   reportSDoc "agda2hs.compile.term" 15 $ text "Reached variable"
@@ -145,7 +144,6 @@ compileSpined c tm ty (e@(Proj o q):es) = do
   let t = tm []
   ty' <- shouldBeProjectible t ty o q
   compileSpined (compileProj q ty t ty') (tm . (e:)) ty' es
--- TODO: use mustBePi
 compileSpined c tm ty (e@(Apply (unArg -> x)):es) = do
   (a, b) <- mustBePi ty
   compileSpined (c . (x:)) (tm . (e:)) (absApp b x) es
@@ -525,7 +523,8 @@ compileArgs ty (x:xs) = do
   compileDom a >>= \case
     DODropped  -> rest
     DOInstance -> checkInstance x *> rest
-    DOKept     -> (:) <$> compileTerm (unDom a) x
+    DOType     -> rest
+    DOTerm     -> (:) <$> compileTerm (unDom a) x
                       <*> rest
 
 clauseToAlt :: Hs.Match () -> C (Hs.Alt ())
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 123f63f8..71e566b6 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -4,7 +4,7 @@
 module Agda2Hs.Compile.Type where
 
 import Control.Arrow ( (>>>) )
-import Control.Monad ( forM, when )
+import Control.Monad ( forM, when, unless )
 import Control.Monad.Trans ( lift )
 import Control.Monad.Reader ( asks )
 import Data.List ( find )
@@ -72,53 +72,6 @@ delayType (_       : _) = __IMPOSSIBLE__
 delayType [] = genericDocError =<< text "Cannot compile unapplied Delay type"
 
 
-{- | 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" 8 $ 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 process: " <+> prettyTCM modTel
-    go weAreOnTop modTel cont
-  where
-    go :: Bool -> Telescope -> (Hs.Type () -> C a) -> C a
-    go _ EmptyTel cont = do
-      ctxArgs <- getContextArgs
-      ty <- compileType . unEl =<< t `piApplyM` ctxArgs
-      cont ty
-    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 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)
-
-
 -- | Compile an Agda term into a Haskell type, along with its strictness.
 compileTypeWithStrictness :: Term -> C (Strictness, Hs.Type ())
 compileTypeWithStrictness t = do
@@ -137,14 +90,13 @@ compileType t = do
   reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t
 
   case t of
-    Pi a b -> compileDomType (absName b) a >>= \case
-      DomType _ hsA -> do
-        hsB <- underAbstraction a b (compileType . unEl)
-        return $ Hs.TyFun () hsA hsB
-      DomConstraint hsA -> do
-        hsB <- underAbstraction a b (compileType . unEl)
-        return $ constrainType hsA hsB
-      DomDropped -> underAbstr a b (compileType . unEl)
+    Pi a b -> do
+      let compileB = underAbstraction a b (compileType . unEl)
+      compileDomType (absName b) a >>= \case
+        DomType _ hsA -> Hs.TyFun () hsA <$> compileB
+        DomConstraint hsA -> constrainType hsA <$> compileB
+        DomDropped -> compileB
+        DomForall hsA -> qualifyType hsA <$> compileB
 
     Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do
       def <- getConstInfo f
@@ -155,42 +107,71 @@ compileType t = do
          | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics es
          | Just args <- allApplyElims es ->
              ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
-             ifM (isTransparentFunction f) (compileTransparentType args) $
+             ifM (isTransparentFunction f) (compileTransparentType (defType def) args) $
              ifM (isInlinedFunction f) (compileInlineType f es) $ do
-               vs <- compileTypeArgs args
+               vs <- compileTypeArgs (defType def) args
                f <- compileQName f
                return $ tApp (Hs.TyCon () f) vs
          | otherwise -> fail
 
     Var x es | Just args <- allApplyElims es -> do
-      vs <- compileTypeArgs args
+      xi <- lookupBV x
+      unless (usableModality xi) $ genericDocError
+        =<< text "Cannot use erased variable" <+> prettyTCM (var x)
+        <+> text "in Haskell type"
+      vs <- compileTypeArgs (snd $ unDom xi) args
       x  <- hsName <$> compileDBVar x
       return $ tApp (Hs.TyVar () x) vs
 
     Sort s -> return (Hs.TyStar ())
 
-    Lam argInfo restAbs
-      | not (keepArg argInfo) -> 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
 
 
-compileTypeArgs :: Args -> C [Hs.Type ()]
-compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args
+compileTypeArgs :: Type -> Args -> C [Hs.Type ()]
+compileTypeArgs ty [] = pure []
+compileTypeArgs ty (x:xs) = do
+  (a, b) <- mustBePi ty
+  reportSDoc "agda2hs.compile.type" 16 $ text "compileTypeArgs x =" <+> prettyTCM x
+  reportSDoc "agda2hs.compile.type" 16 $ text "                a =" <+> prettyTCM a
+  reportSDoc "agda2hs.compile.type" 16 $ text "         modality =" <+> prettyTCM (getModality a)
+  let rest = compileTypeArgs (absApp b $ unArg x) xs  
+  let fail msg = genericDocError =<< (text msg <> text ":") <+> parens (prettyTCM (absName b) <+> text ":" <+> prettyTCM (unDom a))
+  compileDom a >>= \case
+    DODropped -> rest
+    DOInstance -> fail "Type-level instance argument not supported"
+    DOType -> do
+      (:) <$> compileType (unArg x) <*> rest
+    DOTerm -> fail "Type-level term argument not supported"
 
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
-  def <- theDef <$> getConstInfo r
-  let tel = telToList $ recTel def `apply` pars
-  case find keepArg tel of
-    Just t  -> compileType $ unEl $ snd (unDom t)
-    Nothing -> __IMPOSSIBLE__
-
-
-compileTransparentType :: Args -> C (Hs.Type ())
-compileTransparentType args = compileTypeArgs args >>= \case
+  def <- getConstInfo r
+  let tel = recTel (theDef def) `apply` pars
+  compileTel tel >>= \case
+    [t] -> return t
+    _   -> __IMPOSSIBLE__
+  
+  where
+    compileTel :: Telescope -> C [Hs.Type ()]
+    compileTel EmptyTel = return []
+    compileTel (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel compileTel
+      DOInstance -> __IMPOSSIBLE__
+      DOType     -> __IMPOSSIBLE__
+      DOTerm     -> (:) <$> compileType (unEl $ unDom a) <*> underAbstraction a tel compileTel
+      
+compileTransparentType :: Type -> Args -> C (Hs.Type ())
+compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs
   []     -> __IMPOSSIBLE__
 
@@ -212,57 +193,70 @@ compileInlineType f args = do
     _                -> genericDocError =<< text "Could not reduce inline type alias " <+> prettyTCM f
 
 
-data DomOutput = DOInstance | DODropped | DOKept
+data DomOutput = DOInstance | DODropped | DOType | DOTerm
 
 compileDom :: Dom Type -> C DomOutput
 compileDom a = do
   isErasable <- pure (not $ usableModality a) `or2M` canErase (unDom a)
   isClassConstraint <- pure (isInstance a) `and2M` isClassType (unDom a)
+  isType <- endsInSort (unDom a)
   return $ if 
     | isErasable        -> DODropped
     | isClassConstraint -> DOInstance
-    | otherwise         -> DOKept
+    | isType            -> DOType
+    | otherwise         -> DOTerm
 
 -- | Compile a function type domain.
 -- A domain can either be:
 --
 -- - dropped if the argument is erased.
 -- - added as a class constraint.
--- - kept as a regular explict argument.
+-- - added as a type parameter
+-- - kept as a regular explicit argument.
 compileDomType :: ArgName -> Dom Type -> C CompiledDom
 compileDomType x a =
   compileDom a >>= \case
     DODropped  -> pure DomDropped
     DOInstance -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
-    DOKept     -> uncurry DomType <$> compileTypeWithStrictness (unEl $ unDom a)
-
+    DOType     -> do
+      -- We compile (non-erased) type parameters to an explicit forall if they
+      -- come from a module parameter.
+      ctx <- getContextSize
+      npars <- size <$> (lookupSection =<< currentModule)
+      if ctx < npars 
+        then do
+          tellExtension Hs.ScopedTypeVariables
+          return $ DomForall $ Hs.UnkindedVar () $ Hs.Ident () x
+        else return $ DomDropped
+    DOTerm     -> uncurry DomType <$> compileTypeWithStrictness (unEl $ unDom a)
 
 compileTeleBinds :: Telescope -> C [Hs.TyVarBind ()]
-compileTeleBinds tel =
-  forM
-    (mapMaybe
-      (fmap unArgDom . checkArgDom)
-      (teleArgNames tel `zip` flattenTel @Type tel))
-    (uncurry compileKeptTeleBind)
-  where
-    checkArgDom (argName, argDom) | keepArg argName = Just (argName, argDom)
-    checkArgDom _ = Nothing
-
-    unArgDom (argName, argDom) = (hsName . unArg $ argName, unDom argDom)
+compileTeleBinds EmptyTel = return []
+compileTeleBinds (ExtendTel a tel) = do
+  reportSDoc "agda2hs.compile.type" 15 $ text "Compiling type parameter: " <+> prettyTCM a
+  let fail msg = genericDocError =<< (text msg <> text ":") <+> parens (prettyTCM (absName tel) <+> text ":" <+> prettyTCM (unDom a))
+  compileDom a >>= \case
+    DODropped  -> underAbstraction a tel compileTeleBinds
+    DOType -> do
+      ha <- compileKeptTeleBind (hsName $ absName tel) (unDom a)
+      (ha:) <$> underAbstraction a tel compileTeleBinds
+    DOInstance -> fail "Constraint in type parameter not supported"
+    DOTerm -> fail "Term variable in type parameter not supported"
 
 compileKeptTeleBind :: Hs.Name () -> Type -> C (Hs.TyVarBind ())
 compileKeptTeleBind x t = do
   checkValidTyVarName x
-  case compileKind t of
-    Just k              -> pure $ Hs.UnkindedVar () x -- In the future we may want to show kind annotations
-    _                   -> genericDocError =<<
-      text "Kind of bound argument not supported:"
-      <+> parens (text (Hs.prettyPrint x) <> text " : " <> prettyTCM t)
+  k <- compileKind t
+  pure $ Hs.UnkindedVar () x -- In the future we may want to show kind annotations
 
-compileKind :: Type -> Maybe (Hs.Kind ())
+compileKind :: Type -> C (Hs.Kind ())
 compileKind t = case unEl t of
   Sort (Type _) -> pure (Hs.TyStar ())
-  Pi a b
-    | keepArg a    -> Hs.TyFun () <$> compileKind (unDom a) <*> compileKind (unAbs b)
-    | otherwise    -> compileKind (unAbs b)
-  _ -> Nothing     -- ^ if the argument is erased, we only compile the rest
+  Pi a b -> compileDom a >>= \case
+    DODropped -> underAbstraction a b compileKind
+    DOType -> Hs.TyFun () <$> compileKind (unDom a) <*> underAbstraction a b compileKind
+    DOTerm -> err
+    DOInstance -> err
+  _ -> err
+  where
+    err = genericDocError =<< text "Not a valid Haskell kind: " <+> prettyTCM t
diff --git a/src/Agda2Hs/Compile/TypeDefinition.hs b/src/Agda2Hs/Compile/TypeDefinition.hs
index 5cd59c3c..3c126ff9 100644
--- a/src/Agda2Hs/Compile/TypeDefinition.hs
+++ b/src/Agda2Hs/Compile/TypeDefinition.hs
@@ -11,10 +11,12 @@ import Agda.Compiler.Backend
 import Agda.Syntax.Common ( namedArg )
 import Agda.Syntax.Internal
 
+import Agda.TypeChecking.Telescope ( mustBePi )
+
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Monad
 
-import Agda2Hs.Compile.Type ( compileType )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
@@ -26,7 +28,7 @@ compileTypeDef name (Defn {..}) = do
   unlessM (isTransparentFunction defName) $ checkValidTypeName name
   Clause{..} <- singleClause funClauses
   addContext (KeepNames clauseTel) $ do
-    as <- compileTypeArgs namedClausePats
+    as <- compileTypeArgs defType namedClausePats
     let hd = foldl (Hs.DHApp ()) (Hs.DHead () name) as
     rhs <- compileType $ fromMaybe __IMPOSSIBLE__ clauseBody
     return [Hs.TypeDecl () hd rhs]
@@ -37,8 +39,16 @@ compileTypeDef name (Defn {..}) = do
       _    -> genericError "Not supported: type definition with several clauses"
 
 
-compileTypeArgs :: NAPs -> C [Hs.TyVarBind ()]
-compileTypeArgs ps = mapM (compileTypeArg . namedArg) $ filter keepArg ps
+compileTypeArgs :: Type -> NAPs -> C [Hs.TyVarBind ()]
+compileTypeArgs ty [] = return []
+compileTypeArgs ty (p:ps) = do
+  (a,b) <- mustBePi ty
+  let rest = underAbstraction a b $ \ty' -> compileTypeArgs ty' ps
+  compileDom a >>= \case
+    DODropped -> rest
+    DOType -> (:) <$> compileTypeArg (namedArg p) <*> rest
+    DOTerm -> genericError "Not supported: type definition with term arguments"
+    DOInstance -> genericError "Not supported: type definition with instance arguments"
 
 compileTypeArg :: DeBruijnPattern -> C (Hs.TyVarBind ())
 compileTypeArg p@(VarP o i) = do
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 44c3b7fe..587dd7a9 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -80,10 +80,10 @@ data CompileEnv = CompileEnv
   -- ^ keeps track of the current minimal record we are compiling
   , locals :: LocalDecls
   -- ^ keeps track of the current clause's where declarations
+  , compilingLocal :: Bool
+  -- ^ whether we are currently compiling a where clause or pattern-matching lambda
   , copatternsEnabled :: Bool
   -- ^ whether copatterns should be allowed when compiling patterns
-  , checkVar :: Bool
-  -- ^ whether to ensure compiled variables are usable and visible
   , rewrites :: SpecialRules
   -- ^ Special compilation rules.
   }
@@ -183,6 +183,8 @@ data CompiledDom
     -- ^ To a Haskell type (with perhaps a strictness annotation)
   | DomConstraint (Hs.Asst ())
     -- ^ To a typeclass constraint
+  | DomForall (Hs.TyVarBind ())
+    -- ^ To an explicit forall
   | DomDropped
     -- ^ To nothing (e.g. erased proofs)
 
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index 6d785463..83ffaccd 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -126,17 +126,6 @@ underAbstr = underAbstraction' KeepNames
 underAbstr_ :: Subst a => Abs a -> (a -> C b) -> C b
 underAbstr_ = underAbstr __DUMMY_DOM__
 
--- | Determine whether an argument should be kept or dropped.
--- We drop all arguments that have quantity 0 (= run-time erased).
--- We also drop hidden non-erased arguments (which should all be of
--- type Level or Set l).
-keepArg :: (LensHiding a, LensModality a) => a -> Bool
-keepArg x = usableModality x && visible x
-
-
-keepClause :: Clause -> Bool
-keepClause = any keepArg . clauseType
-
 isPropSort :: Sort -> C Bool
 isPropSort s = reduce s <&> \case
   Prop _ -> True
@@ -151,7 +140,6 @@ canErase a = do
   addContext tel $ orM
     [ isLevelType b                       -- Level
     , isJust <$> isSizeType b             -- Size
-    , isJust . isSort <$> reduce (unEl b) -- Set
     , isPropSort (getSort b)              -- _ : Prop
     ]
 
@@ -192,19 +180,6 @@ dropClassModule m@(MName ns) = isClassModule m >>= \case
   True  -> dropClassModule $ MName $ init ns
   False -> return m
 
-moduleParametersToDrop :: ModuleName -> C Telescope
-moduleParametersToDrop mod = do
-   reportSDoc "agda2hs.moduleParameters" 25 $ text "Getting telescope for" <+> prettyTCM mod
-   isDatatypeModule mod >>= \case
-     Just _ -> return EmptyTel
-     Nothing -> do
-       reportSDoc "agda2hs.moduleParameters" 25 $ text "Current context: " <+> (prettyTCM =<< getContext)
-       ctxArgs <- getContextArgs
-       reportSDoc "agda2hs.moduleParameters" 25 $ text "Context arguments: " <+> prettyTCM ctxArgs
-       sec <- lookupSection mod
-       reportSDoc "agda2hs.moduleParameters" 25 $ text "Module section: " <+> prettyTCM sec
-       return $ sec `apply` ctxArgs
-
 isUnboxRecord :: QName -> C (Maybe Strictness)
 isUnboxRecord q = do
   getConstInfo q >>= \case
@@ -264,6 +239,9 @@ checkInstance u@(Con c _ _)
     prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" = return ()
 checkInstance u = genericDocError =<< text "illegal instance: " <+> prettyTCM u
 
+compileLocal :: C a -> C a
+compileLocal = local $ \e -> e { compilingLocal = True }
+
 modifyLCase :: (Int -> Int) -> CompileState -> CompileState
 modifyLCase f (CompileState {lcaseUsed = n}) = CompileState {lcaseUsed = f n}
 
@@ -325,9 +303,6 @@ checkNewtypeCon :: Hs.Name () -> [b] -> C ()
 checkNewtypeCon name tys =
   checkSingleElement name tys "Newtype must have exactly one field in constructor"
 
-checkingVars :: C a -> C a
-checkingVars = local $ \e -> e { checkVar = True }
-
 checkFixityLevel :: QName -> FixityLevel -> C (Maybe Int)
 checkFixityLevel name Unrelated = pure Nothing
 checkFixityLevel name (Related lvl) =
diff --git a/src/Agda2Hs/Compile/Var.hs b/src/Agda2Hs/Compile/Var.hs
index 877619f1..13ed373f 100644
--- a/src/Agda2Hs/Compile/Var.hs
+++ b/src/Agda2Hs/Compile/Var.hs
@@ -15,15 +15,8 @@ import Agda.TypeChecking.Monad.Context ( lookupBV )
 import Agda.Utils.Monad ( whenM )
 
 
--- | Compile a variable. 
--- If the variable check is enabled, ensure that the variable is usable and visible.
+-- | Compile a variable.
 compileDBVar :: Nat -> C String
 compileDBVar x = do
   (d, n) <- (fmap snd &&& fst . unDom) <$> lookupBV x
-  let cn = prettyShow $ nameConcrete n
-  let b | notVisible d   = "hidden"
-        | hasQuantity0 d = "erased"
-        | otherwise      = ""
-  whenM (asks checkVar) $ unless (null b) $ genericDocError =<<
-    text ("Cannot use " <> b <> " variable " <> cn)
-  return cn
+  return $ prettyShow $ nameConcrete n
diff --git a/src/Agda2Hs/HsUtils.hs b/src/Agda2Hs/HsUtils.hs
index 134ebafd..1c4efae0 100644
--- a/src/Agda2Hs/HsUtils.hs
+++ b/src/Agda2Hs/HsUtils.hs
@@ -297,12 +297,10 @@ constrainType c = \case
 
 -- | Add explicit quantification over a variable to a Haskell type.
 qualifyType
-  :: String  -- ^ Name of the variable.
+  :: TyVarBind ()  -- ^ Name of the variable.
   -> Type () -- ^ Type to quantify.
   -> Type ()
-qualifyType s = \case
+qualifyType a = \case
     TyForall _ (Just as) cs t -> TyForall () (Just (a:as)) cs      t
     TyForall _ Nothing   cs t -> TyForall () (Just [a]   ) cs      t
     t                         -> TyForall () (Just [a]   ) Nothing t
-  where
-    a = UnkindedVar () $ Ident () s
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 850f59bb..3c5b5ae0 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -75,6 +75,10 @@ import Issue286
 import NonClassInstance
 import Issue218
 import Issue251
+import TypeBasedUnboxing
+import Issue145
+import Issue264
+import Issue301
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -149,4 +153,8 @@ import Issue286
 import NonClassInstance
 import Issue218
 import Issue251
+import TypeBasedUnboxing
+import Issue145
+import Issue264
+import Issue301
 #-}
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/Fail/Issue145.agda b/test/Issue145.agda
similarity index 94%
rename from test/Fail/Issue145.agda
rename to test/Issue145.agda
index d4863b10..feae5372 100644
--- a/test/Fail/Issue145.agda
+++ b/test/Issue145.agda
@@ -1,4 +1,4 @@
-module Fail.Issue145 where
+module Issue145 where
 
 open import Haskell.Prelude
 open import Haskell.Prim.Strict
diff --git a/test/Issue264.agda b/test/Issue264.agda
new file mode 100644
index 00000000..68ab94ec
--- /dev/null
+++ b/test/Issue264.agda
@@ -0,0 +1,15 @@
+
+module Issue264 (@0 name : Set) where
+
+data Term : @0 Set → Set where
+  Dummy : Term name
+
+{-# COMPILE AGDA2HS Term #-}
+
+reduce : Term name → Term name
+reduce v = go v
+  where
+    go : Term name → Term name
+    go v = v
+
+{-# COMPILE AGDA2HS reduce #-}
diff --git a/test/Issue301.agda b/test/Issue301.agda
new file mode 100644
index 00000000..16793fc4
--- /dev/null
+++ b/test/Issue301.agda
@@ -0,0 +1,36 @@
+
+open import Haskell.Prelude
+open import Haskell.Prim.Monoid
+open import Haskell.Prim.Foldable
+
+data MyData (a : Set) : Set where
+  Nuttin' : MyData a
+{-# COMPILE AGDA2HS MyData #-}
+
+-- notice this does not occur with other classes such as Foldable
+myDataDefaultFoldable : DefaultFoldable MyData
+DefaultFoldable.foldMap myDataDefaultFoldable _ _ = mempty
+
+instance
+  MyDataFoldable : Foldable MyData
+  MyDataFoldable = record {DefaultFoldable myDataDefaultFoldable}
+{-# COMPILE AGDA2HS MyDataFoldable #-}
+
+-- need to create instance for semigroup first
+-- (requires explicitly typed function AFAICT)
+_><_ : {a : Set} -> MyData a -> MyData a -> MyData a
+_ >< _ = Nuttin'
+{-# COMPILE AGDA2HS _><_ #-}
+
+instance
+  MyDataSemigroup : Semigroup (MyData a)
+  MyDataSemigroup ._<>_ = _><_
+{-# COMPILE AGDA2HS MyDataSemigroup #-}
+
+myDataDefaultMonoid : DefaultMonoid (MyData a)
+DefaultMonoid.mempty myDataDefaultMonoid = Nuttin'
+
+instance
+  MyDataMonoid : Monoid (MyData a)
+  MyDataMonoid = record {DefaultMonoid myDataDefaultMonoid}
+{-# COMPILE AGDA2HS MyDataMonoid #-}
diff --git a/test/TypeBasedUnboxing.agda b/test/TypeBasedUnboxing.agda
new file mode 100644
index 00000000..bb7e8e7f
--- /dev/null
+++ b/test/TypeBasedUnboxing.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --prop --sized-types #-}
+
+open import Agda.Primitive
+open import Agda.Builtin.Size
+open import Haskell.Prelude
+
+data P : Prop where
+
+record R : Set where
+  field
+    @0 anErasedThing : Bool
+    aRealThing : Int
+    aLevel : Level
+    aProp : P
+    aSize : Size
+open R public
+
+{-# COMPILE AGDA2HS R unboxed #-}
+
+foo : R → Int
+foo = aRealThing
+
+{-# COMPILE AGDA2HS foo #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index e38f94a7..1f7e9158 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -72,4 +72,8 @@ import Issue286
 import NonClassInstance
 import Issue218
 import Issue251
+import TypeBasedUnboxing
+import Issue145
+import Issue264
+import Issue301
 
diff --git a/test/golden/ErasedRecordParameter.err b/test/golden/ErasedRecordParameter.err
index 2aaa71fe..fcd7e22e 100644
--- a/test/golden/ErasedRecordParameter.err
+++ b/test/golden/ErasedRecordParameter.err
@@ -1,2 +1,2 @@
 test/Fail/ErasedRecordParameter.agda:4,8-10
-Cannot use erased variable a
+Cannot use erased variable a in Haskell type
diff --git a/test/golden/Issue113a.err b/test/golden/Issue113a.err
index 9e533801..8fef39b0 100644
--- a/test/golden/Issue113a.err
+++ b/test/golden/Issue113a.err
@@ -1,3 +1,2 @@
 test/Fail/Issue113a.agda:5,8-12
-An unboxed type must be a non-recursive record type with exactly
-one non-erased field.
+Unboxed record Loop cannot be recursive
diff --git a/test/golden/Issue113b.err b/test/golden/Issue113b.err
index e9694b43..95bceec2 100644
--- a/test/golden/Issue113b.err
+++ b/test/golden/Issue113b.err
@@ -1,3 +1,2 @@
 test/Fail/Issue113b.agda:7,8-12
-An unboxed type must be a non-recursive record type with exactly
-one non-erased field.
+Unboxed record Loop cannot be recursive
diff --git a/test/golden/Issue145.err b/test/golden/Issue145.err
deleted file mode 100644
index 81999292..00000000
--- a/test/golden/Issue145.err
+++ /dev/null
@@ -1,2 +0,0 @@
-test/Fail/Issue145.agda:23,6-8
-Cannot use hidden variable a
diff --git a/test/golden/Issue145.hs b/test/golden/Issue145.hs
new file mode 100644
index 00000000..f18013ae
--- /dev/null
+++ b/test/golden/Issue145.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE ScopedTypeVariables, BangPatterns #-}
+module Issue145 where
+
+it :: forall a . a -> a
+it x = x
+
+it' :: Monoid a => a -> a
+it' x = x
+
+data Ok' a = Thing' !a
+
+data Ok a = Thing a
+
+test :: Ok String
+test = Thing "ok"
+
diff --git a/test/golden/Issue264.hs b/test/golden/Issue264.hs
new file mode 100644
index 00000000..f1fd847f
--- /dev/null
+++ b/test/golden/Issue264.hs
@@ -0,0 +1,10 @@
+module Issue264 where
+
+data Term = Dummy
+
+reduce :: Term -> Term
+reduce v = go v
+  where
+    go :: Term -> Term
+    go v = v
+
diff --git a/test/golden/Issue301.hs b/test/golden/Issue301.hs
new file mode 100644
index 00000000..0b4061ce
--- /dev/null
+++ b/test/golden/Issue301.hs
@@ -0,0 +1,16 @@
+module Issue301 where
+
+data MyData a = Nuttin'
+
+instance Foldable MyData where
+    foldMap _ _ = mempty
+
+(><) :: MyData a -> MyData a -> MyData a
+_ >< _ = Nuttin'
+
+instance Semigroup (MyData a) where
+    (<>) = (><)
+
+instance Monoid (MyData a) where
+    mempty = Nuttin'
+
diff --git a/test/golden/ModuleParameters.hs b/test/golden/ModuleParameters.hs
index bb75c348..8705650c 100644
--- a/test/golden/ModuleParameters.hs
+++ b/test/golden/ModuleParameters.hs
@@ -4,7 +4,7 @@ module ModuleParameters where
 data Scope p = Empty
              | Bind p (Scope p)
 
-unbind :: Scope p -> Scope p
+unbind :: forall p . Scope p -> Scope p
 unbind Empty = Empty
 unbind (Bind _ s) = s
 
diff --git a/test/golden/NonStarDatatypeIndex.err b/test/golden/NonStarDatatypeIndex.err
index bd13e264..71835141 100644
--- a/test/golden/NonStarDatatypeIndex.err
+++ b/test/golden/NonStarDatatypeIndex.err
@@ -1,2 +1,2 @@
 test/Fail/NonStarDatatypeIndex.agda:5,6-7
-Kind of bound argument not supported: (n : Nat)
+Term variable in type parameter not supported: (n : Nat)
diff --git a/test/golden/NonStarRecordIndex.err b/test/golden/NonStarRecordIndex.err
index d6fb0e36..6803b92c 100644
--- a/test/golden/NonStarRecordIndex.err
+++ b/test/golden/NonStarRecordIndex.err
@@ -1,2 +1,2 @@
 test/Fail/NonStarRecordIndex.agda:5,8-9
-Kind of bound argument not supported: (n : Nat)
+Term variable in type parameter not supported: (n : Nat)
diff --git a/test/golden/TypeBasedUnboxing.hs b/test/golden/TypeBasedUnboxing.hs
new file mode 100644
index 00000000..f71a61a0
--- /dev/null
+++ b/test/golden/TypeBasedUnboxing.hs
@@ -0,0 +1,5 @@
+module TypeBasedUnboxing where
+
+foo :: Int -> Int
+foo = \ r -> r
+
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