diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
index c34c6c676d..4305f162e8 100644
--- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
@@ -423,6 +423,7 @@ goStatement = \case
   StatementInductive t -> goInductive t
   StatementOpenModule t -> goOpen t
   StatementFunctionDef t -> goFunctionDef t
+  StatementDeriving t -> goDeriving t
   StatementSyntax syn -> goSyntax syn
   StatementImport t -> goImport t
   StatementModule m -> goLocalModule m
@@ -537,13 +538,15 @@ goAxiom axiom = do
     axiomHeader :: Sem r Html
     axiomHeader = ppCodeHtml defaultOptions (set axiomDoc Nothing axiom)
 
+goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
+goDeriving def = do
+  sig <- ppHelper (ppCode def)
+  defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing
+
 goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
 goFunctionDef def = do
-  sig' <- funSig
-  defHeader (def ^. signName) sig' (def ^. signDoc)
-  where
-    funSig :: Sem r Html
-    funSig = ppHelper (ppCode (functionDefLhs def))
+  sig <- ppHelper (ppCode (functionDefLhs def))
+  defHeader (def ^. signName) sig (def ^. signDoc)
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do
diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
index f4c849fc3b..ac53b3c3b5 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
@@ -213,12 +213,13 @@ indModuleFilter :: forall s. [Concrete.Statement s] -> [Concrete.Statement s]
 indModuleFilter =
   filter
     ( \case
-        Concrete.StatementSyntax _ -> True
-        Concrete.StatementFunctionDef _ -> True
-        Concrete.StatementImport _ -> True
-        Concrete.StatementInductive _ -> True
         Concrete.StatementModule o -> o ^. Concrete.moduleOrigin == LocalModuleSource
-        Concrete.StatementOpenModule _ -> True
-        Concrete.StatementAxiom _ -> True
-        Concrete.StatementProjectionDef _ -> True
+        Concrete.StatementSyntax {} -> True
+        Concrete.StatementFunctionDef {} -> True
+        Concrete.StatementDeriving {} -> True
+        Concrete.StatementImport {} -> True
+        Concrete.StatementInductive {} -> True
+        Concrete.StatementOpenModule {} -> True
+        Concrete.StatementAxiom {} -> True
+        Concrete.StatementProjectionDef {} -> True
     )
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index 4537498e5f..64ab634fd3 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -166,7 +166,7 @@ data BuiltinFunction
   | BuiltinIntLe
   | BuiltinIntLt
   | BuiltinFromNat
-  | BuiltinIsEq
+  | BuiltinIsEqual
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -208,7 +208,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
-    BuiltinIsEq -> Str.isEqual
+    BuiltinIsEqual -> Str.isEqual
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -441,7 +441,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
@@ -494,7 +494,7 @@ isIntBuiltin = \case
   BuiltinFromNat -> False
   BuiltinFromInt -> False
   BuiltinSeq -> False
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
@@ -502,7 +502,7 @@ isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
@@ -542,7 +542,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
-        .&&. (/= BuiltinIsEq)
+        .&&. (/= BuiltinIsEqual)
         $ f
 
     explicit :: Bool
@@ -574,7 +574,7 @@ isIgnoredBuiltin f
       BuiltinNatLt -> False
       BuiltinNatEq -> False
       -- Eq
-      BuiltinIsEq -> False
+      BuiltinIsEqual -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index c790b5b1b6..3b5abbcc6e 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1052,19 +1052,108 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do
 (@$>) :: (Functor m) => (a -> m ()) -> a -> m a
 (@$>) f a = f a $> a
 
