diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 7220cc2351..548c7487f5 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -40,7 +40,6 @@ import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as S
 import Juvix.Compiler.Store.Scoped.Language (createExportsTable)
 import Juvix.Compiler.Store.Scoped.Language qualified as S
 import Juvix.Prelude
-import Juvix.Prelude.Stream qualified as Stream
 import Safe (lastMay)
 
 -- | Needed to generate field projections and deriving instances
@@ -602,10 +601,15 @@ deriveEq pragmas instanceName funParams (eqName, args) = do
           Internal.ConstructorName ->
           Sem r Internal.LambdaClause
         lambdaClause band btrue bisEqual c = do
-          numArgs :: Int <- getNumArgs
-          let mkpat = do
-                xs <- mapM (Internal.freshVar (getLoc instanceName)) (Stream.take numArgs allWords)
-                return (xs, Internal.mkConstructorVarPattern Explicit c ((Explicit,) <$> xs))
+          numArgs :: [IsImplicit] <- getNumArgs
+          let loc = getLoc instanceName
+              mkpat :: Sem r ([Internal.VarName], Internal.PatternArg)
+              mkpat = runOutputList . runStreamOf allWords $ do
+                xs :: [(IsImplicit, Internal.VarName)] <- forM numArgs $ \impl -> do
+                  v <- yield >>= Internal.freshVar loc
+                  output v
+                  return (impl, v)
+                return (Internal.mkConstructorVarPattern Explicit c xs)
           (v1, p1) <- mkpat
           (v2, p2) <- mkpat
           return
@@ -628,12 +632,15 @@ deriveEq pragmas instanceName funParams (eqName, args) = do
             mkEq :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression
             mkEq a b = bisEqual Internal.@@ a Internal.@@ b
 
-            getNumArgs :: Sem r Int
+            getNumArgs :: Sem r [IsImplicit]
             getNumArgs = do
               def <- getDefinedConstructor c
-              let cargs :: [Internal.FunctionParameter] = Internal.constructorArgs (def ^. Internal.constructorInfoType)
-              unless (all ((== Explicit) . (^. Internal.paramImplicit)) cargs) (error "TODO all args must be explicit")
-              return (length cargs)
+              return $
+                def
+                  ^.. Internal.constructorInfoType
+                    . to Internal.constructorArgs
+                    . each
+                    . Internal.paramImplicit
 
 goFunctionDef ::
   forall r.