From 9627efea4bd7f99fcfb2141aeaaf15e48cedc1a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 11:42:35 +0200
Subject: [PATCH 01/11] Add test case

---
 examples/pos/codepos.check  | 2 ++
 examples/pos/codepos.effekt | 7 +++++++
 2 files changed, 9 insertions(+)
 create mode 100644 examples/pos/codepos.check
 create mode 100644 examples/pos/codepos.effekt

diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
new file mode 100644
index 000000000..6160c070f
--- /dev/null
+++ b/examples/pos/codepos.check
@@ -0,0 +1,2 @@
+examples/pos/codepos.effekt:82-96
+examples/pos/codepos.effekt:99-113
\ No newline at end of file
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
new file mode 100644
index 000000000..fa519df95
--- /dev/null
+++ b/examples/pos/codepos.effekt
@@ -0,0 +1,7 @@
+def printCodepos(): Unit / Codepos = {
+  println(do codepos())
+}
+def main() = {
+  printCodepos()
+  printCodepos()
+}
\ No newline at end of file

From 4b52a8bac2a548f1d134f03ac7e0b47eb3f462b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 11:46:30 +0200
Subject: [PATCH 02/11] Implicitly handle Codepos at each callsite (if it is
 required)

---
 .../shared/src/main/scala/effekt/Typer.scala  |  5 ++-
 .../effekt/source/ExplicitCapabilities.scala  | 36 +++++++++++++++++--
 .../main/scala/effekt/symbols/builtins.scala  | 18 ++++++++--
 .../scala/effekt/typer/CapabilityScope.scala  |  9 +++--
 4 files changed, 60 insertions(+), 8 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Typer.scala b/effekt/shared/src/main/scala/effekt/Typer.scala