-withFunctionDefLhs ::
-  FunctionLhs 'Parsed ->
-  (FunctionLhs 'Scoped -> Sem r a)
-  Sem r a
-withFunctionDefLhs FunctionLhs {..} checkBody = do
-  body' <- withLocalScope $ do
-    args' <- mapM checkArg _funLhsArgs
-    ret' <- mapM checkParseExpressionAtoms _funLhsRetType
-    let lhs' = FunctionLhs {
-          _funLhsArgs = args',
-          _funLhsRetType = ret'
-                           }
-    checkBody lhs'
+checkDeriving ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  Deriving 'Parsed ->
+  Sem r (Deriving 'Scoped)
+checkDeriving Deriving {..} = withLocalScope $ do
+  let lhs@FunctionLhs {..} = _derivingFunLhs
+  args' <- mapM checkSigArg _funLhsArgs
+  ret' <- mapM checkParseExpressionAtoms _funLhsRetType
+  name' <-
+    if
+        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName
+        | otherwise -> reserveFunctionSymbol lhs
+  let lhs' =
+        FunctionLhs
+          { _funLhsArgs = args',
+            _funLhsRetType = ret',
+            _funLhsName = name',
+            ..
+          }
+
+  return
+    Deriving
+      { _derivingFunLhs = lhs',
+        ..
+      }
+
+checkSigArg ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  SigArg 'Parsed ->
+  Sem r (SigArg 'Scoped)
+checkSigArg arg@SigArg {..} = do
+  names' <- checkSigArgNames _sigArgNames
+  ty' <- mapM checkParseExpressionAtoms _sigArgType
+  default' <- case _sigArgDefault of
+    Nothing -> return Nothing
+    Just ArgDefault {..} ->
+      let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg})
+       in case _sigArgImplicit of
+            Explicit -> err
+            ImplicitInstance -> err
+            Implicit -> do
+              val' <- checkParseExpressionAtoms _argDefaultValue
+              return (Just ArgDefault {_argDefaultValue = val', ..})
+  return
+    SigArg
+      { _sigArgNames = names',
+        _sigArgType = ty',
+        _sigArgDefault = default',
+        ..
+      }
+
+checkSigArgNames ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  SigArgNames 'Parsed ->
+  Sem r (SigArgNames 'Scoped)
+checkSigArgNames = \case
+  SigArgNamesInstance -> return SigArgNamesInstance
+  SigArgNames ns -> fmap SigArgNames . forM ns $ \case
+    ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
+    ArgumentWildcard w -> return (ArgumentWildcard w)
 
 checkFunctionDef ::
   forall r.
@@ -1074,7 +1163,7 @@ checkFunctionDef ::
 checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
   (args', sigType', sigBody') <- withLocalScope $ do
-    a' <- mapM checkArg _signArgs
+    a' <- mapM checkSigArg _signArgs
     t' <- mapM checkParseExpressionAtoms _signRetType
     b' <- checkBody
     return (a', t', b')
@@ -1094,34 +1183,6 @@ checkFunctionDef fdef@FunctionDef {..} = do
   registerNameSignature (sigName' ^. S.nameId) def
   registerFunctionDef @$> def
   where
-    checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped)
-    checkSigArgNames = \case
-      SigArgNamesInstance -> return SigArgNamesInstance
-      SigArgNames ns -> fmap SigArgNames . forM ns $ \case
-        ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
-        ArgumentWildcard w -> return (ArgumentWildcard w)
-
-    checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped)
-    checkArg arg@SigArg {..} = do
-      names' <- checkSigArgNames _sigArgNames
-      ty' <- mapM checkParseExpressionAtoms _sigArgType
-      default' <- case _sigArgDefault of
-        Nothing -> return Nothing
-        Just ArgDefault {..} ->
-          let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg})
-           in case _sigArgImplicit of
-                Explicit -> err
-                ImplicitInstance -> err
-                Implicit -> do
-                  val' <- checkParseExpressionAtoms _argDefaultValue
-                  return (Just ArgDefault {_argDefaultValue = val', ..})
-      return
-        SigArg
-          { _sigArgNames = names',
-            _sigArgType = ty',
-            _sigArgDefault = default',
-            ..
-          }
     checkBody :: Sem r (FunctionDefBody 'Scoped)
     checkBody = case _signBody of
       SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
@@ -2196,6 +2257,7 @@ checkLetStatements =
               DefinitionFunctionDef d -> LetFunctionDef d
               DefinitionSyntax syn -> fromSyn syn
               DefinitionInductive {} -> impossible
+              DefinitionDeriving {} -> impossible
               DefinitionProjectionDef {} -> impossible
               DefinitionAxiom {} -> impossible
 
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index db5d3be01e..8130da10a5 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1368,14 +1368,13 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   _signBody <- parseBody
   unless
     ( isJust (_funLhsColonKw ^. unIrrelevant)
-        || (maybe True P.isBodyExpression _signBody && null _funLhsArgs)
+        || (P.isBodyExpression _signBody && null _funLhsArgs)
     )
     $ parseFailure off "expected result type"
   return
     FunctionDef
       { _signName = _funLhsName,
         _signArgs = _funLhsArgs,
-        _signDeriving = _funLhsDeriving,
         _signColonKw = _funLhsColonKw,
         _signRetType = _funLhsRetType,
         _signTerminating = _funLhsTerminating,
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 59b75ff729..c90354ad68 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -54,7 +54,7 @@ fromCore fsize tab =
       BuiltinIntLe -> False
       BuiltinIntLt -> False
       BuiltinSeq -> False
-      BuiltinIsEq -> False
+      BuiltinIsEqual -> False
       BuiltinMonadBind -> True -- TODO revise
       BuiltinFromNat -> True
       BuiltinFromInt -> True
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index cde2d3a091..8573a0916c 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -424,12 +424,15 @@ foldApplication f args = case nonEmpty args of
 unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg)
 unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l')
 
--- TODO make it tail recursive
 unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg])
-unfoldExpressionApp = \case
-  ExpressionApplication (Application l r i) ->
-    second (`snoc` ApplicationArg i r) (unfoldExpressionApp l)
-  e -> (e, [])
+unfoldExpressionApp = swap . run . runAccumListReverse . go
+  where
+    go :: Expression -> Sem '[Accum ApplicationArg] Expression
+    go = \case
+      ExpressionApplication (Application l r i) -> do
+        accum (ApplicationArg i r)
+        go l
+      e -> return e
 
 unfoldApplication :: Application -> (Expression, NonEmpty Expression)
 unfoldApplication = fmap (fmap (^. appArg)) . unfoldApplication'
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 4f080319b8..8c822bb019 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -19,6 +19,7 @@ import Juvix.Data.Universe hiding (smallUniverse)
 import Juvix.Data.WithLoc
 import Juvix.Extra.Serialize
 import Juvix.Prelude
+import Juvix.Prelude.Pretty
 
 type Module = Module' MutualBlock
 
@@ -31,6 +32,18 @@ type PreModuleBody = ModuleBody' PreStatement
 newtype PreLetStatement
   = PreLetFunctionDef FunctionDef
 
+-- | Traits that support builtin deriving
+data DerivingTrait = DerivingEq
+  deriving stock (Generic, Data, Bounded, Enum, Show)
+
+instance IsBuiltin DerivingTrait where
+  toBuiltinPrim :: DerivingTrait -> BuiltinPrim
+  toBuiltinPrim = \case
+    DerivingEq -> toBuiltinPrim BuiltinEq
+
+instance Pretty DerivingTrait where
+  pretty = pretty . toBuiltinPrim
+
 data PreStatement
   = PreFunctionDef FunctionDef
   | PreInductiveDef InductiveDef
@@ -484,6 +497,7 @@ data NormalizedExpression = NormalizedExpression
   }
 
 makePrisms ''Expression
+makePrisms ''Iden
 makePrisms ''MutualStatement
 
 makeLenses ''SideIfBranch
@@ -584,7 +598,7 @@ instance HasAtomicity Pattern where
     PatternWildcardConstructor {} -> Atom
 
 instance HasLoc Module where
-  getLoc m = getLoc (m ^. moduleName) <>? maybe Nothing (Just . getLocSpan) (nonEmpty (m ^. moduleBody . moduleStatements))
+  getLoc m = getLoc (m ^. moduleName) <>? fmap getLocSpan (nonEmpty (m ^. moduleBody . moduleStatements))
 
 instance HasLoc MutualBlock where
   getLoc = getLocSpan . (^. mutualStatements)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 924ecbaf27..acdcb500f2 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -275,9 +275,13 @@ goModuleBody ::
 goModuleBody stmts = do
   _moduleImports <- mapM goImport (scanImports stmts)
   otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goAxiomInductive) ss
-  functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions
-  projections <- map (fmap Internal.PreFunctionDef) <$> mkProjections
-  let unsorted = otherThanFunctions <> functions <> projections
+  funs :: [Indexed Internal.PreStatement] <-
+    sequence
+      [ Indexed i . Internal.PreFunctionDef <$> d
+        | Indexed i s <- ss,
+          Just d <- [mkFunctionLike s]
+      ]
+  let unsorted = otherThanFunctions <> funs
       _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) unsorted)
   return Internal.ModuleBody {..}
   where
