diff --git a/community-build/community-projects/stdLib213 b/community-build/community-projects/stdLib213
index 21cb41941e39..2361c1f0373f 160000
--- a/community-build/community-projects/stdLib213
+++ b/community-build/community-projects/stdLib213
@@ -1 +1 @@
-Subproject commit 21cb41941e399b0b06c4ea80abbc6e2084f2e415
+Subproject commit 2361c1f0373f8af5418abe393bb85663f8f95259
diff --git a/compiler/src/dotty/tools/dotc/config/Feature.scala b/compiler/src/dotty/tools/dotc/config/Feature.scala
index 4b9ade558b5d..42fc2d0e9375 100644
--- a/compiler/src/dotty/tools/dotc/config/Feature.scala
+++ b/compiler/src/dotty/tools/dotc/config/Feature.scala
@@ -19,11 +19,13 @@ object Feature:
   private def deprecated(str: String): TermName =
     QualifiedName(nme.deprecated, str.toTermName)
 
-  private val Xdependent = experimental("dependent")
-  private val XnamedTypeArguments = experimental("namedTypeArguments")
-  private val XgenericNumberLiterals = experimental("genericNumberLiterals")
-  private val Xmacros = experimental("macros")
-  private val symbolLiterals: TermName = deprecated("symbolLiterals")
+  private val namedTypeArguments = experimental("namedTypeArguments")
+  private val genericNumberLiterals = experimental("genericNumberLiterals")
+  private val scala2macros = experimental("macros")
+
+  val dependent = experimental("dependent")
+  val erasedDefinitions = experimental("erasedDefinitions")
+  val symbolLiterals: TermName = deprecated("symbolLiterals")
 
 /** Is `feature` enabled by by a command-line setting? The enabling setting is
    *
@@ -62,15 +64,13 @@ object Feature:
 
   def dynamicsEnabled(using Context): Boolean = enabled(nme.dynamics)
 
-  def dependentEnabled(using Context) = enabled(Xdependent)
-
-  def namedTypeArgsEnabled(using Context) = enabled(XnamedTypeArguments)
+  def dependentEnabled(using Context) = enabled(dependent)
 
-  def genericNumberLiteralsEnabled(using Context) = enabled(XgenericNumberLiterals)
+  def namedTypeArgsEnabled(using Context) = enabled(namedTypeArguments)
 
-  def symbolLiteralsEnabled(using Context) = enabled(symbolLiterals)
+  def genericNumberLiteralsEnabled(using Context) = enabled(genericNumberLiterals)
 
-  def scala2ExperimentalMacroEnabled(using Context) = enabled(Xmacros)
+  def scala2ExperimentalMacroEnabled(using Context) = enabled(scala2macros)
 
   def sourceVersionSetting(using Context): SourceVersion =
     SourceVersion.valueOf(ctx.settings.source.value)
diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index 81411374f060..01e7d87117d2 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -227,9 +227,9 @@ class ScalaSettings extends Settings.SettingGroup with CommonScalaSettings {
   // Extremely experimental language features
   val YnoKindPolymorphism: Setting[Boolean] = BooleanSetting("-Yno-kind-polymorphism", "Disable kind polymorphism.")
   val YexplicitNulls: Setting[Boolean] = BooleanSetting("-Yexplicit-nulls", "Make reference types non-nullable. Nullable types can be expressed with unions: e.g. String|Null.")
-  val YerasedTerms: Setting[Boolean] = BooleanSetting("-Yerased-terms", "Allows the use of erased terms.")
   val YcheckInit: Setting[Boolean] = BooleanSetting("-Ysafe-init", "Ensure safe initialization of objects")
   val YrequireTargetName: Setting[Boolean] = BooleanSetting("-Yrequire-targetName", "Warn if an operator is defined without a @targetName annotation")
+  val YerasedTerms: Setting[Boolean] = BooleanSetting("-Yerased-terms", "(disabled, use -language:experimental.erasedDefinitions instead)")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")
diff --git a/compiler/src/dotty/tools/dotc/core/Flags.scala b/compiler/src/dotty/tools/dotc/core/Flags.scala
index 5bcc32de158f..d077524342ac 100644
--- a/compiler/src/dotty/tools/dotc/core/Flags.scala
+++ b/compiler/src/dotty/tools/dotc/core/Flags.scala
@@ -360,8 +360,8 @@ object Flags {
   /** An export forwarder */
   val (Exported @ _, _, _) = newFlags(41, "exported")
 
-  /** Labeled with `erased` modifier (erased value)  */
-  val (_, Erased @ _, _) = newFlags(42, "erased")
+  /** Labeled with `erased` modifier (erased value or class)  */
+  val (Erased @ _, _, _) = newFlags(42, "erased")
 
   /** An opaque type alias or a class containing one */
   val (Opaque @ _, _, _) = newFlags(43, "opaque")
