Refresh bound variable ids when substituting in Internal (#2501)

* Closes #2476 

Bound variable ids need to be refreshed to maintain the invariant that
each bound variable has a unique id.

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -49,7 +49,7 @@ unsupported thing = error ("Internal to Core: Not yet supported: " <> thing)
 mkIdentIndex :: Name -> Text
 mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
 
-fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
+fromInternal :: (Member NameIdGen k) => Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
   res <-
     execInfoTableBuilder emptyInfoTable
@@ -62,7 +62,7 @@ fromInternal i = do
         _coreResultInternalTypedResult = i
       }
   where
-    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable] r) => Sem r ()
+    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, NameIdGen] r) => Sem r ()
     f = do
       reserveLiteralIntToNatSymbol
       reserveLiteralIntToIntSymbol
@@ -77,7 +77,7 @@ fromInternal i = do
       setupLiteralIntToNat literalIntToNatNode
       setupLiteralIntToInt literalIntToIntNode
 
-fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
+fromInternalExpression :: (Member NameIdGen r) => CoreResult -> Internal.Expression -> Sem r Node
 fromInternalExpression res exp = do
   let modules = res ^. coreResultInternalTypedResult . InternalTyped.resultModules
   fmap snd
@@ -96,7 +96,7 @@ goModule = visit . Internal.ModuleIndex
 
 goModuleNoVisit ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, MVisit] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, MVisit] r) =>
   Internal.ModuleIndex ->
   Sem r ()
 goModuleNoVisit (Internal.ModuleIndex m) = do
@@ -109,7 +109,7 @@ goModuleNoVisit (Internal.ModuleIndex m) = do
 -- | predefine an inductive definition
 preInductiveDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
   Internal.InductiveDef ->
   Sem r PreInductiveDef
 preInductiveDef i = do
@@ -150,7 +150,7 @@ preInductiveDef i = do
 
 goInductiveDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
   PreInductiveDef ->
   Sem r ()
 goInductiveDef PreInductiveDef {..} = do
@@ -164,7 +164,7 @@ goInductiveDef PreInductiveDef {..} = do
 
 goConstructor ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
   Symbol ->
   Internal.ConstructorDef ->
   Sem r ConstructorInfo
@@ -226,7 +226,7 @@ goConstructor sym ctor = do
 
 goMutualBlock ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
   Internal.MutualBlock ->
   Sem r ()
 goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual
@@ -265,7 +265,7 @@ goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual
 
 preFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
   Internal.FunctionDef ->
   Sem r PreFunctionDef
 preFunctionDef f = do
@@ -334,7 +334,7 @@ preFunctionDef f = do
 
 goFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
   PreFunctionDef ->
   Sem r ()
 goFunctionDef PreFunctionDef {..} = do
@@ -353,12 +353,12 @@ goFunctionDef PreFunctionDef {..} = do
       let (is, _) = unfoldLambdas node
       setIdentArgs _preFunSym (map (^. lambdaLhsBinder) is)
 
-strongNormalizeHelper :: (Member (State InternalTyped.FunctionsTable) r) => Internal.Expression -> Sem r Internal.Expression
+strongNormalizeHelper :: (Members '[State InternalTyped.FunctionsTable, NameIdGen] r) => Internal.Expression -> Sem r Internal.Expression
 strongNormalizeHelper ty = evalState InternalTyped.iniState (InternalTyped.strongNormalize' ty)
 
 goType ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Reader IndexTable] r) =>
   Internal.Expression ->
   Sem r Type
 goType ty = do
@@ -368,7 +368,7 @@ goType ty = do
 
 mkFunBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Type -> -- converted type of the function
   Internal.FunctionDef ->
   Sem r Node
@@ -380,7 +380,7 @@ mkFunBody ty f =
 
 mkBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Type -> -- type of the function
   Location ->
   NonEmpty ([Internal.PatternArg], Internal.Expression) ->
@@ -467,7 +467,7 @@ mkBody ty loc clauses
 
 goCase ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.Case ->
   Sem r Node
 goCase c = do
@@ -501,7 +501,7 @@ goCase c = do
 
 goLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.Lambda ->
   Sem r Node
 goLambda l = do
@@ -510,7 +510,7 @@ goLambda l = do
 
 goLet ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.Let ->
   Sem r Node
 goLet l = goClauses (toList (l ^. Internal.letClauses))
@@ -548,7 +548,7 @@ goLet l = goClauses (toList (l ^. Internal.letClauses))
 
 goAxiomInductive ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
   Internal.AxiomDef ->
   Sem r ()
 goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