index f9c345af2..a65ff5abd 100644
--- a/effekt/shared/src/main/scala/effekt/Typer.scala
+++ b/effekt/shared/src/main/scala/effekt/Typer.scala
@@ -62,6 +62,9 @@ object Typer extends Phase[NameResolved, Typechecked] {
         Context in {
           Context.withUnificationScope {
             flowingInto(builtins.toplevelCaptures) {
+              // first, annotate root terms
+              Context.bind(builtins.Codepos.codepos, builtins.Codepos.codepos.toType)
+
               // We split the type-checking of definitions into "pre-check" and "check"
               // to allow mutually recursive defs
               tree.defs.foreach { d => precheckDef(d) }
@@ -1511,7 +1514,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
 
     // We add return effects last to have more information at this point to
     // concretize the effect.
-    effs = effs ++ Effects(retEffs)
+    effs = effs ++ Effects(retEffs.filterNot { p => p.typeConstructor == builtins.Codepos.interface })
 
     // annotate call node with inferred type arguments
     Context.annotateTypeArgs(call, typeArgs)
diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index 91a4ce270..a730b4a4e 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -39,6 +39,23 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       extDef.copy(bodies = rewrittenBodies)
   }
 
+  def codeposImplFor(span: Span)(using Context): Term = {
+    val pos = s"${span.source.name}:${span.from}-${span.to}"
+    val sp = span.synthesized
+    // now, synthesize an object that always returns the current position
+    val idIfce = IdRef(Nil, builtins.Codepos.interface.name.name, sp)
+    Context.annotate(Annotations.Symbol, idIfce, builtins.Codepos.interface)
+    val idOp = IdRef(Nil, builtins.Codepos.codepos.name.name, sp)
+    Context.annotate(Annotations.Symbol, idOp, builtins.Codepos.codepos)
+    val impl = Implementation(TypeRef(idIfce, Many(Nil, sp), sp),
+      List(OpClause(idOp,
+        Nil, Nil, Nil, Some(Effectful(ValueTypeTree(builtins.TString, sp), source.Effects(Nil, sp), sp)),
+        Stmt.Return(Term.Literal(pos, builtins.TString, sp), sp),
+        IdDef("resume", sp), sp)), sp)
+    Context.annotate(Annotations.InferredBlockType, impl, builtins.Codepos.tpe)
+    New(impl, sp)
+  }
+
   override def expr(using Context) = {
 
     // an effect call -- translate to method call on the inferred capability
@@ -53,7 +70,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       val others = Context.annotation(Annotations.CapabilityArguments, c)
 
       // the remaining capabilities are provided as arguments
-      val capabilityArgs = others.map(referenceToCapability)
+      val capabilityArgs = others.map{
+        case p if p.tpe.contains(builtins.Codepos.tpe) =>
+          codeposImplFor(span)
+        case p => referenceToCapability(p)
+      }
 
       val typeArguments = Context.annotation(Annotations.TypeArguments, c)
       val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }
@@ -70,7 +91,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       val blockArgs = bargs.map { a => rewrite(a) }
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
-      val capabilityArgs = capabilities.map(referenceToCapability)
+      val capabilityArgs = capabilities.map{
+        case p if p.tpe.contains(builtins.Codepos.tpe) =>
+          codeposImplFor(span)
+        case p => referenceToCapability(p)
+      }
 
       val typeArguments = Context.annotation(Annotations.TypeArguments, c)
       val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }
@@ -85,7 +110,12 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       val blockArgs = bargs.map { a => rewrite(a) }
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
-      val capabilityArgs = capabilities.map(referenceToCapability)
+      val capabilityArgs = capabilities.map{
+        case p if p.tpe.contains(builtins.Codepos.tpe) =>
+          codeposImplFor(span)
+        case p =>
+          referenceToCapability(p)
+      }
 
       val typeArguments = Context.annotation(Annotations.TypeArguments, c)
       val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }
diff --git a/effekt/shared/src/main/scala/effekt/symbols/builtins.scala b/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
index 682871a9e..f44761db2 100644
--- a/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
+++ b/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
@@ -56,6 +56,15 @@ object builtins {
   val GlobalSymbol = Interface(Name.local("Global"), Nil, Nil, decl = NoSource)
   val GlobalCapability = ExternResource(name("global"), InterfaceType(GlobalSymbol, Nil), Resource(name("global")), decl = NoSource)
 
+  object Codepos {
+    val interface: Interface = Interface(Name.local("Codepos"), Nil, Nil, decl = NoSource)
+    val tpe: BlockType.InterfaceType = BlockType.InterfaceType(interface, Nil)
+    val codepos = Operation(name("codepos"), Nil, Nil, Nil, TString, Effects.Pure, interface, decl = NoSource)
+    val capture: Capture = Capture.Resource(Name.local("codepos"))
+    val param = BlockParam(Name.local("codeposCap"), Some(tpe), capture, decl = NoSource)
+    interface.operations = List(codepos)
+  }
+
   object TState {
     val S: TypeParam = TypeParam(Name.local("S"))
     val interface: Interface = Interface(Name.local("Ref"), List(S), Nil, decl = NoSource)
@@ -86,7 +95,8 @@ object builtins {
     "Any" -> TopSymbol,
     "Nothing" -> BottomSymbol,
     "IO" -> IOSymbol,
-    "Region" -> RegionSymbol
+    "Region" -> RegionSymbol,
+    "Codepos" -> Codepos.interface
   )
 
   val rootCaptures: Map[String, Capture] = Map(
@@ -95,11 +105,15 @@ object builtins {
     "global" -> GlobalCapability.capture
   )
 
+  val rootTerms: Map[String, Set[TermSymbol]] = Map(
+    "codepos" -> Set(Codepos.codepos)
+  )
+
   // captures which are allowed on the toplevel
   val toplevelCaptures: CaptureSet = CaptureSet() // CaptureSet(IOCapability.capture, GlobalCapability.capture)
 
   lazy val rootBindings: Bindings =
-    Bindings(Map.empty, rootTypes, rootCaptures, Map("effekt" -> Bindings(Map.empty, rootTypes, rootCaptures, Map.empty)))
+    Bindings(rootTerms, rootTypes, rootCaptures, Map("effekt" -> Bindings(Map.empty, rootTypes, rootCaptures, Map.empty)))
 
   // All built-in symbols that can occur in core programs
   val coreBuiltins: Map[String, symbols.Symbol] = {
diff --git a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
index 5aa207aec..278b7f216 100644
--- a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
+++ b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
@@ -19,8 +19,13 @@ case object GlobalCapabilityScope extends CapabilityScope {
   def parent: CapabilityScope = sys error "No parent"
   // If we try to find a capability for an effect that is known to be unhandled (that is no outer scope could
   // potentially handle it, then we raise an error.
-  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam =
-    C.abort(pretty"Effect ${tpe} is not allowed in this context.")
+  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam = {
+    if (tpe.typeConstructor == symbols.builtins.Codepos.interface) {
+      symbols.builtins.Codepos.param 
+    } else {
+      C.abort(pretty"Effect ${tpe} is not allowed in this context.")
+    }
+  }
   def relevantInScopeFor(tpe: symbols.InterfaceType)(using C: Context): Set[symbols.InterfaceType] = Set.empty
 }
 

From 53be75a7b357beac50bc27c5d8b5d339491616a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 13:36:44 +0200
Subject: [PATCH 03/11] Instead declare effect in stdlib and just match on name

---
 .../shared/src/main/scala/effekt/Typer.scala  |  5 +---
 .../effekt/source/ExplicitCapabilities.scala  | 29 +++++++++++--------
 .../main/scala/effekt/symbols/builtins.scala  | 18 ++----------
 .../scala/effekt/typer/CapabilityScope.scala  |  9 ++----
 examples/pos/codepos.effekt                   |  2 +-
 libraries/common/effekt.effekt                |  2 +-
 6 files changed, 24 insertions(+), 41 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Typer.scala b/effekt/shared/src/main/scala/effekt/Typer.scala
index a65ff5abd..7f70c8264 100644
--- a/effekt/shared/src/main/scala/effekt/Typer.scala
+++ b/effekt/shared/src/main/scala/effekt/Typer.scala
@@ -62,9 +62,6 @@ object Typer extends Phase[NameResolved, Typechecked] {
         Context in {
           Context.withUnificationScope {
             flowingInto(builtins.toplevelCaptures) {
-              // first, annotate root terms
-              Context.bind(builtins.Codepos.codepos, builtins.Codepos.codepos.toType)
-
               // We split the type-checking of definitions into "pre-check" and "check"
               // to allow mutually recursive defs
               tree.defs.foreach { d => precheckDef(d) }
@@ -1514,7 +1511,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
 
     // We add return effects last to have more information at this point to
     // concretize the effect.
-    effs = effs ++ Effects(retEffs.filterNot { p => p.typeConstructor == builtins.Codepos.interface })
+    effs = effs ++ Effects(retEffs.filterNot { p => p.name.name == "Codepos" })
 
     // annotate call node with inferred type arguments
     Context.annotateTypeArgs(call, typeArgs)
diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index a730b4a4e..ad13f7895 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -39,20 +39,25 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       extDef.copy(bodies = rewrittenBodies)
   }
 
-  def codeposImplFor(span: Span)(using Context): Term = {
+  def codeposImplFor(span: Span, p: TrackedParam.BlockParam)(using Context): Term = {
     val pos = s"${span.source.name}:${span.from}-${span.to}"
     val sp = span.synthesized
+    val (ifce, op, tpe) = p.tpe match {
+      case Some(tpe @ BlockType.InterfaceType(ifce @ BlockTypeConstructor.Interface(name, Nil, List(op), decl), Nil)) =>
+        (ifce, op, tpe)
+      case _ => Context.abort("Could not find Codepos interface with compatible type")
+    }
     // now, synthesize an object that always returns the current position
-    val idIfce = IdRef(Nil, builtins.Codepos.interface.name.name, sp)
-    Context.annotate(Annotations.Symbol, idIfce, builtins.Codepos.interface)
-    val idOp = IdRef(Nil, builtins.Codepos.codepos.name.name, sp)
-    Context.annotate(Annotations.Symbol, idOp, builtins.Codepos.codepos)
+    val idIfce = IdRef(Nil, "Codepos", sp)
+    Context.annotate(Annotations.Symbol, idIfce, ifce)
+    val idOp = IdRef(Nil, op.name.name, sp)
+    Context.annotate(Annotations.Symbol, idOp, op)
     val impl = Implementation(TypeRef(idIfce, Many(Nil, sp), sp),
       List(OpClause(idOp,
         Nil, Nil, Nil, Some(Effectful(ValueTypeTree(builtins.TString, sp), source.Effects(Nil, sp), sp)),
         Stmt.Return(Term.Literal(pos, builtins.TString, sp), sp),
         IdDef("resume", sp), sp)), sp)
-    Context.annotate(Annotations.InferredBlockType, impl, builtins.Codepos.tpe)
+    Context.annotate(Annotations.InferredBlockType, impl, tpe)
     New(impl, sp)
   }
 
@@ -71,8 +76,8 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       // the remaining capabilities are provided as arguments
       val capabilityArgs = others.map{
-        case p if p.tpe.contains(builtins.Codepos.tpe) =>
-          codeposImplFor(span)
+        case p if p.name.name == "Codepos" =>
+          codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
 
@@ -92,8 +97,8 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.tpe.contains(builtins.Codepos.tpe) =>
-          codeposImplFor(span)
+        case p if p.name.name == "Codepos" =>
+          codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
 
@@ -111,8 +116,8 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.tpe.contains(builtins.Codepos.tpe) =>
-          codeposImplFor(span)
+        case p if p.name.name == "Codepos" =>
+          codeposImplFor(span, p)
         case p =>
           referenceToCapability(p)
       }
diff --git a/effekt/shared/src/main/scala/effekt/symbols/builtins.scala b/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
index f44761db2..682871a9e 100644
--- a/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
+++ b/effekt/shared/src/main/scala/effekt/symbols/builtins.scala
@@ -56,15 +56,6 @@ object builtins {
   val GlobalSymbol = Interface(Name.local("Global"), Nil, Nil, decl = NoSource)
   val GlobalCapability = ExternResource(name("global"), InterfaceType(GlobalSymbol, Nil), Resource(name("global")), decl = NoSource)
 
-  object Codepos {
-    val interface: Interface = Interface(Name.local("Codepos"), Nil, Nil, decl = NoSource)
-    val tpe: BlockType.InterfaceType = BlockType.InterfaceType(interface, Nil)
-    val codepos = Operation(name("codepos"), Nil, Nil, Nil, TString, Effects.Pure, interface, decl = NoSource)
-    val capture: Capture = Capture.Resource(Name.local("codepos"))
-    val param = BlockParam(Name.local("codeposCap"), Some(tpe), capture, decl = NoSource)
-    interface.operations = List(codepos)
-  }
-
   object TState {
     val S: TypeParam = TypeParam(Name.local("S"))
     val interface: Interface = Interface(Name.local("Ref"), List(S), Nil, decl = NoSource)
@@ -95,8 +86,7 @@ object builtins {
     "Any" -> TopSymbol,
     "Nothing" -> BottomSymbol,
     "IO" -> IOSymbol,
-    "Region" -> RegionSymbol,
-    "Codepos" -> Codepos.interface
+    "Region" -> RegionSymbol
   )
 
   val rootCaptures: Map[String, Capture] = Map(
@@ -105,15 +95,11 @@ object builtins {
     "global" -> GlobalCapability.capture
   )
 
-  val rootTerms: Map[String, Set[TermSymbol]] = Map(
-    "codepos" -> Set(Codepos.codepos)
-  )
-
   // captures which are allowed on the toplevel
   val toplevelCaptures: CaptureSet = CaptureSet() // CaptureSet(IOCapability.capture, GlobalCapability.capture)
 
   lazy val rootBindings: Bindings =
-    Bindings(rootTerms, rootTypes, rootCaptures, Map("effekt" -> Bindings(Map.empty, rootTypes, rootCaptures, Map.empty)))
+    Bindings(Map.empty, rootTypes, rootCaptures, Map("effekt" -> Bindings(Map.empty, rootTypes, rootCaptures, Map.empty)))
 
   // All built-in symbols that can occur in core programs
   val coreBuiltins: Map[String, symbols.Symbol] = {
diff --git a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
index 278b7f216..5aa207aec 100644
--- a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
+++ b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
@@ -19,13 +19,8 @@ case object GlobalCapabilityScope extends CapabilityScope {
   def parent: CapabilityScope = sys error "No parent"
   // If we try to find a capability for an effect that is known to be unhandled (that is no outer scope could
   // potentially handle it, then we raise an error.
-  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam = {
-    if (tpe.typeConstructor == symbols.builtins.Codepos.interface) {
-      symbols.builtins.Codepos.param 
-    } else {
-      C.abort(pretty"Effect ${tpe} is not allowed in this context.")
-    }
-  }
+  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam =
+    C.abort(pretty"Effect ${tpe} is not allowed in this context.")
   def relevantInScopeFor(tpe: symbols.InterfaceType)(using C: Context): Set[symbols.InterfaceType] = Set.empty
 }
 
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
index fa519df95..2ac07d9ad 100644
--- a/examples/pos/codepos.effekt
+++ b/examples/pos/codepos.effekt
@@ -1,5 +1,5 @@
 def printCodepos(): Unit / Codepos = {
-  println(do codepos())
+  println(do Codepos())
 }
 def main() = {
   printCodepos()
diff --git a/libraries/common/effekt.effekt b/libraries/common/effekt.effekt
index 04f6ae549..5a62bcfa6 100644
--- a/libraries/common/effekt.effekt
+++ b/libraries/common/effekt.effekt
@@ -832,4 +832,4 @@ effect write(s: String): Unit
 
 effect splice[A](x: A): Unit
 
-
+effect Codepos(): String
\ No newline at end of file

From d99d596a4ab73915d6e7d6217768e72636336b5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 13:38:41 +0200
Subject: [PATCH 04/11] Documentation, Codepos -> codepos

---
 effekt/shared/src/main/scala/effekt/Typer.scala        |  2 +-
 .../scala/effekt/source/ExplicitCapabilities.scala     | 10 +++++-----
 examples/pos/codepos.effekt                            |  4 ++--
 libraries/common/effekt.effekt                         |  6 +++++-
 4 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Typer.scala b/effekt/shared/src/main/scala/effekt/Typer.scala
index 7f70c8264..f73407555 100644
--- a/effekt/shared/src/main/scala/effekt/Typer.scala
+++ b/effekt/shared/src/main/scala/effekt/Typer.scala
@@ -1511,7 +1511,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
 
     // We add return effects last to have more information at this point to
     // concretize the effect.
-    effs = effs ++ Effects(retEffs.filterNot { p => p.name.name == "Codepos" })
+    effs = effs ++ Effects(retEffs.filterNot { p => p.name.name == "codepos" })
 
     // annotate call node with inferred type arguments
     Context.annotateTypeArgs(call, typeArgs)
diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index ad13f7895..460b97ed6 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -45,10 +45,10 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
     val (ifce, op, tpe) = p.tpe match {
       case Some(tpe @ BlockType.InterfaceType(ifce @ BlockTypeConstructor.Interface(name, Nil, List(op), decl), Nil)) =>
         (ifce, op, tpe)
-      case _ => Context.abort("Could not find Codepos interface with compatible type")
+      case _ => Context.abort("Could not find codepos interface with compatible type")
     }
     // now, synthesize an object that always returns the current position
-    val idIfce = IdRef(Nil, "Codepos", sp)
+    val idIfce = IdRef(Nil, "codepos", sp)
     Context.annotate(Annotations.Symbol, idIfce, ifce)
     val idOp = IdRef(Nil, op.name.name, sp)
     Context.annotate(Annotations.Symbol, idOp, op)
@@ -76,7 +76,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       // the remaining capabilities are provided as arguments
       val capabilityArgs = others.map{
-        case p if p.name.name == "Codepos" =>
+        case p if p.name.name == "codepos" =>
           codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
@@ -97,7 +97,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.name.name == "Codepos" =>
+        case p if p.name.name == "codepos" =>
           codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
@@ -116,7 +116,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.name.name == "Codepos" =>
+        case p if p.name.name == "codepos" =>
           codeposImplFor(span, p)
         case p =>
           referenceToCapability(p)
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
index 2ac07d9ad..0c4c50fd4 100644
--- a/examples/pos/codepos.effekt
+++ b/examples/pos/codepos.effekt
@@ -1,5 +1,5 @@
-def printCodepos(): Unit / Codepos = {
-  println(do Codepos())
+def printCodepos(): Unit / codepos = {
+  println(do codepos())
 }
 def main() = {
   printCodepos()
diff --git a/libraries/common/effekt.effekt b/libraries/common/effekt.effekt
index 5a62bcfa6..03d395a11 100644
--- a/libraries/common/effekt.effekt
+++ b/libraries/common/effekt.effekt
@@ -832,4 +832,8 @@ effect write(s: String): Unit
 
 effect splice[A](x: A): Unit
 
-effect Codepos(): String
\ No newline at end of file
+// Code positions
+// ==============
+// 
+/// Allows to get the code position of the callsite of the current function
+effect codepos(): String
\ No newline at end of file

From 05f35b281a9bbb8ecd1e873051fcc726ee91ab52 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 13:51:58 +0200
Subject: [PATCH 05/11] Fix generation of params

---
 .../src/main/scala/effekt/typer/CapabilityScope.scala | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
index 5aa207aec..a2fa31300 100644
--- a/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
+++ b/effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
@@ -19,8 +19,15 @@ case object GlobalCapabilityScope extends CapabilityScope {
   def parent: CapabilityScope = sys error "No parent"
   // If we try to find a capability for an effect that is known to be unhandled (that is no outer scope could
   // potentially handle it, then we raise an error.
-  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam =
-    C.abort(pretty"Effect ${tpe} is not allowed in this context.")
+  def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam = {
+    if (tpe.typeConstructor.name.name == "codepos") {
+      symbols.BlockParam(symbols.Name.local("codepos"), Some(tpe),
+        symbols.Resource(symbols.Name.local("codepos")), decl = source.NoSource)
+    } else {
+      C.abort(pretty"Effect ${tpe} is not allowed in this context.")
+    }
+  }
+
   def relevantInScopeFor(tpe: symbols.InterfaceType)(using C: Context): Set[symbols.InterfaceType] = Set.empty
 }
 

From 8d57b167e1a29439e934652e7eed5273a305e00e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 14:00:22 +0200
Subject: [PATCH 06/11] Forward codepos if the effect is explicit in the
 current context

---
 .../scala/effekt/source/ExplicitCapabilities.scala    | 11 +++++++----
 examples/pos/codepos.check                            |  4 +++-
 examples/pos/codepos.effekt                           |  6 ++++++
 3 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index 460b97ed6..5c50f6bc6 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -23,6 +23,7 @@ import effekt.source.SpannedOps._
 object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
   val phaseName = "explicit-capabilities"
+  val shouldForward = scala.util.DynamicVariable[Boolean](false)
 
   def run(input: Typechecked)(using C: Context) =
     val rewritten = C.timed(phaseName, input.source.name) { rewrite(input.tree) }
@@ -33,7 +34,9 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
     case f @ FunDef(id, tps, vps, bps, ret, cpt, body, doc, span) =>
       val capabilities = Context.annotation(Annotations.BoundCapabilities, f)
       val capParams = capabilities.map(definitionFor)
-      f.copy(bparams = (bps.unspan ++ capParams).spanned(bps.span), body = rewrite(body))
+      shouldForward.withValue(capParams.exists { p => p.id.name == "codepos" }) {
+        f.copy(bparams = (bps.unspan ++ capParams).spanned(bps.span), body = rewrite(body))
+      }
     case extDef @ ExternDef(capture, id, tparams, vparams, bparams, ret, bodies, doc, span) =>
       val rewrittenBodies = bodies.map { rewrite }
       extDef.copy(bodies = rewrittenBodies)
@@ -76,7 +79,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       // the remaining capabilities are provided as arguments
       val capabilityArgs = others.map{
-        case p if p.name.name == "codepos" =>
+        case p if p.name.name == "codepos" && !shouldForward.value =>
           codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
@@ -97,7 +100,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.name.name == "codepos" =>
+        case p if p.name.name == "codepos" && !shouldForward.value =>
           codeposImplFor(span, p)
         case p => referenceToCapability(p)
       }
@@ -116,7 +119,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
       val capabilityArgs = capabilities.map{
-        case p if p.name.name == "codepos" =>
+        case p if p.name.name == "codepos" && !shouldForward.value =>
           codeposImplFor(span, p)
         case p =>
           referenceToCapability(p)
diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
index 6160c070f..c517025b5 100644
--- a/examples/pos/codepos.check
+++ b/examples/pos/codepos.check
@@ -1,2 +1,4 @@
 examples/pos/codepos.effekt:82-96
-examples/pos/codepos.effekt:99-113
\ No newline at end of file
+examples/pos/codepos.effekt:99-113
+examples/pos/codepos.effekt:197-216
+examples/pos/codepos.effekt:197-216
\ No newline at end of file
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
index 0c4c50fd4..298a787b7 100644
--- a/examples/pos/codepos.effekt
+++ b/examples/pos/codepos.effekt
@@ -1,7 +1,13 @@
 def printCodepos(): Unit / codepos = {
   println(do codepos())
 }
+
+def printCodeposTwice(): Unit / codepos = {
+  printCodepos()
+  printCodepos()
+}
 def main() = {
   printCodepos()
   printCodepos()
+  printCodeposTwice()
 }
\ No newline at end of file

From 86e672da2cb62ae8835f9cd2e6edf3718d7284c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 14:04:45 +0200
Subject: [PATCH 07/11] Allow explicitly handling codepos at the callsite

---
 effekt/shared/src/main/scala/effekt/Typer.scala            | 2 +-
 .../main/scala/effekt/source/ExplicitCapabilities.scala    | 7 +++++--
 examples/pos/codepos.check                                 | 3 ++-
 examples/pos/codepos.effekt                                | 1 +
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Typer.scala b/effekt/shared/src/main/scala/effekt/Typer.scala
index f73407555..9d09da6e6 100644
--- a/effekt/shared/src/main/scala/effekt/Typer.scala
+++ b/effekt/shared/src/main/scala/effekt/Typer.scala
@@ -314,7 +314,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
             val allImplicit = capabilities.forall { c => !(explicitCapabilities contains c) }
             val used = effs.exists(e => e == effect)
 
-            if (allImplicit && !used)
+            if (allImplicit && !used && effect.name.name != "codepos")
               Context.warning(pp"Handling effect ${effect}, which seems not to be used by the program.")
         }
 
diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index 5c50f6bc6..f5d6a7db3 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -131,10 +131,13 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       Call(receiver, typeArgs, valueArgs, blockArgs ++ capabilityArgs, span)
 
     case h @ TryHandle(prog, handlers, span) =>
-      val body = rewrite(prog)
-
       val capabilities = Context.annotation(Annotations.BoundCapabilities, h)
 
+      val body = shouldForward.withValue(capabilities.exists { p => p.name.name == "codepos" }) {
+        rewrite(prog)
+      }
+
+
       assert(capabilities.size == handlers.size)
 
       // here we use the invariant that the order of capabilities is the same as the order of handlers
diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
index c517025b5..7b346ba15 100644
--- a/examples/pos/codepos.check
+++ b/examples/pos/codepos.check
@@ -1,4 +1,5 @@
 examples/pos/codepos.effekt:82-96
 examples/pos/codepos.effekt:99-113
 examples/pos/codepos.effekt:197-216
-examples/pos/codepos.effekt:197-216
\ No newline at end of file
+examples/pos/codepos.effekt:197-216
+END
\ No newline at end of file
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
index 298a787b7..aa41711f4 100644
--- a/examples/pos/codepos.effekt
+++ b/examples/pos/codepos.effekt
@@ -10,4 +10,5 @@ def main() = {
   printCodepos()
   printCodepos()
   printCodeposTwice()
+  try { printCodepos() } with codepos { () => resume("END") }
 }
\ No newline at end of file

From 80c55f5e2a08e7316a90e57a6d3802b7573a6e68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 14:08:51 +0200
Subject: [PATCH 08/11] Allow explicitly handling codepos at the callsite via a
 hof

---
 .../src/main/scala/effekt/source/ExplicitCapabilities.scala | 5 ++++-
 examples/pos/codepos.check                                  | 3 ++-
 examples/pos/codepos.effekt                                 | 6 +++++-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index f5d6a7db3..b1eeec497 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -168,7 +168,10 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
     case b @ source.BlockLiteral(tps, vps, bps, body, span) =>
       val capabilities = Context.annotation(Annotations.BoundCapabilities, b)
       val capParams = capabilities.map(definitionFor)
-      source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body), span)
+
+      shouldForward.withValue(capabilities.exists { p => p.name.name == "codepos" }) {
+        source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body), span)
+      }
   }
 
   override def rewrite(body: ExternBody)(using context.Context): ExternBody =
diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
index 7b346ba15..dc0a94178 100644
--- a/examples/pos/codepos.check
+++ b/examples/pos/codepos.check
@@ -2,4 +2,5 @@ examples/pos/codepos.effekt:82-96
 examples/pos/codepos.effekt:99-113
 examples/pos/codepos.effekt:197-216
 examples/pos/codepos.effekt:197-216
-END
\ No newline at end of file
+X
+examples/pos/codepos.effekt:196-202
\ No newline at end of file
diff --git a/examples/pos/codepos.effekt b/examples/pos/codepos.effekt
index aa41711f4..ca54ed108 100644
--- a/examples/pos/codepos.effekt
+++ b/examples/pos/codepos.effekt
@@ -6,9 +6,13 @@ def printCodeposTwice(): Unit / codepos = {
   printCodepos()
   printCodepos()
 }
+def atHere{ body: => Unit / codepos }: Unit = {
+  body()
+}
 def main() = {
   printCodepos()
   printCodepos()
   printCodeposTwice()
-  try { printCodepos() } with codepos { () => resume("END") }
+  try { printCodepos() } with codepos { () => resume("X") }
+  atHere{ printCodepos() }
 }
\ No newline at end of file

From 64cebd568e5bc6f8198e9f0c3419fa70292213d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 14:11:39 +0200
Subject: [PATCH 09/11] Update test

---
 examples/pos/codepos.check | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
index dc0a94178..cd16b7b38 100644
--- a/examples/pos/codepos.check
+++ b/examples/pos/codepos.check
@@ -1,6 +1,6 @@
-examples/pos/codepos.effekt:82-96
-examples/pos/codepos.effekt:99-113
-examples/pos/codepos.effekt:197-216
-examples/pos/codepos.effekt:197-216
+examples/pos/codepos.effekt:222-236
+examples/pos/codepos.effekt:239-253
+examples/pos/codepos.effekt:256-275
+examples/pos/codepos.effekt:256-275
 X
 examples/pos/codepos.effekt:196-202
\ No newline at end of file

From 9a254b560bfac37207cc0c2f9122a2b4654f0f6a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 14:14:35 +0200
Subject: [PATCH 10/11] Forward over multiple levels

---
 .../src/main/scala/effekt/source/ExplicitCapabilities.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index b1eeec497..7beb96583 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -34,7 +34,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
     case f @ FunDef(id, tps, vps, bps, ret, cpt, body, doc, span) =>
       val capabilities = Context.annotation(Annotations.BoundCapabilities, f)
       val capParams = capabilities.map(definitionFor)
-      shouldForward.withValue(capParams.exists { p => p.id.name == "codepos" }) {
+      shouldForward.withValue(shouldForward.value || capParams.exists { p => p.id.name == "codepos" }) {
         f.copy(bparams = (bps.unspan ++ capParams).spanned(bps.span), body = rewrite(body))
       }
     case extDef @ ExternDef(capture, id, tparams, vparams, bparams, ret, bodies, doc, span) =>
@@ -133,7 +133,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
     case h @ TryHandle(prog, handlers, span) =>
       val capabilities = Context.annotation(Annotations.BoundCapabilities, h)
 
-      val body = shouldForward.withValue(capabilities.exists { p => p.name.name == "codepos" }) {
+      val body = shouldForward.withValue(shouldForward.value || capabilities.exists { p => p.name.name == "codepos" }) {
         rewrite(prog)
       }
 
@@ -169,7 +169,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       val capabilities = Context.annotation(Annotations.BoundCapabilities, b)
       val capParams = capabilities.map(definitionFor)
 
-      shouldForward.withValue(capabilities.exists { p => p.name.name == "codepos" }) {
+      shouldForward.withValue(shouldForward.value || capabilities.exists { p => p.name.name == "codepos" }) {
         source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body), span)
       }
   }

From b0e9a89f312612f4717f07c9d645fc5a0753b1a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcial=20Gai=C3=9Fert?= <uni@gaisseml.de>
Date: Wed, 8 Apr 2026 15:13:18 +0200
Subject: [PATCH 11/11] Use line+column for more readable codepos strings

---
 .../scala/effekt/source/ExplicitCapabilities.scala     |  4 +++-
 examples/pos/codepos.check                             | 10 +++++-----
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index 7beb96583..b5be06fbb 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -43,7 +43,9 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
   }
 
   def codeposImplFor(span: Span, p: TrackedParam.BlockParam)(using Context): Term = {
-    val pos = s"${span.source.name}:${span.from}-${span.to}"
+    val from = span.source.offsetToPosition(span.from)
+    val to = span.source.offsetToPosition(span.to)
+    val pos = s"${span.source.name}:${from.line}:${from.column}-${to.line}:${to.column}"
     val sp = span.synthesized
     val (ifce, op, tpe) = p.tpe match {
       case Some(tpe @ BlockType.InterfaceType(ifce @ BlockTypeConstructor.Interface(name, Nil, List(op), decl), Nil)) =>
diff --git a/examples/pos/codepos.check b/examples/pos/codepos.check
index cd16b7b38..d1dbc3447 100644
--- a/examples/pos/codepos.check
+++ b/examples/pos/codepos.check
@@ -1,6 +1,6 @@
-examples/pos/codepos.effekt:222-236
-examples/pos/codepos.effekt:239-253
-examples/pos/codepos.effekt:256-275
-examples/pos/codepos.effekt:256-275
+examples/pos/codepos.effekt:13:3-13:17
+examples/pos/codepos.effekt:14:3-14:17
+examples/pos/codepos.effekt:15:3-15:22
+examples/pos/codepos.effekt:15:3-15:22
 X
-examples/pos/codepos.effekt:196-202
\ No newline at end of file
+examples/pos/codepos.effekt:10:3-10:9
\ No newline at end of file