@@ -439,13 +439,13 @@ object Flags {
 
   /** Flags representing source modifiers */
   private val CommonSourceModifierFlags: FlagSet =
-    commonFlags(Private, Protected, Final, Case, Implicit, Given, Override, JavaStatic, Transparent)
+    commonFlags(Private, Protected, Final, Case, Implicit, Given, Override, JavaStatic, Transparent, Erased)
 
   val TypeSourceModifierFlags: FlagSet =
     CommonSourceModifierFlags.toTypeFlags | Abstract | Sealed | Opaque | Open
 
   val TermSourceModifierFlags: FlagSet =
-    CommonSourceModifierFlags.toTermFlags | Inline | AbsOverride | Lazy | Erased
+    CommonSourceModifierFlags.toTermFlags | Inline | AbsOverride | Lazy
 
   /** Flags representing modifiers that can appear in trees */
   val ModifierFlags: FlagSet =
@@ -515,12 +515,12 @@ object Flags {
   val RetainedModuleValAndClassFlags: FlagSet =
     AccessFlags | Package | Case |
     Synthetic | JavaDefined | JavaStatic | Artifact |
-    Lifted | MixedIn | Specialized | ConstructorProxy | Invisible
+    Lifted | MixedIn | Specialized | ConstructorProxy | Invisible | Erased
 
   /** Flags that can apply to a module val */
   val RetainedModuleValFlags: FlagSet = RetainedModuleValAndClassFlags |
     Override | Final | Method | Implicit | Given | Lazy |
-    Accessor | AbsOverride | StableRealizable | Captured | Synchronized | Erased | Transparent
+    Accessor | AbsOverride | StableRealizable | Captured | Synchronized | Transparent
 
   /** Flags that can apply to a module class */
   val RetainedModuleClassFlags: FlagSet = RetainedModuleValAndClassFlags | Enum
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index ff8a1ef035ce..076010399651 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -466,6 +466,7 @@ object StdNames {
     val equalsNumNum : N        = "equalsNumNum"
     val equalsNumObject : N     = "equalsNumObject"
     val equals_ : N             = "equals"
+    val erased: N               = "erased"
     val error: N                = "error"
     val eval: N                 = "eval"
     val eqlAny: N               = "eqlAny"
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index ccbbacf2cb63..0ee7fe15f32d 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -729,10 +729,10 @@ class TreePickler(pickler: TastyPickler) {
     if flags.is(Transparent) then writeModTag(TRANSPARENT)
     if flags.is(Infix) then writeModTag(INFIX)
     if flags.is(Invisible) then writeModTag(INVISIBLE)
+    if (flags.is(Erased)) writeModTag(ERASED)
     if (isTerm) {
       if (flags.is(Implicit)) writeModTag(IMPLICIT)
       if (flags.is(Given)) writeModTag(GIVEN)
-      if (flags.is(Erased)) writeModTag(ERASED)
       if (flags.is(Lazy, butNot = Module)) writeModTag(LAZY)
       if (flags.is(AbsOverride)) { writeModTag(ABSTRACT); writeModTag(OVERRIDE) }
       if (flags.is(Mutable)) writeModTag(MUTABLE)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index e52368d6b117..16a044a759eb 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -28,7 +28,8 @@ import util.Chars
 import scala.annotation.{tailrec, switch}
 import rewrites.Rewrites.{patch, overlapsPatch}
 import reporting._
-import config.Feature.{sourceVersion, migrateTo3, dependentEnabled, symbolLiteralsEnabled}
+import config.Feature
+import config.Feature.{sourceVersion, migrateTo3}
 import config.SourceVersion._
 import config.SourceVersion
 
@@ -179,6 +180,7 @@ object Parsers {
 
     def isIdent = in.isIdent
     def isIdent(name: Name) = in.isIdent(name)
+    def isErased = isIdent(nme.erased) && in.erasedEnabled
     def isSimpleLiteral =
       simpleLiteralTokens.contains(in.token)
       || isIdent(nme.raw.MINUS) && numericLitTokens.contains(in.lookahead.token)
@@ -446,11 +448,10 @@ object Parsers {
      *  Parameters appear in reverse order.
      */
     var placeholderParams: List[ValDef] = Nil
-    var languageImportContext: Context = ctx
 
     def checkNoEscapingPlaceholders[T](op: => T): T =
       val savedPlaceholderParams = placeholderParams
-      val savedLanguageImportContext = languageImportContext
+      val savedLanguageImportContext = in.languageImportContext
       placeholderParams = Nil
       try op
       finally
@@ -458,7 +459,7 @@ object Parsers {
           case vd :: _ => syntaxError(UnboundPlaceholderParameter(), vd.span)
           case _ =>
         placeholderParams = savedPlaceholderParams
-        languageImportContext = savedLanguageImportContext
+        in.languageImportContext = savedLanguageImportContext
 
     def isWildcard(t: Tree): Boolean = t match {
       case Ident(name1) => placeholderParams.nonEmpty && name1 == placeholderParams.head.name
@@ -1141,7 +1142,7 @@ object Parsers {
             Quote(t)
           }
           else
-            if !symbolLiteralsEnabled(using languageImportContext) then
+            if !in.featureEnabled(Feature.symbolLiterals) then
               report.errorOrMigrationWarning(
                 em"""symbol literal '${in.name} is no longer supported,
                     |use a string literal "${in.name}" or an application Symbol("${in.name}") instead,
@@ -1374,7 +1375,7 @@ object Parsers {
             functionRest(Nil)
           }
           else {
-            imods = modifiers(funTypeArgMods)
+            if isErased then imods = addModifier(imods)
             val paramStart = in.offset
             val ts = funArgType() match {
               case Ident(name) if name != tpnme.WILDCARD && in.token == COLON =>
@@ -1572,7 +1573,7 @@ object Parsers {
         typeIdent()
       else
         def singletonArgs(t: Tree): Tree =
-          if in.token == LPAREN && dependentEnabled(using languageImportContext)
+          if in.token == LPAREN && in.featureEnabled(Feature.dependent)
           then singletonArgs(AppliedTypeTree(t, inParens(commaSeparated(singleton))))
           else t
         singletonArgs(simpleType1())
@@ -1861,7 +1862,7 @@ object Parsers {
 
     def expr(location: Location): Tree = {
       val start = in.offset
-      def isSpecialClosureStart = in.lookahead.token == ERASED
+      def isSpecialClosureStart = in.lookahead.isIdent(nme.erased) && in.erasedEnabled
       if in.token == IMPLICIT then
         closure(start, location, modifiers(BitSet(IMPLICIT)))
       else if in.token == LPAREN && isSpecialClosureStart then
@@ -2093,7 +2094,7 @@ object Parsers {
           Nil
         else
           var mods1 = mods
-          if in.token == ERASED then mods1 = addModifier(mods1)
+          if isErased then mods1 = addModifier(mods1)
           try
             commaSeparated(() => binding(mods1))
           finally
@@ -2684,7 +2685,6 @@ object Parsers {
       case FINAL       => Mod.Final()
       case IMPLICIT    => Mod.Implicit()
       case GIVEN       => Mod.Given()
-      case ERASED      => Mod.Erased()
       case LAZY        => Mod.Lazy()
       case OVERRIDE    => Mod.Override()
       case PRIVATE     => Mod.Private()
@@ -2692,6 +2692,7 @@ object Parsers {
       case SEALED      => Mod.Sealed()
       case IDENTIFIER =>
         name match {
+          case nme.erased if in.erasedEnabled => Mod.Erased()
           case nme.inline => Mod.Inline()
           case nme.opaque => Mod.Opaque()
           case nme.open => Mod.Open()
@@ -2775,8 +2776,6 @@ object Parsers {
       normalize(loop(start))
     }
 
-    val funTypeArgMods: BitSet = BitSet(ERASED)
-
     /** Wrap annotation or constructor in New(...).<init> */
     def wrapNew(tpt: Tree): Select = Select(New(tpt), nme.CONSTRUCTOR)
 
@@ -2899,10 +2898,13 @@ object Parsers {
       def addParamMod(mod: () => Mod) = impliedMods = addMod(impliedMods, atSpan(in.skipToken()) { mod() })
 
       def paramMods() =
-        if in.token == IMPLICIT then addParamMod(() => Mod.Implicit())
+        if in.token == IMPLICIT then
+          addParamMod(() => Mod.Implicit())
         else
-          if isIdent(nme.using) then addParamMod(() => Mod.Given())
-          if in.token == ERASED then addParamMod(() => Mod.Erased())
+          if isIdent(nme.using) then
+            addParamMod(() => Mod.Given())
+          if isErased then
+            addParamMod(() => Mod.Erased())
 
       def param(): ValDef = {
         val start = in.offset
@@ -2959,7 +2961,7 @@ object Parsers {
         if in.token == RPAREN && !prefix && !impliedMods.is(Given) then Nil
         else
           val clause =
-            if prefix && !isIdent(nme.using) then param() :: Nil
+            if prefix && !isIdent(nme.using) && !isIdent(nme.erased) then param() :: Nil
             else
               paramMods()
               if givenOnly && !impliedMods.is(Given) then
@@ -3032,7 +3034,7 @@ object Parsers {
     def mkImport(outermost: Boolean = false): ImportConstr = (tree, selectors) =>
       val imp = Import(tree, selectors)
       if isLanguageImport(tree) then
-        languageImportContext = languageImportContext.importContext(imp, NoSymbol)
+        in.languageImportContext = in.languageImportContext.importContext(imp, NoSymbol)
         for
           case ImportSelector(id @ Ident(imported), EmptyTree, _) <- selectors
           if allSourceVersionNames.contains(imported)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
index 7e5eb3993f9e..789a76e88190 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
@@ -17,6 +17,7 @@ import scala.annotation.{switch, tailrec}
 import scala.collection.mutable
 import scala.collection.immutable.{SortedMap, BitSet}
 import rewrites.Rewrites.patch
+import config.Feature
 import config.Feature.migrateTo3
 import config.SourceVersion._
 import reporting.Message
@@ -185,6 +186,13 @@ object Scanners {
         error(s"illegal combination of -rewrite targets: ${enabled(0).name} and ${enabled(1).name}")
     }
 
+    private var myLanguageImportContext: Context = ctx
+    def languageImportContext = myLanguageImportContext
+    final def languageImportContext_=(c: Context) = myLanguageImportContext = c
+
+    def featureEnabled(name: TermName) = Feature.enabled(name)(using languageImportContext)
+    def erasedEnabled = featureEnabled(Feature.erasedDefinitions) || ctx.settings.YerasedTerms.value
+
     /** All doc comments kept by their end position in a `Map`.
       *
       * Note: the map is necessary since the comments are looked up after an
@@ -215,8 +223,7 @@ object Scanners {
     private val commentBuf = CharBuffer()
 
     private def handleMigration(keyword: Token): Token =
-      if keyword == ERASED && !ctx.settings.YerasedTerms.value then IDENTIFIER
-      else if scala3keywords.contains(keyword) && migrateTo3 then treatAsIdent()
+      if scala3keywords.contains(keyword) && migrateTo3 then treatAsIdent()
       else keyword
 
     private def treatAsIdent(): Token =
@@ -907,7 +914,9 @@ object Scanners {
         reset()
       next
 
-    class LookaheadScanner() extends Scanner(source, offset)
+    class LookaheadScanner() extends Scanner(source, offset) {
+      override def languageImportContext = Scanner.this.languageImportContext
+    }
 
     /** Skip matching pairs of `(...)` or `[...]` parentheses.
      *  @pre  The current token is `(` or `[`
@@ -1009,7 +1018,8 @@ object Scanners {
       }
 
     def isSoftModifier: Boolean =
-      token == IDENTIFIER && softModifierNames.contains(name)
+      token == IDENTIFIER
+      && (softModifierNames.contains(name) || name == nme.erased && erasedEnabled)
 
     def isSoftModifierInModifierPosition: Boolean =
       isSoftModifier && inModifierPosition()
@@ -1017,6 +1027,8 @@ object Scanners {
     def isSoftModifierInParamModifierPosition: Boolean =
       isSoftModifier && lookahead.token != COLON
 
+    def isErased: Boolean = isIdent(nme.erased) && erasedEnabled
+
     def canStartStatTokens =
       if migrateTo3 then canStartStatTokens2 else canStartStatTokens3
 
diff --git a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
index 4bbd0cbd8184..24a38f9d5e0a 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
@@ -95,7 +95,6 @@ abstract class TokensCommon {
   //final val THEN = 60;             enter(THEN, "then")
   //final val FORSOME = 61;          enter(FORSOME, "forSome") // TODO: deprecate
   //final val ENUM = 62;             enter(ENUM, "enum")
-  //final val ERASED = 63;           enter(ERASED, "erased")
 
   /** special symbols */
   final val COMMA = 70;            enter(COMMA, "','")
@@ -181,10 +180,9 @@ object Tokens extends TokensCommon {
   final val THEN = 60;             enter(THEN, "then")
   final val FORSOME = 61;          enter(FORSOME, "forSome") // TODO: deprecate
   final val ENUM = 62;             enter(ENUM, "enum")
-  final val ERASED = 63;           enter(ERASED, "erased")
-  final val GIVEN = 64;            enter(GIVEN, "given")
-  final val EXPORT = 65;           enter(EXPORT, "export")
-  final val MACRO = 67;            enter(MACRO, "macro") // TODO: remove
+  final val GIVEN = 63;            enter(GIVEN, "given")
+  final val EXPORT = 64;           enter(EXPORT, "export")
+  final val MACRO = 65;            enter(MACRO, "macro") // TODO: remove
 
   /** special symbols */
   final val NEWLINE = 78;          enter(NEWLINE, "end of statement", "new line")
@@ -240,8 +238,7 @@ object Tokens extends TokensCommon {
 
   final val defIntroTokens: TokenSet = templateIntroTokens | dclIntroTokens
 
-  final val localModifierTokens: TokenSet = BitSet(
-    ABSTRACT, FINAL, SEALED, IMPLICIT, LAZY, ERASED)
+  final val localModifierTokens: TokenSet = BitSet(ABSTRACT, FINAL, SEALED, IMPLICIT, LAZY)
 
   final val accessModifierTokens: TokenSet = BitSet(
     PRIVATE, PROTECTED)
@@ -251,7 +248,7 @@ object Tokens extends TokensCommon {
 
   final val modifierTokensOrCase: TokenSet = modifierTokens | BitSet(CASE)
 
-  final val modifierFollowers = modifierTokens | defIntroTokens
+  final val modifierFollowers = modifierTokensOrCase | defIntroTokens
 
   /** Is token only legal as start of statement (eof also included)? */
   final val mustStartStatTokens: TokenSet = defIntroTokens | modifierTokens | BitSet(IMPORT, EXPORT, PACKAGE)
@@ -283,7 +280,7 @@ object Tokens extends TokensCommon {
    */
   final val startParamTokens: BitSet = modifierTokens | BitSet(VAL, VAR, AT)
 
-  final val scala3keywords = BitSet(ENUM, ERASED, GIVEN)
+  final val scala3keywords = BitSet(ENUM, GIVEN)
 
   final val endMarkerTokens = identifierTokens | BitSet(IF, WHILE, FOR, MATCH, TRY, NEW, THROW, GIVEN, VAL, THIS)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 8d1f5e4a8051..1ae489094355 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -925,7 +925,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       else PrintableFlags(isType)
     if (homogenizedView && mods.flags.isTypeFlags) flagMask &~= GivenOrImplicit // drop implicit/given from classes
     val rawFlags = if (sym.exists) sym.flags else mods.flags
-    if (rawFlags.is(Param)) flagMask = flagMask &~ Given
+    if (rawFlags.is(Param)) flagMask = flagMask &~ Given &~ Erased
     val flags = rawFlags & flagMask
     var flagsText = toTextFlags(sym, flags)
     val annotations =
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 583613169e48..3231a36702b8 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -13,6 +13,7 @@ import core.Names._
 import core.StdNames._
 import core.NameOps._
 import core.NameKinds.{AdaptedClosureName, BodyRetainerName}
+import core.Scopes.newScopeWith
 import core.Decorators._
 import core.Constants._
 import core.Definitions._
@@ -81,16 +82,22 @@ class Erasure extends Phase with DenotTransformer {
         val oldName = ref.name
         val newName = ref.targetName
         val oldInfo = ref.info
-        val newInfo = transformInfo(oldSymbol, oldInfo)
+        var newInfo = transformInfo(oldSymbol, oldInfo)
         val oldFlags = ref.flags
         var newFlags =
-          if (oldSymbol.is(Flags.TermParam) && isCompacted(oldSymbol.owner.denot)) oldFlags &~ Flags.Param
+          if oldSymbol.is(Flags.TermParam) && isCompacted(oldSymbol.owner.denot) then oldFlags &~ Flags.Param
           else oldFlags
         val oldAnnotations = ref.annotations
         var newAnnotations = oldAnnotations
         if oldSymbol.isRetainedInlineMethod then
           newFlags = newFlags &~ Flags.Inline
           newAnnotations = newAnnotations.filterConserve(!_.isInstanceOf[BodyAnnotation])
+        oldSymbol match
+          case cls: ClassSymbol if cls.is(Flags.Erased) =>
+            newFlags = newFlags | Flags.Trait | Flags.JavaInterface
+            newAnnotations = Nil
+            newInfo = erasedClassInfo(cls)
+          case _ =>
         // TODO: define derivedSymDenotation?
         if ref.is(Flags.PackageClass)
            || !ref.isClass  // non-package classes are always copied since their base types change
@@ -125,6 +132,12 @@ class Erasure extends Phase with DenotTransformer {
     unit.tpdTree = eraser.typedExpr(unit.tpdTree)(using ctx.fresh.setTyper(eraser).setPhase(this.next))
   }
 
+  /** erased classes get erased to empty traits with Object as parent and an empty constructor */
+  private def erasedClassInfo(cls: ClassSymbol)(using Context) =
+    cls.classInfo.derivedClassInfo(
+      declaredParents = defn.ObjectClass.typeRef :: Nil,
+      decls = newScopeWith(newConstructor(cls, Flags.EmptyFlags, Nil, Nil)))
+
   override def checkPostCondition(tree: tpd.Tree)(using Context): Unit = {
     assertErased(tree)
     tree match {
@@ -584,13 +597,33 @@ object Erasure {
           case _ => // OK
         }
       }
-      tree
+      checkNotErasedClass(tree)
     }
 
-    def erasedDef(sym: Symbol)(using Context): Thicket = {
-      if (sym.owner.isClass) sym.dropAfter(erasurePhase)
-      tpd.EmptyTree
-    }
+    private def checkNotErasedClass(tp: Type, tree: untpd.Tree)(using Context): Unit = tp match
+      case JavaArrayType(et) =>
+        checkNotErasedClass(et, tree)
+      case _ =>
+        if tp.isErasedClass then
+          val (kind, tree1) = tree match
+            case tree: untpd.ValOrDefDef => ("definition", tree.tpt)
+            case tree: untpd.DefTree => ("definition", tree)
+            case _ => ("expression", tree)
+          report.error(em"illegal reference to erased ${tp.typeSymbol} in $kind that is not itself erased", tree1.srcPos)
+
+    private def checkNotErasedClass(tree: Tree)(using Context): tree.type =
+      checkNotErasedClass(tree.tpe.widen.finalResultType, tree)
+      tree
+
+    def erasedDef(sym: Symbol)(using Context): Tree =
+      if sym.isClass then
+      	// We cannot simply drop erased classes, since then they would not generate classfiles
+      	// and would not be visible under separate compilation. So we transform them to
+      	// empty interfaces instead.
+        tpd.ClassDef(sym.asClass, DefDef(sym.primaryConstructor.asTerm), Nil)
+      else
+        if sym.owner.isClass then sym.dropAfter(erasurePhase)
+        tpd.EmptyTree
 
     def erasedType(tree: untpd.Tree)(using Context): Type = {
       val tp = tree.typeOpt
@@ -609,7 +642,7 @@ object Erasure {
      *  are handled separately by [[typedDefDef]], [[typedValDef]] and [[typedTyped]].
      */
     override def typedTypeTree(tree: untpd.TypeTree, pt: Type)(using Context): TypeTree =
-      tree.withType(erasure(tree.tpe))
+      checkNotErasedClass(tree.withType(erasure(tree.tpe)))
 
     /** This override is only needed to semi-erase type ascriptions */
     override def typedTyped(tree: untpd.Typed, pt: Type)(using Context): Tree =
@@ -628,7 +661,7 @@ object Erasure {
       if (tree.typeOpt.isRef(defn.UnitClass))
         tree.withType(tree.typeOpt)
       else if (tree.const.tag == Constants.ClazzTag)
-        clsOf(tree.const.typeValue)
+        checkNotErasedClass(clsOf(tree.const.typeValue))
       else
         super.typedLiteral(tree)
 
@@ -869,6 +902,7 @@ object Erasure {
     override def typedValDef(vdef: untpd.ValDef, sym: Symbol)(using Context): Tree =
       if (sym.isEffectivelyErased) erasedDef(sym)
       else
+        checkNotErasedClass(sym.info, vdef)
         super.typedValDef(untpd.cpy.ValDef(vdef)(
           tpt = untpd.TypedSplice(TypeTree(sym.info).withSpan(vdef.tpt.span))), sym)
 
@@ -880,6 +914,7 @@ object Erasure {
       if sym.isEffectivelyErased || sym.name.is(BodyRetainerName) then
         erasedDef(sym)
       else
+        checkNotErasedClass(sym.info.finalResultType, ddef)
         val restpe = if sym.isConstructor then defn.UnitType else sym.info.resultType
         var vparams = outerParamDefs(sym)
             ::: ddef.paramss.collect {
@@ -892,8 +927,9 @@ object Erasure {
             case closureDef(meth) =>
               val contextParams = meth.termParamss.head
               for param <- contextParams do
-                param.symbol.copySymDenotation(owner = sym).installAfter(erasurePhase)
-              vparams ++= contextParams
+                if !param.symbol.is(Flags.Erased) then
+                  param.symbol.copySymDenotation(owner = sym).installAfter(erasurePhase)
+                  vparams = vparams :+ param
               if crCount == 1 then meth.rhs.changeOwnerAfter(meth.symbol, sym, erasurePhase)
               else skipContextClosures(meth.rhs, crCount - 1)
 
@@ -995,6 +1031,9 @@ object Erasure {
       adaptClosure(implClosure)
     }
 
+    override def typedNew(tree: untpd.New, pt: Type)(using Context): Tree =
+      checkNotErasedClass(super.typedNew(tree, pt))
+
     override def typedTypeDef(tdef: untpd.TypeDef, sym: Symbol)(using Context): Tree =
       EmptyTree
 
@@ -1012,8 +1051,10 @@ object Erasure {
         if mbr.is(ConstructorProxy) then mbr.dropAfter(erasurePhase)
 
     override def typedClassDef(cdef: untpd.TypeDef, cls: ClassSymbol)(using Context): Tree =
-      try super.typedClassDef(cdef, cls)
-      finally dropConstructorProxies(cls)
+      if cls.is(Flags.Erased) then erasedDef(cls)
+      else
+        try super.typedClassDef(cdef, cls)
+        finally dropConstructorProxies(cls)
 
     override def typedAnnotated(tree: untpd.Annotated, pt: Type)(using Context): Tree =
       typed(tree.arg, pt)
diff --git a/compiler/src/dotty/tools/dotc/transform/PruneErasedDefs.scala b/compiler/src/dotty/tools/dotc/transform/PruneErasedDefs.scala
index 121b2f664c6e..e18de6e60876 100644
--- a/compiler/src/dotty/tools/dotc/transform/PruneErasedDefs.scala
+++ b/compiler/src/dotty/tools/dotc/transform/PruneErasedDefs.scala
@@ -34,7 +34,7 @@ class PruneErasedDefs extends MiniPhase with SymTransformer { thisTransform =>
   override def runsAfterGroupsOf: Set[String] = Set(RefChecks.name, ExplicitOuter.name)
 
   override def transformSym(sym: SymDenotation)(using Context): SymDenotation =
-    if (sym.isEffectivelyErased && !sym.is(Private) && sym.owner.isClass)
+    if (sym.isEffectivelyErased && sym.isTerm && !sym.is(Private) && sym.owner.isClass)
       sym.copySymDenotation(initFlags = sym.flags | Private)
     else sym
 
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
index d92812409ffe..813f8ddf8780 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeUtils.scala
@@ -21,6 +21,9 @@ object TypeUtils {
     def isPrimitiveValueType(using Context): Boolean =
       self.classSymbol.isPrimitiveValueClass
 
+    def isErasedClass(using Context): Boolean =
+      self.underlyingClassRef(refinementOK = true).typeSymbol.is(Flags.Erased)
+
     def isByName: Boolean =
       self.isInstanceOf[ExprType]
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index e00253515aa8..7b799a25c996 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -501,7 +501,8 @@ object Checking {
         sym.setFlag(Private) // break the overriding relationship by making sym Private
       }
     if (sym.is(Erased))
-      checkApplicable(Erased, !sym.isOneOf(MutableOrLazy, butNot = Given))
+      checkApplicable(Erased,
+        !sym.isOneOf(MutableOrLazy, butNot = Given) && !sym.isType || sym.isClass)
   }
 
   /** Check the type signature of the symbol `M` defined by `tree` does not refer
@@ -997,11 +998,6 @@ trait Checking {
       errorTree(tpt, MissingTypeParameterFor(tpt.tpe))
     else tpt
 
-  /** Check that the signature of the class mamber does not return a repeated parameter type */
-  def checkSignatureRepeatedParam(sym: Symbol)(using Context): Unit =
-    if (!sym.isOneOf(Synthetic | InlineProxy | Param) && sym.info.finalResultType.isRepeatedParam)
-      report.error(em"Cannot return repeated parameter type ${sym.info.finalResultType}", sym.srcPos)
-
   /** Verify classes extending AnyVal meet the requirements */
   def checkDerivedValueClass(clazz: Symbol, stats: List[Tree])(using Context): Unit =
     Checking.checkDerivedValueClass(clazz, stats)
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index ffb1d403230a..2b01a7245969 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -898,7 +898,7 @@ trait Implicits:
       case Select(qual, nme.apply) if defn.isFunctionType(qual.tpe.widen) =>
         val qt = qual.tpe.widen
         val qt1 = qt.dealiasKeepAnnots
-        def addendum = if (qt1 eq qt) "" else (i"\nwhich is an alias of: $qt1")
+        def addendum = if (qt1 eq qt) "" else (i"\nThe required type is an alias of: $qt1")
         em"parameter of ${qual.tpe.widen}$addendum"
       case _ =>
         em"${ if paramName.is(EvidenceParamName) then "an implicit parameter"
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 0a7fc772bbfa..9b94f897ddf5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1147,8 +1147,24 @@ class Typer extends Namer
 
     assert(!funFlags.is(Erased) || !args.isEmpty, "An empty function cannot not be erased")
 
-    val funCls = defn.FunctionClass(args.length,
-        isContextual = funFlags.is(Given), isErased = funFlags.is(Erased))
+    val numArgs = args.length
+    val isContextual = funFlags.is(Given)
+    val isErased = funFlags.is(Erased)
+    val funCls = defn.FunctionClass(numArgs, isContextual, isErased)
+
+    /** If `app` is a function type with arguments that are all erased classes,
+     *  turn it into an erased function type.
+     */
+    def propagateErased(app: Tree): Tree = app match
+      case AppliedTypeTree(tycon: TypeTree, args)
+      if !isErased
+         && numArgs > 0
+         && args.indexWhere(!_.tpe.isErasedClass) == numArgs =>
+        val tycon1 = TypeTree(defn.FunctionClass(numArgs, isContextual, isErased = true).typeRef)
+          .withSpan(tycon.span)
+        assignType(cpy.AppliedTypeTree(app)(tycon1, args), tycon1, args)
+      case _ =>
+        app
 
     /** Typechecks dependent function type with given parameters `params` */
     def typedDependent(params: List[untpd.ValDef])(using Context): Tree =
@@ -1172,7 +1188,7 @@ class Typer extends Namer
       val resTpt = TypeTree(mt.nonDependentResultApprox).withSpan(body.span)
       val typeArgs = appDef.termParamss.head.map(_.tpt) :+ resTpt
       val tycon = TypeTree(funCls.typeRef)
-      val core = AppliedTypeTree(tycon, typeArgs)
+      val core = propagateErased(AppliedTypeTree(tycon, typeArgs))
       RefinedTypeTree(core, List(appDef), ctx.owner.asClass)
     end typedDependent
 
@@ -1181,7 +1197,8 @@ class Typer extends Namer
         typedDependent(args.asInstanceOf[List[untpd.ValDef]])(
           using ctx.fresh.setOwner(newRefinedClassSymbol(tree.span)).setNewScope)
       case _ =>
-        typed(cpy.AppliedTypeTree(tree)(untpd.TypeTree(funCls.typeRef), args :+ body), pt)
+        propagateErased(
+          typed(cpy.AppliedTypeTree(tree)(untpd.TypeTree(funCls.typeRef), args :+ body), pt))
     }
   }
 
@@ -2065,7 +2082,7 @@ class Typer extends Namer
       case rhs => typedExpr(rhs, tpt1.tpe.widenExpr)
     }
     val vdef1 = assignType(cpy.ValDef(vdef)(name, tpt1, rhs1), sym)
-    checkSignatureRepeatedParam(sym)
+    postProcessInfo(sym)
     vdef1.setDefTree
   }
 
@@ -2153,11 +2170,20 @@ class Typer extends Namer
 
     val ddef2 = assignType(cpy.DefDef(ddef)(name, paramss1, tpt1, rhs1), sym)
 
-    checkSignatureRepeatedParam(sym)
+    postProcessInfo(sym)
     ddef2.setDefTree
       //todo: make sure dependent method types do not depend on implicits or by-name params
   }
 
+  /** (1) Check that the signature of the class mamber does not return a repeated parameter type
+   *  (2) If info is an erased class, set erased flag of member
+   */
+  private def postProcessInfo(sym: Symbol)(using Context): Unit =
+    if (!sym.isOneOf(Synthetic | InlineProxy | Param) && sym.info.finalResultType.isRepeatedParam)
+      report.error(em"Cannot return repeated parameter type ${sym.info.finalResultType}", sym.srcPos)
+    if !sym.is(Module) && !sym.isConstructor && sym.info.finalResultType.isErasedClass then
+      sym.setFlag(Erased)
+
   def typedTypeDef(tdef: untpd.TypeDef, sym: Symbol)(using Context): Tree = {
     val TypeDef(name, rhs) = tdef
     completeAnnotations(tdef, sym)
diff --git a/compiler/test/dotty/tools/DottyTest.scala b/compiler/test/dotty/tools/DottyTest.scala
index b3b5c2f2fca6..43e387623d13 100644
--- a/compiler/test/dotty/tools/DottyTest.scala
+++ b/compiler/test/dotty/tools/DottyTest.scala
@@ -42,7 +42,7 @@ trait DottyTest extends ContextEscapeDetection {
   protected def initializeCtx(fc: FreshContext): Unit = {
     fc.setSetting(fc.settings.encoding, "UTF8")
     fc.setSetting(fc.settings.classpath, TestConfiguration.basicClasspath)
-    fc.setSetting(fc.settings.YerasedTerms, true)
+    fc.setSetting(fc.settings.language, List("experimental.erasedDefinitions"))
     fc.setProperty(ContextDoc, new ContextDocstrings)
   }
 
diff --git a/compiler/test/dotty/tools/dotc/BootstrappedOnlyCompilationTests.scala b/compiler/test/dotty/tools/dotc/BootstrappedOnlyCompilationTests.scala
index 528793ab50f0..e4fb84680123 100644
--- a/compiler/test/dotty/tools/dotc/BootstrappedOnlyCompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/BootstrappedOnlyCompilationTests.scala
@@ -118,7 +118,7 @@ class BootstrappedOnlyCompilationTests {
     aggregateTests(
       compileFilesInDir("tests/run-macros", defaultOptions.and("-Xcheck-macros")),
       compileFilesInDir("tests/run-custom-args/Yretain-trees", defaultOptions and "-Yretain-trees"),
-      compileFilesInDir("tests/run-custom-args/run-macros-erased", defaultOptions.and("-Yerased-terms").and("-Xcheck-macros")),
+      compileFilesInDir("tests/run-custom-args/run-macros-erased", defaultOptions.and("-language:experimental.erasedDefinitions").and("-Xcheck-macros")),
     )
   }.checkRuns()
 
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index b6266d5dac34..16ee334bc81c 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -39,7 +39,7 @@ class CompilationTests {
       compileFilesInDir("tests/pos-special/isInstanceOf", allowDeepSubtypes.and("-Xfatal-warnings")),
       compileFilesInDir("tests/new", defaultOptions),
       compileFilesInDir("tests/pos-scala2", scala2CompatMode),
-      compileFilesInDir("tests/pos-custom-args/erased", defaultOptions.and("-Yerased-terms")),
+      compileFilesInDir("tests/pos-custom-args/erased", defaultOptions.and("-language:experimental.erasedDefinitions")),
       compileFilesInDir("tests/pos", defaultOptions.and("-Ysafe-init")),
       compileFilesInDir("tests/pos-deep-subtype", allowDeepSubtypes),
       compileDir("tests/pos-special/java-param-names", defaultOptions.withJavacOnlyOptions("-parameters")),
@@ -126,7 +126,7 @@ class CompilationTests {
       compileFilesInDir("tests/neg-no-kind-polymorphism", defaultOptions and "-Yno-kind-polymorphism"),
       compileFilesInDir("tests/neg-custom-args/deprecation", defaultOptions.and("-Xfatal-warnings", "-deprecation")),
       compileFilesInDir("tests/neg-custom-args/fatal-warnings", defaultOptions.and("-Xfatal-warnings")),
-      compileFilesInDir("tests/neg-custom-args/erased", defaultOptions.and("-Yerased-terms")),
+      compileFilesInDir("tests/neg-custom-args/erased", defaultOptions.and("-language:experimental.erasedDefinitions")),
       compileFilesInDir("tests/neg-custom-args/allow-double-bindings", allowDoubleBindings),
       compileFilesInDir("tests/neg-custom-args/allow-deep-subtypes", allowDeepSubtypes),
       compileFilesInDir("tests/neg-custom-args/explicit-nulls", defaultOptions.and("-Yexplicit-nulls")),
@@ -165,7 +165,7 @@ class CompilationTests {
       compileDir("tests/neg-custom-args/adhoc-extension", defaultOptions.and("-source", "future", "-feature", "-Xfatal-warnings")),
       compileFile("tests/neg/i7575.scala", defaultOptions.withoutLanguageFeatures.and("-language:_")),
       compileFile("tests/neg-custom-args/kind-projector.scala", defaultOptions.and("-Ykind-projector")),
-      compileFile("tests/neg-custom-args/typeclass-derivation2.scala", defaultOptions.and("-Yerased-terms")),
+      compileFile("tests/neg-custom-args/typeclass-derivation2.scala", defaultOptions.and("-language:experimental.erasedDefinitions")),
       compileFile("tests/neg-custom-args/i5498-postfixOps.scala", defaultOptions withoutLanguageFeature "postfixOps"),
       compileFile("tests/neg-custom-args/deptypes.scala", defaultOptions.and("-language:experimental.dependent")),
       compileFile("tests/neg-custom-args/matchable.scala", defaultOptions.and("-Xfatal-warnings", "-source", "future")),
@@ -189,7 +189,7 @@ class CompilationTests {
       compileFile("tests/run-custom-args/fors.scala", defaultOptions.and("-source", "future")),
       compileFile("tests/run-custom-args/no-useless-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"),
       compileFile("tests/run-custom-args/defaults-serizaliable-no-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"),
-      compileFilesInDir("tests/run-custom-args/erased", defaultOptions.and("-Yerased-terms")),
+      compileFilesInDir("tests/run-custom-args/erased", defaultOptions.and("-language:experimental.erasedDefinitions")),
       compileFilesInDir("tests/run-deep-subtype", allowDeepSubtypes),
       compileFilesInDir("tests/run", defaultOptions.and("-Ysafe-init"))
     ).checkRuns()
@@ -248,7 +248,7 @@ class CompilationTests {
     val lib =
       compileList("lib", librarySources,
         defaultOptions.and("-Ycheck-reentrant",
-          "-Yerased-terms", // support declaration of scala.compiletime.erasedValue
+          "-language:experimental.erasedDefinitions", // support declaration of scala.compiletime.erasedValue
           //  "-source", "future",  // TODO: re-enable once we allow : @unchecked in pattern definitions. Right now, lots of narrowing pattern definitions fail.
           ))(libGroup)
 
diff --git a/compiler/test/dotty/tools/repl/ReplTest.scala b/compiler/test/dotty/tools/repl/ReplTest.scala
index 6fa5b6648bf6..0c2517dd0219 100644
--- a/compiler/test/dotty/tools/repl/ReplTest.scala
+++ b/compiler/test/dotty/tools/repl/ReplTest.scala
@@ -94,6 +94,6 @@ extends ReplDriver(options, new PrintStream(out, true, StandardCharsets.UTF_8.na
 }
 
 object ReplTest:
-  val commonOptions = Array("-color:never", "-Yerased-terms", "-pagewidth", "80")
+  val commonOptions = Array("-color:never", "-language:experimental.erasedDefinitions", "-pagewidth", "80")
   val defaultOptions = commonOptions ++ Array("-classpath", TestConfiguration.basicClasspath)
   lazy val withStagingOptions = commonOptions ++ Array("-classpath", TestConfiguration.withStagingClasspath)
diff --git a/docs/docs/reference/experimental/canthrow.md b/docs/docs/reference/experimental/canthrow.md
new file mode 100644
index 000000000000..261e4b3edd3e
--- /dev/null
+++ b/docs/docs/reference/experimental/canthrow.md
@@ -0,0 +1,241 @@
+---
+layout: doc-page
+title: CanThrow Abilities
+author: Martin Odersky
+---
+
+This page describes experimental support for exception checking in Scala 3. It is enabled by the language import
+```scala
+import language.experimental.saferExceptions
+```
+The reason for publishing this extension now is to get feedback on its usability. We are working on more advanced type systems that build on the general ideas put forward in the extension. Those type systems have application areas beyond checked exceptions. Exception checking is a useful starting point since exceptions are familiar to all Scala programmers and their current treatment leaves room for improvement.
+
+## Why Exceptions?
+
+Exceptions are an ideal mechanism for error handling in many situations. They serve the intended purpose of propagating error conditions with a minimum of boilerplate. They cause zero overhead for the "happy path", which means they are very efficient as long as errors arise infrequently. Exceptions are also debug friendly, since they produce stack traces that can be inspected at the handler site. So one never has to guess where an erroneous condition originated.
+
+## Why Not Exceptions?
+
+However, exceptions in current Scala and many other languages are not reflected in the type system. This means that an essential part of the contract of a function - i.e. what exceptions can it produce? - is not statically checked. Most people acknowledge that this is a problem, but that so far the alternative of checked exceptions was just too painful to be considered. A good example are Java checked exceptions, which do the right thing in principle, but are widely regarded as a mistake since they are so difficult to deal with. So far, none of the successor languages that are modeled after Java or that build on the JVM has copied this feature. See for example Anders Hejlsberg's [statement on why C# does not have checked exceptions](https://www.artima.com/articles/the-trouble-with-checked-exceptions).
+
+## The Problem With Java's Checked Exceptions
+
+The main problem with Java's checked exception model is its inflexibility, which is due to lack of polymorphism. Consider for instance the `map` function which is declared on `List[A]` like this:
+```scala
+  def map[B](f: A => B): List[B]
+```
+In the Java model, function `f` is not allowed to throw a checked exception. So the following call would be invalid:
+```scala
+  xs.map(x => if x < limit then x * x else throw LimitExceeded())
+```
+The only way around this would be to wrap the checked exception `LimitExceeded` in an unchecked `RuntimeException` that is caught at the callsite and unwrapped again. Something like this:
+```scala
+  try
+    xs.map(x => if x < limit then x * x else throw Wrapper(LimitExceeded()))
+  catch case Wrapper(ex) => throw ex
+```
+Ugh! No wonder checked exceptions in Java are not very popular.
+
+## Monadic Effects
+
+So the dilemma is that exceptions are easy to use only as long as we forgo static type checking. This has caused many people working with Scala to abandon exceptions altogether and to use an error monad like `Either` instead. This can work in many situations but is not without its downsides either. It makes code a lot more complicated and harder to refactor. It means one is quickly confronted with the problem how to work with several monads. In general, dealing with one monad at a time in Scala is straightforward but dealing with several monads together is much less pleasant since monads don't compose. A great number of techniques have been proposed, implemented, and promoted to deal with this, from monad transformers, to free monads, to tagless final. But none of these techniques is universally liked;  each introduces a complicated DSL that's hard to understand for non-experts, introduces runtime overheads, and makes debugging difficult. In the end, quite a few developers prefer to work instead with a single "super-monad" like ZIO that has error propagation built in alongside other aspects. This one-size fits all approach can work very nicely, even though (or is it because?) it represents an all-encompassing framework.
+
+However, a programming language is not a framework; it has to cater also for those applications that do not fit the framework's use cases. So there's still a strong motivation for getting exception checking right.
+
+## From Effects To Abilities
+
+Why does `map` work so poorly with Java's checked exception model? It's because
+`map`'s signature limits function arguments to not throw checked exceptions. We could try to come up with a more polymorphic formulation of `map`. For instance, it could look like this:
+```scala
+  def map[B, E](f: A => B canThrow E): List[B] canThrow E
+```
+This assumes a type `A canThrow E` to indicate computations of type `A` that can throw an exception of type `E`. But in practice the overhead of the additional type parameters makes this approach unappealing as well. Note in particular that we'd have to parameterize _every method_ that takes a function argument that way, so the added overhead of declaring all these exception types looks just like a sort of ceremony we would like to avoid.
+
+But there is a way to avoid the ceremony. Instead of concentrating on possible _effects_ such as "this code might throw an exception", concentrate on _capabilities_ such as "this code needs the capability to throw an exception". From a standpoint of expressiveness this is quite similar. But capabilities can be expressed as parameters whereas traditionally effects are expressed as some addition to result values. It turns out that this can make a big difference!
+
+Going to the root of the word _capability_, it means "being _able_ to do something", so the "cap" prefix is really just a filler. Following Conor McBride, we will use the name _ability_ from now on.
+
+## The CanThrow Ability
+
+In the _effects as abilities_ model, an effect is expressed as an (implicit) parameter of a certain type. For exceptions we would expect parameters of type
+`CanThrow[E]` where `E` stands for the exception that can be thrown. Here is the definition of `CanThrow`:
+```scala
+erased class CanThrow[-E <: Exception]
+```
+This shows another experimental Scala feature: [erased definitions](./erased-defs). Roughly speaking, values of an erased class do not generate runtime code; they are erased before code generation. This means that all `CanThrow` abilities are compile-time only artifacts; they do not have a runtime footprint.
+
+Now, if the compiler sees a `throw Exc()` construct where `Exc` is a checked exception, it will check that there is an ability of type `CanThrow[Exc]` that can be summoned as a given. It's a compile-time error if that's not the case.
+
+How can the ability be produced? There are several possibilities:
+
+Most often, the ability is produced by having a using clause `(using CanThrow[Exc])` in some enclosing scope. This roughly corresponds to a `throws` clause
+in Java. The analogy is even stronger since alongside `CanThrow` there is also the following type alias defined in the `scala` package:
+```scala
+infix type canThrow[R, +E <: Exception] = CanThrow[E] ?=> R
+```
+That is, `R canThrow E` is a context function type that takes an implicit `CanThrow[E]` parameter and that returns a value of type `R`. Therefore, a method written like this:
+```scala
+def m(x: T)(using CanThrow[E]): U
+```
+can alternatively be expressed like this:
+```scala
+def m(x: T): U canThrow E
+```
+_Aside_: If we rename `canThrow` to `throws` we would have a perfect analogy with Java but unfortunately `throws` is already taken in Scala 2.13.
+
+The `CanThrow`/`canThrow` combo essentially propagates the `CanThrow` requirement outwards. But where are these abilities created in the first place? That's in the `try` expression. Given a `try` like this:
+
+```scala
+try
+  body
+catch
+  case ex1: Ex1 => handler1
+  ...
+  case exN: ExN => handlerN
+```
+the compiler generates abilities for `CanThrow[Ex1]`, ..., `CanThrow[ExN]` that are in scope as givens in `body`. It does this by augmenting the `try` roughly as follows:
+```scala
+try
+  erased given CanThrow[Ex1] = ???
+  ...
+  erased given CanThrow[ExN] = ???
+  body
+catch ...
+```
+Note that the right-hand side of all givens is `???` (undefined). This is OK since
+these givens are erased; they will not be executed at runtime.
+
+## An Example
+
+That's it. Let's see it in action in an example. First, add an import
+```scala
+import language.experimental.saferExceptions
+```
+to enable exception checking. Now, define an exception `LimitExceeded` and
+a function `f` like this:
+```scala
+val limit = 10e9
+class LimitExceeded extends Exception
+def f(x: Double): Double =
+  if x < limit then x * x else throw LimitExceeded()
+```
+You'll get this error message:
+```
+9 |  if x < limit then x * x else throw LimitExceeded()
+  |                               ^^^^^^^^^^^^^^^^^^^^^
+  |The ability to throw exception LimitExceeded is missing.
+  |The ability can be provided by one of the following:
+  | - A using clause `(using CanThrow[LimitExceeded])`
+  | - A `canThrow` clause in a result type such as `X canThrow LimitExceeded`
+  | - an enclosing `try` that catches LimitExceeded
+  |
+  |The following import might fix the problem:
+  |
+  |  import unsafeExceptions.canThrowAny
+```
+As the error message implies, you have to declare that `f` needs the ability to throw a `LimitExceeded` exception. The most concise way to do so is to add a `canThrow` clause:
+```scala
+def f(x: Double): Double canThrow LimitExceeded =
+  if x < limit then x * x else throw LimitExceeded()
+```
+Now put a call to `f` in a `try` that catches `LimitExceeded`:
+```scala
+@main def test(xs: Double*) =
+  try println(xs.map(f).sum)
+  catch case ex: LimitExceeded => println("too large")
+```
+Run the program with some inputs:
+```
+> scala test 1 2 3
+14.0
+> scala test
+0.0
+> scala test 1 2 3 100000000000
+too large
+```
+Everything typechecks and works as expected. But wait - we have called `map` without any ceremony! How did that work? Here's how the compiler expands the `test` function:
+```scala
+// compiler-generated code
+@main def test(xs: Double*) =
+  try
+    erased given ctl: CanThrow[LimitExceeded] = ???
+    println(xs.map(x => f(x)(using ctl)).sum)
+  catch case ex: LimitExceeded => println("too large")
+```
+The `CanThrow[LimitExceeded]` ability is passed in a synthesized `using` clause to `f`, since `f` requires it. Then the resulting closure is passed to `map`. The signature of `map` does not have to account for effects. It takes a closure as always, but that
+closure may refer to abilities in its free variables. This means that `map` is
+already effect polymorphic even though we did not change its signature at all.
+So the takeaway is that the effects as abilities model naturally provides for effect polymorphism whereas this is something that other approaches struggle with.
+
+## Gradual Typing Via Imports
+
+Another advantage is that the model allows a gradual migration from current unchecked exceptions to safer exceptions. Imagine for a moment that `experimental.saferExceptions` is turned on everywhere. There would be lots of code that breaks since functions have not yet been properly annotated with `canThrow`. But it's easy to create an escape hatch that lets us ignore the breakages for a while: simply add the import
+```scala
+import scala.unsafeExceptions.canThrowAny
+```
+This will provide the `CanThrow` ability for any exception, and thereby allow
+all throws and all other calls, no matter what the current state of `canThrow` declarations is. Here's the
+definition of `canThrowAny`:
+```scala
+package scala
+object unsafeExceptions:
+  given canThrowAny: CanThrow[Exception] = ???
+```
+Of course, defining a global ability like this amounts to cheating. But the cheating is useful for gradual typing. The import could be used to migrate existing code, or to
+enable more fluid explorations of code without regard for complete exception safety. At the end of these migrations or explorations the import should be removed.
+
+## Scope Of the Extension
+
+To summarize, the extension for safer exception checking consists of the following elements:
+
+ - It adds to the standard library the class `scala.CanThrow`, the type `scala.canThrow`, and the `scala.unsafeExceptions` object, as they were described above.
+ - It augments the type checking of `throw` by _demanding_ a `CanThrow` ability or the thrown exception.
+ - It augments the type checking of `try` by _providing_ `CanThrow` abilities for every caught exception.
+
+That's all. It's quite remarkable that one can do exception checking in this way without any special additions to the type system. We just need regular givens and context functions. Any runtime overhead is eliminated using `erased`.
+
+## Caveats
+
+Our ability model allows to declare and check the thrown exceptions of first-order code. But as it stands, it does not give us enough mechanism to enforce the _absence_ of
+abilities for arguments to higher-order functions. Consider a variant `pureMap`
+of `map` that should enforce that its argument does not throw exceptions or have any other effects (maybe because wants to reorder computations transparently). Right now
+we cannot enforce that since the function argument to `pureMap` can capture arbitrary
+abilities in its free variables without them showing up in its type. One possible way to
+address this would be to introduce a pure function type (maybe written `A -> B`). Pure functions are not allowed to close over abilities. Then `pureMap` could be written
+like this:
+```
+  def pureMap(f: A -> B): List[B]
+```
+Another area where the lack of purity requirements shows up is when abilities escape from bounded scopes. Consider the following function
+```scala
+def escaped(xs: Double*): () => Int =
+  try () => xs.map(f).sum
+  catch case ex: LimitExceeded => -1
+```
+With the system presented here, this function typechecks, with expansion
+```scala
+// compiler-generated code
+def escaped(xs: Double*): () => Int =
+  try
+    given ctl: CanThrow[LimitExceeded] = ???
+    () => xs.map(x => f(x)(using ctl)).sum
+  catch case ex: LimitExceeded => -1
+```
+But if you try to call `escaped` like this
+```scala
+val g = escaped(1, 2, 1000000000)
+g()
+```
+the result will be a `LimitExceeded` exception thrown at the second line where `g` is called. What's missing is that `try` should enforce that the abilities it generates do not escape as free variables in the result of its body. It makes sense to describe such scoped effects as _ephemeral abilities_ - they have lifetimes that cannot be extended to delayed code in a lambda.
+
+
+# Outlook
+
+We are working on a new class of type system that supports ephemeral abilities by tracking the free variables of values. Once that research matures, it will hopefully be possible to augment the language so that we can enforce the missing properties.
+
+And it would have many other applications besides: Exceptions are a special case of _algebraic effects_, which has been a very active research area over the last 20 years and is finding its way into programming languages (e.g. Koka, Eff, Multicore OCaml, Unison). In fact, algebraic effects have been characterized as being equivalent to exceptions with an additional _resume_ operation. The techniques developed here for exceptions can probably be generalized to other classes of algebraic effects.
+
+But even without these additional mechanisms, exception checking is already useful as it is. It gives a clear path forward to make code that uses exceptions safer, better documented, and easier to refactor. The only loophole arises for scoped abilities - here we have to verify manually that these abilities do not escape. Specifically, a `try` always has to be placed in the same computation stage as the throws that it enables.
+
+Put another way: If the status quo is 0% static checking since 100% is too painful, then an alternative that gives you 95% static checking with great ergonomics looks like a win. And we might still get to 100% in the future.
+
diff --git a/docs/docs/reference/metaprogramming/erased-terms-spec.md b/docs/docs/reference/experimental/erased-defs-spec.md
similarity index 87%
rename from docs/docs/reference/metaprogramming/erased-terms-spec.md
rename to docs/docs/reference/experimental/erased-defs-spec.md
index 2930f336c5eb..ed8490f7e30e 100644
--- a/docs/docs/reference/metaprogramming/erased-terms-spec.md
+++ b/docs/docs/reference/experimental/erased-defs-spec.md
@@ -1,14 +1,16 @@
 ---
 layout: doc-page
-title: "Erased Terms Spec"
+title: "Erased Definitions: More Details"
 ---
 
+TODO: complete
 ## Rules
 
-1. The `erased` modifier can appear:
+1. `erased` is a soft modifier. It can appear:
    * At the start of a parameter block of a method, function or class
    * In a method definition
    * In a `val` definition (but not `lazy val` or `var`)
+   * In a `class` or `trait` definition
 
     ```scala
     erased val x = ...
@@ -20,10 +22,11 @@ title: "Erased Terms Spec"
     def h(x: (erased Int) => Int) = ...
 
     class K(erased x: Int) { ... }
+    erased class E {}
     ```
 
 
-2. A reference to an `erased` definition can only be used
+2. A reference to an `erased` val or def can only be used
    * Inside the expression of argument to an `erased` parameter
    * Inside the body of an `erased` `val` or `def`
 
diff --git a/docs/docs/reference/metaprogramming/erased-terms.md b/docs/docs/reference/experimental/erased-defs.md
similarity index 74%
rename from docs/docs/reference/metaprogramming/erased-terms.md
rename to docs/docs/reference/experimental/erased-defs.md
index 944d357d6daf..b5224fe687b4 100644
--- a/docs/docs/reference/metaprogramming/erased-terms.md
+++ b/docs/docs/reference/experimental/erased-defs.md
@@ -1,8 +1,14 @@
 ---
 layout: doc-page
-title: "Erased Terms"
+title: "Erased Definitions"
 ---
 
+`erased` is a modifier that expresses that some definition or expression is erased by the compiler instead of being represented in the compiled output. It is not yet part of the Scala language standard. To enable `erased`, turn on the language feature
+`experimental.erasedDefinitions`. This can be done with a language import
+```scala
+import scala.language.experimental.erasedDefinitions
+```
+or by setting the command line option `-language:experimental.erasedDefinitions`.
 ## Why erased terms?
 
 Let's describe the motivation behind erased terms with an example. In the
@@ -187,4 +193,36 @@ end Machine
    m.turnOn().turnOn() // error: Turning on an already turned on machine
 ```
 
-[More Details](./erased-terms-spec.md)
+## Erased Classes
+
+`erased` can also be used as a modifier for a class. An erased class is intended to be used only in erased definitions. If the type of a val definition or parameter is
+a (possibly aliased, refined, or instantiated) erased class, the definition is assumed to be `erased` itself. Likewise, a method with an erased class return type is assumed to be `erased` itself. Since given instances expand to vals and defs, they are also assumed to be erased if the type they produce is an erased class. Finally
+function types with erased classes as arguments turn into erased function types.
+
+Example:
+```scala
+erased class CanRead
+
+val x: CanRead = ...        // `x` is turned into an erased val
+val y: CanRead => Int = ... // the function is turned into an erased function
+def f(x: CanRead) = ...     // `f` takes an erased parameter
+def g(): CanRead = ...      // `g` is turned into an erased def
+given CanRead = ...         // the anonymous given is assumed to be erased
+```
+The code above expands to
+```scala
+erased class CanRead
+
+erased val x: CanRead = ...
+val y: (erased CanRead) => Int = ...
+def f(erased x: CanRead) = ...
+erased def g(): CanRead = ...
+erased given CanRead = ...
+```
+After erasure, it is checked that no references to values of erased classes remain and that no instances of erased classes are created. So the following would be an error:
+```scala
+val err: Any = CanRead() // error: illegal reference to erased class CanRead
+```
+Here, the type of `err` is `Any`, so `err` is not considered erased. Yet its initializing value is a reference to the erased class `CanRead`.
+
+[More Details](./erased-defs-spec.md)
diff --git a/library/src-non-bootstrapped/scala/compiletime/package.scala b/library/src-non-bootstrapped/scala/compiletime/package.scala
index 2d2e92bb00af..37d5a123c5da 100644
--- a/library/src-non-bootstrapped/scala/compiletime/package.scala
+++ b/library/src-non-bootstrapped/scala/compiletime/package.scala
@@ -2,6 +2,7 @@ package scala
 import annotation.compileTimeOnly
 
 package object compiletime {
+  import language.experimental.erasedDefinitions
 
   /** Use this method when you have a type, do not have a value for it but want to
    *  pattern match on it. For example, given a type `Tup <: Tuple`, one can
diff --git a/library/src/scala/annotation/internal/ContextResultCount.scala b/library/src/scala/annotation/internal/ContextResultCount.scala
index ab6b9ef0f6ba..ecaedb65bf4f 100644
--- a/library/src/scala/annotation/internal/ContextResultCount.scala
+++ b/library/src/scala/annotation/internal/ContextResultCount.scala
@@ -1,7 +1,7 @@
 package scala.annotation
 package internal
 
-/** An annotation that's aitomatically added for methods
+/** An annotation that's automatically added for methods
  *  that have one or more nested context closures as their right hand side.
  *  The parameter `n` is an Int Literal that tells how many nested closures
  *  there are.
diff --git a/library/src/scala/runtime/stdLibPatches/language.scala b/library/src/scala/runtime/stdLibPatches/language.scala
index cf95c0a2ff98..08fef20e3339 100644
--- a/library/src/scala/runtime/stdLibPatches/language.scala
+++ b/library/src/scala/runtime/stdLibPatches/language.scala
@@ -36,6 +36,13 @@ object language:
       * @see [[https://dotty.epfl.ch/docs/reference/changed-features/numeric-literals]]
       */
     object genericNumberLiterals
+
+    /** Experimental support for `erased` modifier
+     *
+     *  @see [[https://dotty.epfl.ch/docs/reference/experimental/erased-defs]]
+     */
+    object erasedDefinitions
+
   end experimental
 
   /** The deprecated object contains features that are no longer officially suypported in Scala.
diff --git a/project/Build.scala b/project/Build.scala
index 3a4816737e7b..9fcb9f1578a9 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -672,6 +672,8 @@ object Build {
       "-sourcepath", (Compile / sourceDirectories).value.map(_.getAbsolutePath).distinct.mkString(File.pathSeparator),
      // support declaration of scala.compiletime.erasedValue
       "-Yerased-terms"
+        // TODO: drop after bootstrap with erasure language import
+        // scala.compile now contains the roght language import so no global setting is needed
     ),
   )
 
diff --git a/tests/neg-custom-args/erased/erased-class.scala b/tests/neg-custom-args/erased/erased-class.scala
deleted file mode 100644
index 577165c0d70c..000000000000
--- a/tests/neg-custom-args/erased/erased-class.scala
+++ /dev/null
@@ -1 +0,0 @@
-erased class Test // error
diff --git a/tests/neg-custom-args/erased/erased-trait.scala b/tests/neg-custom-args/erased/erased-trait.scala
deleted file mode 100644
index d80ad3848b83..000000000000
--- a/tests/neg-custom-args/erased/erased-trait.scala
+++ /dev/null
@@ -1 +0,0 @@
-erased trait Test // error
diff --git a/tests/neg-custom-args/erased/i4058.scala b/tests/neg-custom-args/erased/i4058.scala
deleted file mode 100644
index e0a41b434ca7..000000000000
--- a/tests/neg-custom-args/erased/i4058.scala
+++ /dev/null
@@ -1 +0,0 @@
-sealed erased class E // error
diff --git a/tests/neg-custom-args/erased/i6795.scala b/tests/neg-custom-args/erased/i6795.scala
deleted file mode 100644
index 5bddc6d326b8..000000000000
--- a/tests/neg-custom-args/erased/i6795.scala
+++ /dev/null
@@ -1 +0,0 @@
-erased class Foo // error
diff --git a/tests/neg/erased-class.scala b/tests/neg/erased-class.scala
new file mode 100644
index 000000000000..29b28d7d5275
--- /dev/null
+++ b/tests/neg/erased-class.scala
@@ -0,0 +1,9 @@
+import language.experimental.erasedDefinitions
+erased class AA
+erased class BB extends AA // ok
+
+@main def Test =
+  val f1: Array[AA] = ??? // error
+  def f2(x: Int): Array[AA] = ??? // error
+  def bar: AA = ???  // ok
+  val baz: AA = ??? // ok
diff --git a/tests/neg/erased-inheritance.scala b/tests/neg/erased-inheritance.scala
new file mode 100644
index 000000000000..7be71e1632a5
--- /dev/null
+++ b/tests/neg/erased-inheritance.scala
@@ -0,0 +1,12 @@
+import language.experimental.erasedDefinitions
+erased class A
+erased class B extends A // ok
+
+class C extends A  // error
+
+erased trait D
+
+val x = new A{} // ok, x is erased
+val y = new C with D{} // error
+
+
diff --git a/tests/neg/i5525.scala b/tests/neg/i5525.scala
index d82d030b2e30..ceec2c90173f 100644
--- a/tests/neg/i5525.scala
+++ b/tests/neg/i5525.scala
@@ -29,6 +29,6 @@ enum Foo11 {
   protected case C9  // ok
 }
 
-enum Foo12 {  // error: enums must contain at least one case
-  inline    case C10() // error // error (inline treated as ident here)
+enum Foo12 {
+  inline    case C10() // error: only access modifiers allowed
 }
\ No newline at end of file
diff --git a/tests/neg/safeThrowsStrawman.check b/tests/neg/safeThrowsStrawman.check
new file mode 100644
index 000000000000..d0f0b8e60176
--- /dev/null
+++ b/tests/neg/safeThrowsStrawman.check
@@ -0,0 +1,16 @@
+-- Error: tests/neg/safeThrowsStrawman.scala:17:32 ---------------------------------------------------------------------
+17 |  if x then 1 else raise(Fail())  // error
+   |                                ^
+   |                                The capability to throw exception scalax.Fail is missing.
+   |                                The capability can be provided by one of the following:
+   |                                 - A using clause `(using CanThrow[scalax.Fail])`
+   |                                 - A throws clause in a result type such as `X throws scalax.Fail`
+   |                                 - an enclosing `try` that catches scalax.Fail
+-- Error: tests/neg/safeThrowsStrawman.scala:27:15 ---------------------------------------------------------------------
+27 |    println(bar)        // error
+   |               ^
+   |               The capability to throw exception Exception is missing.
+   |               The capability can be provided by one of the following:
+   |                - A using clause `(using CanThrow[Exception])`
+   |                - A throws clause in a result type such as `X throws Exception`
+   |                - an enclosing `try` that catches Exception
diff --git a/tests/neg/safeThrowsStrawman.scala b/tests/neg/safeThrowsStrawman.scala
new file mode 100644
index 000000000000..08f169e91701
--- /dev/null
+++ b/tests/neg/safeThrowsStrawman.scala
@@ -0,0 +1,29 @@
+import language.experimental.erasedDefinitions
+import annotation.implicitNotFound
+
+object scalax:
+  @implicitNotFound("The capability to throw exception ${E} is missing.\nThe capability can be provided by one of the following:\n - A using clause `(using CanThrow[${E}])`\n - A throws clause in a result type such as `X throws ${E}`\n - an enclosing `try` that catches ${E}")
+  erased class CanThrow[-E <: Exception]
+
+  infix type throws[R, +E <: Exception] = CanThrow[E] ?=> R
+
+  class Fail extends Exception
+
+  def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+import scalax._
+
+def foo(x: Boolean): Int =
+  if x then 1 else raise(Fail())  // error
+
+def bar: Int throws Exception =
+  raise(Fail())
+
+@main def Test =
+  try
+    erased given CanThrow[Fail] = ???
+    println(foo(true))
+    println(foo(false))
+    println(bar)        // error
+  catch case ex: Fail =>
+    println("failed")
diff --git a/tests/neg/safeThrowsStrawman2.scala b/tests/neg/safeThrowsStrawman2.scala
new file mode 100644
index 000000000000..80e5139b1f8d
--- /dev/null
+++ b/tests/neg/safeThrowsStrawman2.scala
@@ -0,0 +1,33 @@
+import language.experimental.erasedDefinitions
+
+object scalax:
+  erased class CanThrow[E <: Exception]
+  type CTF = CanThrow[Fail]
+
+  infix type throws[R, E <: Exception] = CanThrow[E] ?=> R
+
+  class Fail extends Exception
+
+  def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+import scalax._
+
+def foo(x: Boolean, y: CanThrow[Fail]): Int throws Fail =
+  if x then 1 else raise(Fail())
+
+def bar(x: Boolean)(using CanThrow[Fail]): Int =
+  if x then 1 else raise(Fail())
+
+@main def Test =
+  try
+    given ctf: CanThrow[Fail] = ???
+    val x = new CanThrow[Fail]()      // OK, x is erased
+    val y: Any = new CanThrow[Fail]() // error: illegal reference to erased class CanThrow
+    val y2: Any = new CTF()       // error: illegal reference to erased class CanThrow
+    println(foo(true, ctf))       // error: ctf is declared as erased, but is in fact used
+    val a = (1, new CanThrow[Fail]()) // error: illegal reference to erased class CanThrow
+    def b: (Int, CanThrow[Fail]) = ???
+    def c = b._2                  // ok; we only check creation sites
+    bar(true)(using ctf)
+  catch case ex: Fail =>
+    println("failed")
diff --git a/tests/pos/CanThrow.scala b/tests/pos/CanThrow.scala
new file mode 100644
index 000000000000..f1603d4245c1
--- /dev/null
+++ b/tests/pos/CanThrow.scala
@@ -0,0 +1,13 @@
+package canThrowStrawman
+import language.experimental.erasedDefinitions
+
+class CanThrow[E <: Exception]
+
+infix type throws[R, E <: Exception] = (erased CanThrow[E]) ?=> R
+
+class Fail extends Exception
+
+def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+def foo(x: Boolean): Int throws Fail =
+  if x then 1 else raise(Fail())
diff --git a/tests/pos/erased-class-separate/A_1.scala b/tests/pos/erased-class-separate/A_1.scala
new file mode 100644
index 000000000000..5c874ce6d89b
--- /dev/null
+++ b/tests/pos/erased-class-separate/A_1.scala
@@ -0,0 +1,3 @@
+import language.experimental.erasedDefinitions
+erased class A
+
diff --git a/tests/pos/erased-class-separate/Test_2.scala b/tests/pos/erased-class-separate/Test_2.scala
new file mode 100644
index 000000000000..f3d1e15f04b0
--- /dev/null
+++ b/tests/pos/erased-class-separate/Test_2.scala
@@ -0,0 +1,2 @@
+import language.experimental.erasedDefinitions
+erased val x: A = A()
diff --git a/tests/pos/erased-conforms.scala b/tests/pos/erased-conforms.scala
new file mode 100644
index 000000000000..1f366e0683c6
--- /dev/null
+++ b/tests/pos/erased-conforms.scala
@@ -0,0 +1,20 @@
+import language.experimental.erasedDefinitions
+erased class ErasedTerm
+
+erased class <::<[-From, +To] extends ErasedTerm
+
+erased class =::=[From, To] extends (From <::< To)
+
+erased given [X]: (X =::= X) = scala.compiletime.erasedValue
+
+extension [From](x: From)
+  inline def cast[To](using From <::< To): To = x.asInstanceOf[To] // Safe cast because we know `From <:< To`
+
+
+def convert[A, B](a: A)(using /*erased*/ x: A <::< B): B =
+  // println(x) // error: OK because x should be erased
+                // but currently x is not marked as erased which it should
+  a.cast[B]
+
+
+@main def App: Unit = convert[Int, Int](3) // should not be an error
diff --git a/tests/pos/i11743.scala b/tests/pos/i11743.scala
new file mode 100644
index 000000000000..ae524ca01ad6
--- /dev/null
+++ b/tests/pos/i11743.scala
@@ -0,0 +1,8 @@
+import language.experimental.erasedDefinitions
+import scala.compiletime.erasedValue
+type UnivEq[A]
+object UnivEq:
+  erased def force[A]: UnivEq[A] = erasedValue
+  extension [A](erased proof: UnivEq[A])
+    inline def univEq(a: A, b: A): Boolean =
+      a == b
diff --git a/tests/run/safeThrowsStrawman.check b/tests/run/safeThrowsStrawman.check
new file mode 100644
index 000000000000..3b8b7ee861f0
--- /dev/null
+++ b/tests/run/safeThrowsStrawman.check
@@ -0,0 +1,3 @@
+1
+failed
+failed
diff --git a/tests/run/safeThrowsStrawman.scala b/tests/run/safeThrowsStrawman.scala
new file mode 100644
index 000000000000..8ddb594b787a
--- /dev/null
+++ b/tests/run/safeThrowsStrawman.scala
@@ -0,0 +1,31 @@
+import language.experimental.erasedDefinitions
+
+object scalax:
+  erased class CanThrow[-E <: Exception]
+
+  infix type throws[R, +E <: Exception] = CanThrow[E] ?=> R
+
+  class Fail extends Exception
+
+  def raise[E <: Exception](e: E): Nothing throws E = throw e
+
+import scalax._
+
+def foo(x: Boolean): Int throws Fail =
+  if x then 1 else raise(Fail())
+
+def bar(x: Boolean)(using CanThrow[Fail]): Int = foo(x)
+def baz: Int throws Exception = foo(false)
+
+@main def Test =
+  try
+    given CanThrow[Fail] = ???
+    println(foo(true))
+    println(foo(false))
+  catch case ex: Fail =>
+    println("failed")
+  try
+    given CanThrow[Exception] = ???
+    println(baz)
+  catch case ex: Fail =>
+    println("failed")