@@ -598,7 +598,7 @@ fromTopIndex = runReader initIndexTable
 
 goAxiomDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
   Internal.AxiomDef ->
   Sem r ()
 goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
@@ -701,7 +701,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
 
 fromPatternArg ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable, NameIdGen] r) =>
   Internal.PatternArg ->
   Sem r Pattern
 fromPatternArg pa = case pa ^. Internal.patternArgName of
@@ -785,7 +785,7 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of
 
 goPatternArgs ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Level -> -- the level of the first binder for the matched value
   Internal.Expression ->
   [Internal.PatternArg] ->
@@ -918,7 +918,7 @@ goIden i = do
 
 goExpression ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.Expression ->
   Sem r Node
 goExpression = \case
@@ -938,7 +938,7 @@ goExpression = \case
 
 goFunction ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   ([Internal.FunctionParameter], Internal.Expression) ->
   Sem r Node
 goFunction (params, returnTypeExpr) = go params
@@ -961,7 +961,7 @@ goFunction (params, returnTypeExpr) = go params
 
 goSimpleLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.SimpleLambda ->
   Sem r Node
 goSimpleLambda l = do
@@ -973,7 +973,7 @@ goSimpleLambda l = do
 
 goApplication ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
   Internal.Application ->
   Sem r Node
 goApplication a = do

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -4,6 +4,7 @@ import Data.Generics.Uniplate.Data hiding (holes)
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Internal.Data.LocalVars
+import Juvix.Compiler.Internal.Extra.Clonable
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 
@@ -153,14 +154,14 @@ holes = leafExpressions . _ExpressionHole
 hasHoles :: (HasExpressions a) => a -> Bool
 hasHoles = has holes
 
-subsHoles :: (HasExpressions a) => HashMap Hole Expression -> a -> a
+subsHoles :: forall a r. (HasExpressions a, Member NameIdGen r) => HashMap Hole Expression -> a -> Sem r a
-subsHoles s = over leafExpressions helper
+subsHoles s = leafExpressions helper
   where
-    helper :: Expression -> Expression
+    helper :: Expression -> Sem r Expression
     helper e = case e of
-      ExpressionHole h -> fromMaybe e (s ^. at h)
+      ExpressionHole h -> maybe (clone e) return (s ^. at h)
-      ExpressionInstanceHole h -> fromMaybe e (s ^. at h)
+      ExpressionInstanceHole h -> maybe (clone e) return (s ^. at h)
-      _ -> e
+      _ -> return e
 
 instance HasExpressions Example where
   leafExpressions f = traverseOf exampleExpression (leafExpressions f)
@@ -246,7 +247,7 @@ instance HasExpressions ConstructorDef where
           _inductiveConstructorPragmas
         }
 
-substituteIndParams :: [(InductiveParameter, Expression)] -> Expression -> Expression
+substituteIndParams :: forall r. (Member NameIdGen r) => [(InductiveParameter, Expression)] -> Expression -> Sem r Expression
 substituteIndParams = substitutionE . HashMap.fromList . map (first (^. inductiveParamName))
 
 typeAbstraction :: IsImplicit -> Name -> FunctionParameter