@@ -287,21 +291,17 @@ goModuleBody stmts = do
     ss :: [Indexed (Statement 'Scoped)]
     ss = zipWith Indexed [0 ..] ss'
 
-    mkProjections :: Sem r [Indexed Internal.FunctionDef]
-    mkProjections =
-      sequence
-        [ Indexed i <$> funDef
-          | Indexed i (StatementProjectionDef f) <- ss,
-            let funDef = goProjectionDef f
-        ]
-
-    compiledFunctions :: Sem r [Indexed Internal.FunctionDef]
-    compiledFunctions =
-      sequence
-        [ Indexed i <$> funDef
-          | Indexed i (StatementFunctionDef f) <- ss,
-            let funDef = goFunctionDef f
-        ]
+    mkFunctionLike :: Statement 'Scoped -> Maybe (Sem r (Internal.FunctionDef))
+    mkFunctionLike s = case s of
+      StatementFunctionDef d -> Just (goFunctionDef d)
+      StatementProjectionDef d -> Just (goProjectionDef d)
+      StatementDeriving d -> Just (goDeriving d)
+      StatementSyntax {} -> Nothing
+      StatementImport {} -> Nothing
+      StatementInductive {} -> Nothing
+      StatementModule {} -> Nothing
+      StatementOpenModule {} -> Nothing
+      StatementAxiom {} -> Nothing
 
 scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
 scanImports = mconcatMap go
@@ -388,12 +388,70 @@ goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs)
                 _argInfoName = goSymbol <$> (i ^. nameItemSymbol)
               }
 