@@ -275,41 +276,6 @@ renameKind k l = HashMap.fromList [(n, toExpression (set nameKind k n)) | n <- l
 renameToSubsE :: Rename -> Subs
 renameToSubsE = fmap (ExpressionIden . IdenVar)
 
-class HasBinders a where
-  bindersTraversal :: Traversal' a VarName
-
-instance HasBinders PatternArg where
-  bindersTraversal f (PatternArg i n p) = PatternArg i <$> traverse f n <*> bindersTraversal f p
-
-instance HasBinders Pattern where
-  bindersTraversal f p = case p of
-    PatternVariable v -> PatternVariable <$> f v
-    PatternWildcardConstructor {} -> pure p
-    PatternConstructorApp a -> PatternConstructorApp <$> goApp f a
-    where
-      goApp :: Traversal' ConstructorApp VarName
-      goApp g = traverseOf constrAppParameters (traverse (bindersTraversal g))
-
-instance HasBinders FunctionParameter where
-  bindersTraversal = paramName . _Just
-
-instance HasBinders InductiveParameter where
-  bindersTraversal = inductiveParamName
-
-instance HasBinders SimpleBinder where
-  bindersTraversal = sbinderVar
-
-instance HasBinders FunctionDef where
-  bindersTraversal = funDefName
-
-instance HasBinders MutualBlockLet where
-  bindersTraversal = mutualLet . each . bindersTraversal
-
-instance HasBinders LetClause where
-  bindersTraversal f = \case
-    LetFunDef fun -> LetFunDef <$> bindersTraversal f fun
-    LetMutualBlock b -> LetMutualBlock <$> bindersTraversal f b
-
 inductiveTypeVarsAssoc :: (Foldable f) => InductiveDef -> f a -> HashMap VarName a
 inductiveTypeVarsAssoc def l
   | length vars < n = impossible
@@ -319,26 +285,26 @@ inductiveTypeVarsAssoc def l
     vars :: [VarName]
     vars = def ^.. inductiveParameters . each . inductiveParamName
 
-substitutionApp :: (Maybe Name, Expression) -> Expression -> Expression
+substitutionApp :: forall r. (Member NameIdGen r) => (Maybe Name, Expression) -> Expression -> Sem r Expression
 substitutionApp (mv, ty) = case mv of
-  Nothing -> id
+  Nothing -> return
   Just v -> substitutionE (HashMap.singleton v ty)
 
 localsToSubsE :: LocalVars -> Subs
 localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap
 
-substitutionE :: Subs -> Expression -> Expression
+substitutionE :: forall r. (Member NameIdGen r) => Subs -> Expression -> Sem r Expression
-substitutionE m = over leafExpressions goLeaf
+substitutionE m = leafExpressions goLeaf
   where
-    goLeaf :: Expression -> Expression
+    goLeaf :: Expression -> Sem r Expression
     goLeaf = \case
       ExpressionIden i -> goIden i
-      e -> e
+      e -> return e
-    goIden :: Iden -> Expression
+    goIden :: Iden -> Sem r Expression
     goIden i = case i of
       IdenVar v
-        | Just e <- HashMap.lookup v m -> e
+        | Just e <- HashMap.lookup v m -> clone e
-      _ -> ExpressionIden i
+      _ -> return $ ExpressionIden i
 
 smallUniverseE :: Interval -> Expression
 smallUniverseE = ExpressionUniverse . SmallUniverse
@@ -742,14 +708,6 @@ allTypeSignatures a =
     <> [f ^. axiomType | f@AxiomDef {} <- universeBi a]
     <> [f ^. inductiveType | f@InductiveDef {} <- universeBi a]
 
-idenName :: Lens' Iden Name
-idenName f = \case
-  IdenFunction g -> IdenFunction <$> f g
-  IdenConstructor c -> IdenConstructor <$> f c
-  IdenVar v -> IdenVar <$> f v
-  IdenInductive i -> IdenInductive <$> f i
-  IdenAxiom a -> IdenAxiom <$> f a
-
 explicitPatternArg :: Pattern -> PatternArg
 explicitPatternArg _patternArgPattern =
   PatternArg

src/Juvix/Compiler/Internal/Extra/Binders.hs

@@ -0,0 +1,39 @@
+module Juvix.Compiler.Internal.Extra.Binders where
+
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+class HasBinders a where
+  bindersTraversal :: Traversal' a VarName
+
+instance HasBinders PatternArg where
+  bindersTraversal f (PatternArg i n p) = PatternArg i <$> traverse f n <*> bindersTraversal f p
+
+instance HasBinders Pattern where
+  bindersTraversal f p = case p of
+    PatternVariable v -> PatternVariable <$> f v
+    PatternWildcardConstructor {} -> pure p
+    PatternConstructorApp a -> PatternConstructorApp <$> goApp f a
+    where
+      goApp :: Traversal' ConstructorApp VarName
+      goApp g = traverseOf constrAppParameters (traverse (bindersTraversal g))
+
+instance HasBinders FunctionParameter where
+  bindersTraversal = paramName . _Just
+
+instance HasBinders InductiveParameter where
+  bindersTraversal = inductiveParamName
+
+instance HasBinders SimpleBinder where
+  bindersTraversal = sbinderVar
+
+instance HasBinders FunctionDef where
+  bindersTraversal = funDefName
+
+instance HasBinders MutualBlockLet where
+  bindersTraversal = mutualLet . each . bindersTraversal
+
+instance HasBinders LetClause where
+  bindersTraversal f = \case
+    LetFunDef fun -> LetFunDef <$> bindersTraversal f fun
+    LetMutualBlock b -> LetMutualBlock <$> bindersTraversal f b

src/Juvix/Compiler/Internal/Extra/Clonable.hs

@@ -5,24 +5,20 @@ module Juvix.Compiler.Internal.Extra.Clonable
 where
 
 import Data.HashMap.Strict qualified as HashMap
-import Juvix.Compiler.Internal.Extra.Base
+import Juvix.Compiler.Internal.Extra.Binders
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 
 type FreshBindersContext = HashMap NameId NameId
 
-type HolesState = HashMap Hole Hole
-
 clone :: (Clonable a, Members '[NameIdGen] r) => a -> Sem r a
-clone = evalState iniState . runReader iniCtx . freshNameIds
+clone = runReader iniCtx . freshNameIds
   where
-    iniState :: HolesState
-    iniState = mempty
     iniCtx :: FreshBindersContext
     iniCtx = mempty
 
 class Clonable a where
-  freshNameIds :: (Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => a -> Sem r a
+  freshNameIds :: (Members '[Reader FreshBindersContext, NameIdGen] r) => a -> Sem r a
 
 instance Clonable Name where
   freshNameIds n = do
@@ -52,15 +48,7 @@ instance Clonable Literal where
   freshNameIds = return
 
 instance Clonable Hole where
-  freshNameIds h = do
+  freshNameIds = return
-    tbl <- get @HolesState
-    case tbl ^. at h of
-      Just h' -> return h'
-      Nothing -> do
-        uid' <- freshNameId
-        let h' = set holeId uid' h
-        modify' @HolesState (set (at h) (Just h'))
-        return h'
 
 instance Clonable SmallUniverse where
   freshNameIds = return
@@ -73,7 +61,7 @@ instance (Clonable a) => Clonable (Maybe a) where
 
 underBinder ::
   forall r a binding.
-  (HasBinders binding, Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) =>
+  (HasBinders binding, Members '[Reader FreshBindersContext, NameIdGen] r) =>
   binding ->
   (binding -> Sem r a) ->
   Sem r a
@@ -81,16 +69,16 @@ underBinder p f = underBinders [p] (f . headDef impossible)
 
 underBindersNonEmpty ::
   forall r a binding.
-  (HasBinders binding, Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) =>
+  (HasBinders binding, Members '[Reader FreshBindersContext, NameIdGen] r) =>
   NonEmpty binding ->
   (NonEmpty binding -> Sem r a) ->
   Sem r a
 underBindersNonEmpty p f = underBinders (toList p) (f . nonEmpty')
 
-underClonableBindersNonEmpty :: forall r a binding. (Clonable binding, HasBinders binding, Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => NonEmpty binding -> (NonEmpty binding -> Sem r a) -> Sem r a
+underClonableBindersNonEmpty :: forall r a binding. (Clonable binding, HasBinders binding, Members '[Reader FreshBindersContext, NameIdGen] r) => NonEmpty binding -> (NonEmpty binding -> Sem r a) -> Sem r a
 underClonableBindersNonEmpty ps0 f = underClonableBinders (toList ps0) (f . nonEmpty')
 
-underClonableBinders :: forall r a binding. (Clonable binding, HasBinders binding, Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => [binding] -> ([binding] -> Sem r a) -> Sem r a
+underClonableBinders :: forall r a binding. (Clonable binding, HasBinders binding, Members '[Reader FreshBindersContext, NameIdGen] r) => [binding] -> ([binding] -> Sem r a) -> Sem r a
 underClonableBinders binders f = do
   ctx <- ask @FreshBindersContext
   let bindersIds :: [NameId] = binders ^.. each . bindersTraversal . nameId
@@ -100,7 +88,7 @@ underClonableBinders binders f = do
     binders' <- freshNameIds binders
     f binders'
 
-underBinders :: forall r a binding. (HasBinders binding, Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => [binding] -> ([binding] -> Sem r a) -> Sem r a
+underBinders :: forall r a binding. (HasBinders binding, Members '[Reader FreshBindersContext, NameIdGen] r) => [binding] -> ([binding] -> Sem r a) -> Sem r a
 underBinders ps f = do
   ctx <- ask @FreshBindersContext
   (ctx', ps') <- runState ctx (mapM goBinders ps)
@@ -169,7 +157,7 @@ instance Clonable LetClause where
     LetMutualBlock m -> LetMutualBlock <$> freshNameIds m
 
 instance Clonable Let where
-  freshNameIds :: (Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => Let -> Sem r Let
+  freshNameIds :: (Members '[Reader FreshBindersContext, NameIdGen] r) => Let -> Sem r Let
   freshNameIds Let {..} = do
     underClonableBindersNonEmpty _letClauses $ \clauses' -> do
       e' <- freshNameIds _letExpression
@@ -220,7 +208,7 @@ instance Clonable Lambda where
         }
 
 instance Clonable Expression where
-  freshNameIds :: (Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => Expression -> Sem r Expression
+  freshNameIds :: (Members '[Reader FreshBindersContext, NameIdGen] r) => Expression -> Sem r Expression
   freshNameIds = \case
     ExpressionIden i -> ExpressionIden <$> freshNameIds i
     ExpressionApplication a -> ExpressionApplication <$> freshNameIds a
@@ -244,7 +232,7 @@ instance Clonable ArgInfo where
         }
 
 instance Clonable FunctionDef where
-  freshNameIds :: (Members '[State HolesState, Reader FreshBindersContext, NameIdGen] r) => FunctionDef -> Sem r FunctionDef
+  freshNameIds :: (Members '[Reader FreshBindersContext, NameIdGen] r) => FunctionDef -> Sem r FunctionDef
   freshNameIds fun@FunctionDef {..} = do
     ty' <- freshNameIds _funDefType
     underBinder fun $ \fun' -> do

src/Juvix/Compiler/Internal/Language.hs

@@ -530,3 +530,11 @@ instance HasLoc ConstructorApp where
     case last <$> nonEmpty _constrAppParameters of
       Just p -> getLoc _constrAppConstructor <> getLoc p
       Nothing -> getLoc _constrAppConstructor
+
+idenName :: Lens' Iden Name
+idenName f = \case
+  IdenFunction g -> IdenFunction <$> f g
+  IdenConstructor c -> IdenConstructor <$> f c
+  IdenVar v -> IdenVar <$> f v
+  IdenInductive i -> IdenInductive <$> f i
+  IdenAxiom a -> IdenAxiom <$> f a

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -784,13 +784,13 @@ goExpression = \case
                   _namedAppArgs = nonEmpty' $ createArgumentBlocks (sig ^. nameSignatureArgs)
                 }
         e <- goNamedApplication napp'
-        let expr =
+        expr <-
-              Internal.substitutionE updateKind
+          Internal.substitutionE updateKind
-                . Internal.ExpressionLet
+            . Internal.ExpressionLet
-                $ Internal.Let
+            $ Internal.Let
-                  { _letClauses = cls,
+              { _letClauses = cls,
-                    _letExpression = e
+                _letExpression = e
-                  }
+              }
         Internal.clone expr
         where
           goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
@@ -849,13 +849,13 @@ goExpression = \case
           argNames :: NonEmpty Internal.ApplicationArg = mkAppArg <$> a ^. dnamedAppArgs
           app = Internal.foldApplication (Internal.toExpression fun) (toList argNames)
       clauses <- mapM mkClause (a ^. dnamedAppArgs)
-      let expr =
+      expr <-
-            Internal.substitutionE updateKind $
+        Internal.substitutionE updateKind $
-              Internal.ExpressionLet
+          Internal.ExpressionLet
-                Internal.Let
+            Internal.Let
-                  { _letExpression = app,
+              { _letExpression = app,
-                    _letClauses = clauses
+                _letClauses = clauses
-                  }
+              }
       Internal.clone expr
       where
         mkClause :: Arg -> Sem r Internal.LetClause

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -767,13 +767,13 @@ checkExpression hintArity expr = case expr of
                       }
               clauses :: NonEmpty Internal.LetClause <- nonEmpty' . Internal.mkLetClauses <$> mapM mkClause args'
               let app = foldApplication (toExpression fun0) (map mkAppArg namedArgs)
-                  letexpr =
+              letexpr <-
-                    Internal.substitutionE (renameKind KNameFunction (map (^. insertedArgName) namedArgs)) $
+                Internal.substitutionE (renameKind KNameFunction (map (^. insertedArgName) namedArgs)) $
-                      ExpressionLet
+                  ExpressionLet
-                        Let
+                    Let
-                          { _letClauses = clauses,
+                      { _letClauses = clauses,
-                            _letExpression = app
+                        _letExpression = app
-                          }
+                      }
               Internal.clone letexpr
 
         helper :: Interval -> Arity -> Sem r [ApplicationArg]

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -257,7 +257,7 @@ checkDefType ty = checkIsType loc ty
 
 checkInstanceType ::
   forall r.
-  (Members '[Error TypeCheckerError, Reader InfoTable, Inference] r) =>
+  (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen] r) =>
   FunctionDef ->
   Sem r ()
 checkInstanceType FunctionDef {..} = case mi of
@@ -401,7 +401,7 @@ resolveInstanceHoles s = do
   (hs, e) <- runOutputList s
   ts <- mapM goResolve hs
   let subs = HashMap.fromList (zipExact (map (^. typedHoleHole) hs) ts)
-  return $ subsHoles subs e
+  subsHoles subs e
   where
     goResolve :: TypedHole -> Sem r Expression
     goResolve h@TypedHole {..} = do
@@ -494,7 +494,7 @@ checkClause clauseType clausePats body = do
   locals0 <- ask
   (localsPats, (checkedPatterns, bodyType)) <- helper clausePats clauseType
   let locals' = locals0 <> localsPats
-      bodyTy' = substitutionE (localsToSubsE locals') bodyType
+  bodyTy' <- substitutionE (localsToSubsE locals') bodyType
   checkedBody <- local (const locals') (checkExpression bodyTy' body)
   return (checkedPatterns, checkedBody)
   where
@@ -559,8 +559,8 @@ checkPattern = go
     go argTy patArg = do
       matchIsImplicit (argTy ^. paramImplicit) patArg
       tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get
-      let ty = substitutionE tyVarMap (argTy ^. paramType)
+      ty <- substitutionE tyVarMap (argTy ^. paramType)
-          pat = patArg ^. patternArgPattern
+      let pat = patArg ^. patternArgPattern
           name = patArg ^. patternArgName
       whenJust name (\n -> addVar n ty argTy)
       pat' <- case pat of
@@ -618,8 +618,8 @@ checkPattern = go
         goConstr :: Iden -> ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ConstructorApp
         goConstr inductivename app@(ConstructorApp c ps _) ctx = do
           (_, psTys) <- constructorArgTypes <$> lookupConstructor c
-          let psTys' = map (substituteIndParams ctx) psTys
+          psTys' <- mapM (substituteIndParams ctx) psTys
-              expectedNum = length psTys
+          let expectedNum = length psTys
               w = map unnamedParameter psTys'
           when (expectedNum /= length ps) (throw (appErr app expectedNum))
           pis <- zipWithM go w ps
@@ -912,6 +912,7 @@ inferExpression' hint e = case e of
                         <> ppTrace (Application l r iapp)
                     )
                 )
+              ty <- substitutionApp (paraName, r') funR
               return
                 TypedExpression
                   { _typedExpression =
@@ -921,7 +922,7 @@ inferExpression' hint e = case e of
                             _appRight = r',
                             _appImplicit = iapp
                           },
-                    _typedType = substitutionApp (paraName, r') funR
+                    _typedType = ty
                   }
             ExpressionHole h -> do
               fun <- ExpressionFunction <$> holeRefineToFunction h

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs

@@ -125,7 +125,7 @@ queryMetavarFinal h = do
     Just (ExpressionHole h') -> queryMetavarFinal h'
     _ -> return m
 
-strongNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
+strongNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression
 strongNormalize' = go
   where
     go :: Expression -> Sem r Expression
@@ -223,7 +223,8 @@ strongNormalize' = go
       l' <- go l
       case l' of
         ExpressionSimpleLambda (SimpleLambda (SimpleBinder lamVar _) lamBody) -> do
-          go (substitutionE (HashMap.singleton lamVar r) lamBody)
+          b' <- substitutionE (HashMap.singleton lamVar r) lamBody
+          go b'
         _ -> do
           r' <- go r
           return (ExpressionApplication (Application l' r' i))
@@ -239,7 +240,7 @@ strongNormalize' = go
       where
         i' = ExpressionIden i
 
-weakNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
+weakNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression
 weakNormalize' = go
   where
     go :: Expression -> Sem r Expression
@@ -270,7 +271,8 @@ weakNormalize' = go
       l' <- go l
       case l' of
         ExpressionSimpleLambda (SimpleLambda (SimpleBinder lamVar _) lamBody) -> do
-          go (substitutionE (HashMap.singleton lamVar r) lamBody)
+          b' <- substitutionE (HashMap.singleton lamVar r) lamBody
+          go b'
         _ -> return (ExpressionApplication (Application l' r i))
     goHole :: Hole -> Sem r Expression
     goHole h = do
@@ -296,7 +298,7 @@ queryMetavar' h = do
     Just (Refined e) -> return (Just e)
 
 re ::
-  (Members '[State FunctionsTable, Error TypeCheckerError] r) =>
+  (Members '[State FunctionsTable, Error TypeCheckerError, NameIdGen] r) =>
   Sem (Inference ': r) a ->
   Sem (State InferenceState ': r) a
 re = reinterpret $ \case
@@ -311,14 +313,14 @@ re = reinterpret $ \case
     registerIdenType' i ty = modify (over inferenceIdens (HashMap.insert (i ^. nameId) ty))
 
     -- Supports alpha equivalence.
-    matchTypes' :: (Members '[State InferenceState, State FunctionsTable, Error TypeCheckerError] r) => Expression -> Expression -> Sem r (Maybe MatchError)
+    matchTypes' :: (Members '[State InferenceState, State FunctionsTable, Error TypeCheckerError, NameIdGen] r) => Expression -> Expression -> Sem r (Maybe MatchError)
     matchTypes' ty = runReader ini . go ty
       where
         ini :: HashMap VarName VarName
         ini = mempty
         go ::
           forall r.
-          (Members '[State InferenceState, Reader (HashMap VarName VarName), State FunctionsTable, Error TypeCheckerError] r) =>
+          (Members '[State InferenceState, Reader (HashMap VarName VarName), State FunctionsTable, Error TypeCheckerError, NameIdGen] r) =>
           Expression ->
           Expression ->
           Sem r (Maybe MatchError)
@@ -478,20 +480,20 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
     err = return False
 
 runInferenceDefs ::
-  (Members '[Termination, HighlightBuilder, Error TypeCheckerError, State FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
+  (Members '[Termination, HighlightBuilder, Error TypeCheckerError, State FunctionsTable, State TypesTable, NameIdGen] r, HasExpressions funDef) =>
   Sem (Inference ': r) (NonEmpty funDef) ->
   Sem r (NonEmpty funDef)
 runInferenceDefs a = do
   (finalState, expr) <- runState iniState (re a)
   (subs, idens) <- closeState finalState
-  let idens' = subsHoles subs <$> idens
+  idens' <- mapM (subsHoles subs) idens
-      stash' = map (subsHoles subs) (finalState ^. inferenceFunctionsStash)
+  stash' <- mapM (subsHoles subs) (finalState ^. inferenceFunctionsStash)
   forM_ stash' registerFunctionDef
   addIdens idens'
-  return (subsHoles subs <$> expr)
+  mapM (subsHoles subs) expr
 
 runInferenceDef ::
-  (Members '[Termination, HighlightBuilder, Error TypeCheckerError, State FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
+  (Members '[Termination, HighlightBuilder, Error TypeCheckerError, State FunctionsTable, State TypesTable, NameIdGen] r, HasExpressions funDef) =>
   Sem (Inference ': r) funDef ->
   Sem r funDef
 runInferenceDef = fmap head . runInferenceDefs . fmap pure
@@ -510,14 +512,14 @@ addIdens idens = do
 --
 -- Throws an error if the return type is Type and it does not satisfy the
 -- above conditions.
-functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
+functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError, NameIdGen] r') => FunctionDef -> Sem r' (Maybe Expression)
 functionDefEval f = do
   (params :: [FunctionParameter], ret :: Expression) <- unfoldFunType <$> strongNorm (f ^. funDefType)
   r <- runFail (goTop params (canBeUniverse ret))
   when (isNothing r && isUniverse ret) (throw (ErrUnsupportedTypeFunction (UnsupportedTypeFunction f)))
   return r
   where
-    strongNorm :: (Members '[State FunctionsTable] r) => Expression -> Sem r Expression
+    strongNorm :: (Members '[State FunctionsTable, NameIdGen] r) => Expression -> Sem r Expression
     strongNorm = evalState iniState . strongNormalize'
 
     isUniverse :: Expression -> Bool
@@ -576,6 +578,6 @@ functionDefEval f = do
                 | Implicit <- p ^. patternArgIsImplicit -> fail
                 | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty)
 
-registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError, Termination] r) => FunctionDef -> Sem r ()
+registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError, NameIdGen, Termination] r) => FunctionDef -> Sem r ()
 registerFunctionDef f = whenJustM (functionDefEval f) $ \e ->
   modify (over functionsTable (HashMap.insert (f ^. funDefName) e))

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs

@@ -48,7 +48,7 @@ resolveTraitInstance TypedHole {..} = do
 
 subsumingInstances ::
   forall r.
-  (Members '[Error TypeCheckerError, Inference] r) =>
+  (Members '[Error TypeCheckerError, Inference, NameIdGen] r) =>
   InstanceTable ->
   InstanceInfo ->
   Sem r [(InstanceInfo)]
@@ -62,29 +62,37 @@ subsumingInstances tab InstanceInfo {..} = do
 -- Local functions
 -------------------------------------------------------------------------------------
 
-substitutionI :: SubsI -> InstanceParam -> InstanceParam
+substitutionI :: (Member NameIdGen r) => SubsI -> InstanceParam -> Sem r InstanceParam
 substitutionI subs p = case p of
-  InstanceParamVar {} -> p
+  InstanceParamVar {} -> return p
-  InstanceParamApp InstanceApp {..} ->
+  InstanceParamApp InstanceApp {..} -> do
-    InstanceParamApp
+    args <- mapM (substitutionI subs) _instanceAppArgs
-      InstanceApp
+    e <- substitutionE (subsIToE subs) _instanceAppExpression
-        { _instanceAppHead,
+    return $
-          _instanceAppArgs = map (substitutionI subs) _instanceAppArgs,
+      InstanceParamApp
-          _instanceAppExpression = substitutionE (subsIToE subs) _instanceAppExpression
+        InstanceApp
-        }
+          { _instanceAppHead,
-  InstanceParamFun InstanceFun {..} ->
+            _instanceAppArgs = args,
-    InstanceParamFun
+            _instanceAppExpression = e
-      InstanceFun
+          }
-        { _instanceFunLeft = substitutionI subs _instanceFunLeft,
+  InstanceParamFun InstanceFun {..} -> do
-          _instanceFunRight = substitutionI subs _instanceFunRight,
+    l <- substitutionI subs _instanceFunLeft
-          _instanceFunExpression = substitutionE (subsIToE subs) _instanceFunExpression
+    r <- substitutionI subs _instanceFunRight
-        }
+    e <- substitutionE (subsIToE subs) _instanceFunExpression
-  InstanceParamHole {} -> p
+    return $
+      InstanceParamFun
+        InstanceFun
+          { _instanceFunLeft = l,
+            _instanceFunRight = r,
+            _instanceFunExpression = e
+          }
+  InstanceParamHole {} -> return p
   InstanceParamMeta v
     | Just p' <- HashMap.lookup v subs ->
-        p'
+        -- we don't need to clone here because `InstanceParam` doesn't have binders
+        return p'
     | otherwise ->
-        p
+        return p
 
 instanceFromTypedExpression' :: InfoTable -> TypedExpression -> Maybe InstanceInfo
 instanceFromTypedExpression' tbl e = do
@@ -155,7 +163,7 @@ expandArity loc subs params e = case params of
 
 lookupInstance' ::
   forall r.
-  (Member Inference r) =>
+  (Members '[Inference, NameIdGen] r) =>
   [Name] ->
   Bool ->
   CoercionTable ->
@@ -191,7 +199,7 @@ lookupInstance' visited canFillHoles ctab tab name params
           and <$> sequence (zipWithExact goMatch _coercionInfoParams params)
       failUnless b
       let name' = _coercionInfoTarget ^. instanceAppHead
-          args' = map (substitutionI si) (_coercionInfoTarget ^. instanceAppArgs)
+      args' <- mapM (substitutionI si) (_coercionInfoTarget ^. instanceAppArgs)
       is <- lookupInstance' (name : visited) canFillHoles ctab tab name' args'
       return $ map (first3 ((ci, si) :)) is
 
@@ -238,7 +246,7 @@ lookupInstance' visited canFillHoles ctab tab name params
 
 lookupInstance ::
   forall r.
-  (Members '[Error TypeCheckerError, Inference] r) =>
+  (Members '[Error TypeCheckerError, Inference, NameIdGen] r) =>
   CoercionTable ->
   InstanceTable ->
   Expression ->

src/Juvix/Compiler/Pipeline/Repl.hs

@@ -161,7 +161,8 @@ fromInternalImport :: (Members '[State Artifacts] r) => Internal.Import -> Sem r
 fromInternalImport i = do
   artiTable <- gets (^. artifactInternalTypedTable)
   let table = Internal.buildTable [i ^. Internal.importModule . Internal.moduleIxModule] <> artiTable
-  runReader table
+  runNameIdGenArtifacts
+    . runReader table
     . runCoreInfoTableBuilderArtifacts
     . runFunctionsTableArtifacts
     . readerTypesTableArtifacts
@@ -173,7 +174,8 @@ fromInternalImport i = do
 fromInternalExpression :: (Members '[State Artifacts] r) => Internal.Expression -> Sem r Core.Node
 fromInternalExpression exp = do
   typedTable <- gets (^. artifactInternalTypedTable)
-  runReader typedTable
+  runNameIdGenArtifacts
+    . runReader typedTable
     . tmpCoreInfoTableBuilderArtifacts
     . runFunctionsTableArtifacts
     . readerTypesTableArtifacts