+goDeriving ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>
+  Deriving 'Scoped ->
+  Sem r Internal.FunctionDef
+goDeriving Deriving {..} = do
+  let FunctionLhs {..} = _derivingFunLhs
+      name = goSymbol _funLhsName
+  (funArgs, ret) <- Internal.unfoldFunType <$> goDefType _derivingFunLhs
+  let (mtrait, traitArgs) = Internal.unfoldExpressionApp ret
+  der <- findDerivingTrait mtrait
+  deriveTrait der name funArgs traitArgs
+
+deriveTrait ::
+  (Members '[Reader S.InfoTable, NameIdGen] r) =>
+  Internal.DerivingTrait ->
+  Internal.Name ->
+  [Internal.FunctionParameter] ->
+  [Internal.ApplicationArg] ->
+  Sem r Internal.FunctionDef
+deriveTrait = \case
+  Internal.DerivingEq -> deriveEq
+
+findDerivingTrait ::
+  ( Members
+      '[ Error ScoperError,
+         Reader S.InfoTable
+       ]
+      r
+  ) =>
+  Internal.Expression ->
+  Sem r Internal.DerivingTrait
+findDerivingTrait e = do
+  i :: Internal.Name <- maybe (throw err) return (e ^? Internal._ExpressionIden . Internal._IdenInductive)
+  tbl :: BuiltinsTable <- asks (^. S.infoBuiltins)
+  let isTrait :: Internal.DerivingTrait -> Bool
+      isTrait t = Just i == (goSymbol <$> tbl ^. at (toBuiltinPrim t))
+  maybe (throw err) return (find isTrait allElements)
+  where
+    err :: ScoperError
+    err = error "TODO It is only possible to derive ...."
+
+deriveEq ::
+  (Members '[Reader S.InfoTable, NameIdGen] r) =>
+  Internal.Name ->
+  [Internal.FunctionParameter] ->
+  [Internal.ApplicationArg] ->
+  Sem r Internal.FunctionDef
+deriveEq name funParam args = do
+  return
+    Internal.FunctionDef
+      { _funDefTerminating = False,
+        _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance,
+        _funDefPragmas = mempty,
+        _funDefDocComment = Nothing,
+        _funDefBuiltin = Nothing
+      }
+
 goFunctionDef ::
   forall r.
   (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>
   FunctionDef 'Scoped ->
   Sem r Internal.FunctionDef
-goFunctionDef FunctionDef {..} = do
+goFunctionDef def@FunctionDef {..} = do
   let _funDefName = goSymbol _signName
       _funDefTerminating = isJust _signTerminating
       _funDefIsInstanceCoercion
@@ -402,7 +460,7 @@ goFunctionDef FunctionDef {..} = do
         | otherwise = Nothing
       _funDefCoercion = isJust _signCoercion
       _funDefBuiltin = (^. withLocParam) <$> _signBuiltin
-  _funDefType <- goDefType
+  _funDefType <- goDefType (functionDefLhs def)
   _funDefPragmas <- goPragmas _signPragmas
   _funDefBody <- goBody
   msig <- asks (^. S.infoNameSigs . at (_funDefName ^. Internal.nameId))
@@ -436,63 +494,79 @@ goFunctionDef FunctionDef {..} = do
           let _lambdaType :: Maybe Internal.Expression = Nothing
           return (Internal.ExpressionLambda Internal.Lambda {..})
 
-    goDefType :: Sem r Internal.Expression
-    goDefType = do
-      args <- concatMapM (fmap toList . argToParam) _signArgs
-      ret <- maybe freshHole goExpression _signRetType
-      return (Internal.foldFunType args ret)
-      where
-        freshHole :: Sem r Internal.Expression
-        freshHole = do
-          i <- freshNameId
-          let loc = maybe (getLoc _signName) getLoc (lastMay _signArgs)
-              h = mkHole loc i
-          return $ Internal.ExpressionHole h
-
-        argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter)
-        argToParam a@SigArg {..} = do
-          let _paramImplicit = _sigArgImplicit
-          _paramType <- case _sigArgType of
-            Nothing -> return (Internal.smallUniverseE (getLoc a))
-            Just ty -> goExpression ty
-
-          let _paramImpligoExpressioncit = _sigArgImplicit
-              noName = Internal.FunctionParameter {_paramName = Nothing, ..}
-              mk :: Concrete.Argument 'Scoped -> Internal.FunctionParameter
-              mk ma =
-                let _paramName =
-                      case ma of
-                        Concrete.ArgumentSymbol s -> Just (goSymbol s)
-                        Concrete.ArgumentWildcard {} -> Nothing
-                 in Internal.FunctionParameter {..}
-
-              arguments :: Maybe (NonEmpty (Argument 'Scoped))
-              arguments = case _sigArgNames of
-                SigArgNamesInstance -> Nothing
-                SigArgNames ns -> Just ns
-
-          return (maybe (pure noName) (fmap mk) arguments)
-
-    argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg)
-    argToPattern arg@SigArg {..} = do
-      let _patternArgIsImplicit = _sigArgImplicit
-          _patternArgName :: Maybe Internal.Name = Nothing
-          noName = goWildcard (Wildcard (getLoc arg))
-          goWildcard w = do
-            _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w
-            return Internal.PatternArg {..}
-          mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg
-          mk = \case
-            Concrete.ArgumentSymbol s ->
-              let _patternArgPattern = Internal.PatternVariable (goSymbol s)
-               in return Internal.PatternArg {..}
-            Concrete.ArgumentWildcard w -> goWildcard w
+argToPattern ::
+  forall r.
+  (Members '[NameIdGen] r) =>
+  SigArg 'Scoped ->
+  Sem r (NonEmpty Internal.PatternArg)
+argToPattern arg@SigArg {..} = do
+  let _patternArgIsImplicit = _sigArgImplicit
+      _patternArgName :: Maybe Internal.Name = Nothing
+      noName = goWildcard (Wildcard (getLoc arg))
+      goWildcard w = do
+        _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w
+        return Internal.PatternArg {..}
+      mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg
+      mk = \case
+        Concrete.ArgumentSymbol s ->
+          let _patternArgPattern = Internal.PatternVariable (goSymbol s)
+           in return Internal.PatternArg {..}
+        Concrete.ArgumentWildcard w -> goWildcard w
+
+      arguments :: Maybe (NonEmpty (Argument 'Scoped))
+      arguments = case _sigArgNames of
+        SigArgNamesInstance -> Nothing
+        SigArgNames ns -> Just ns
+  maybe (pure <$> noName) (mapM mk) arguments
+
+goDefType ::
+  forall r.
+  ( Members
+      '[ Reader DefaultArgsStack,
+         NameIdGen,
+         Error ScoperError,
+         Reader Pragmas,
+         Reader S.InfoTable
+       ]
+      r
+  ) =>
+  FunctionLhs 'Scoped ->
+  Sem r Internal.Expression
+goDefType FunctionLhs {..} = do
+  args <- concatMapM (fmap toList . argToParam) _funLhsArgs
+  ret <- maybe freshHole goExpression _funLhsRetType
+  return (Internal.foldFunType args ret)
+  where
+    freshHole :: Sem r Internal.Expression
+    freshHole = do
+      i <- freshNameId
+      let loc = maybe (getLoc _funLhsName) getLoc (lastMay _funLhsArgs)
+          h = mkHole loc i
+      return $ Internal.ExpressionHole h
+
+    argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter)
+    argToParam a@SigArg {..} = do
+      let _paramImplicit = _sigArgImplicit
+      _paramType <- case _sigArgType of
+        Nothing -> return (Internal.smallUniverseE (getLoc a))
+        Just ty -> goExpression ty
+
+      let _paramImpligoExpressioncit = _sigArgImplicit
+          noName = Internal.FunctionParameter {_paramName = Nothing, ..}
+          mk :: Concrete.Argument 'Scoped -> Internal.FunctionParameter
+          mk ma =
+            let _paramName =
+                  case ma of
+                    Concrete.ArgumentSymbol s -> Just (goSymbol s)
+                    Concrete.ArgumentWildcard {} -> Nothing
+             in Internal.FunctionParameter {..}
 
           arguments :: Maybe (NonEmpty (Argument 'Scoped))
           arguments = case _sigArgNames of
             SigArgNamesInstance -> Nothing
             SigArgNames ns -> Just ns
-      maybe (pure <$> noName) (mapM mk) arguments
+
+      return (maybe (pure noName) (fmap mk) arguments)
 
 goInductiveParameters ::
   forall r.