Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

regression: crash when summoning type equivalence #18650

Closed
p-pavel opened this issue Oct 4, 2023 · 3 comments · Fixed by #18719
Closed

regression: crash when summoning type equivalence #18650

p-pavel opened this issue Oct 4, 2023 · 3 comments · Fixed by #18719
Assignees
@dwijnand
Labels
area:typer itype:bug itype:crash regression This worked in a previous version but doesn't anymore

Comments

@p-pavel
Copy link

p-pavel commented Oct 4, 2023 •
edited by bishabosha
Loading

Compiler version

3.3.1

Minimized code

I know the code may look a bit strange, but this is what I could reproduce:

trait Lam:
  type F[_]
  extension [A, B](f: F[A => B]) def apply(arg: F[A]): F[B]
  def lam[A, B](f: F[A] => F[B]): F[A => B]
  final def id[A]: F[A => A] = lam(identity[F[A]])

object LamInterpreter extends Lam:
  type F[t] = t
  def lam[A, B](f: F[A] => F[B]): F[A => B] = f
  extension [A, B](f: F[A => B]) def apply(arg: F[A]): F[B] = f(arg)


class Church[A](using val l: Lam):
  import l.*
  type Nat = F[(A => A) => (A => A)]
  def zero: Nat = id
  extension (n: Nat) def suc: Nat = lam(f => lam(x => f(n(f)(x))))

given [A](using l: Lam): Church[A] = Church()


@main
def churchTest = 
  given Lam = LamInterpreter
  val c: Church[Int] = summon
  summon[c.Nat =:= ((Int => Int) => (Int => Int))]

Output

Stack trace 
java.lang.AssertionError: assertion failed while typechecking a.scala
exception occurred while typechecking a.scala

  exception occurred while compiling List(a.scala)

  An unhandled exception was thrown in the compiler.
  Please file a crash report here:
  https://github.com/lampepfl/dotty/issues/new/choose

     while compiling: <no file>
        during phase: <no phase>
                mode: Mode(ImplicitsEnabled)
     library version: version 2.13.10
    compiler version: version 3.3.1
            settings: -d out -usejavacp true

                tree: EmptyTree
       tree position: :<unknown>
           tree type: <notype>
              symbol: val <none>
           call site: package <root> in module class <root>

  == Source file context for tree position ==


Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:11)
        at dotty.tools.dotc.ast.tpd$.TypeApply(tpd.scala:60)
        at dotty.tools.dotc.ast.tpd$TreeOps$.appliedToTypeTrees$extension(tpd.scala:985)
        at dotty.tools.dotc.typer.Typer.adapt1(Typer.scala:4255)
        at dotty.tools.dotc.typer.Typer.adapt(Typer.scala:3587)
        at dotty.tools.dotc.typer.ProtoTypes$FunProto.typedArg(ProtoTypes.scala:497)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:897)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:897)
        at dotty.tools.dotc.typer.Applications$Application.addTyped$1(Applications.scala:589)
        at dotty.tools.dotc.typer.Applications$Application.matchArgs(Applications.scala:653)
        at dotty.tools.dotc.typer.Applications$Application.init(Applications.scala:492)
        at dotty.tools.dotc.typer.Applications$TypedApply.<init>(Applications.scala:779)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.<init>(Applications.scala:896)
        at dotty.tools.dotc.typer.Applications.ApplyTo(Applications.scala:1126)
        at dotty.tools.dotc.typer.Applications.ApplyTo$(Applications.scala:352)
        at dotty.tools.dotc.typer.Typer.ApplyTo(Typer.scala:116)
        at dotty.tools.dotc.typer.Applications.simpleApply$1(Applications.scala:969)
        at dotty.tools.dotc.typer.Applications.realApply$1$$anonfun$2(Applications.scala:1052)
        at dotty.tools.dotc.typer.Typer.tryEither(Typer.scala:3324)
        at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:1063)
        at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:1101)
        at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:352)
        at dotty.tools.dotc.typer.Typer.typedApply(Typer.scala:116)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3048)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3112)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Implicits.tryConversion$1(Implicits.scala:1136)
        at dotty.tools.dotc.typer.Implicits.typedImplicit(Implicits.scala:1167)
        at dotty.tools.dotc.typer.Implicits.typedImplicit$(Implicits.scala:818)
        at dotty.tools.dotc.typer.Typer.typedImplicit(Typer.scala:116)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.tryImplicit(Implicits.scala:1242)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.rank$1(Implicits.scala:1341)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.searchImplicit(Implicits.scala:1511)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.searchImplicit(Implicits.scala:1539)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.searchImplicit(Implicits.scala:1547)
        at dotty.tools.dotc.typer.Implicits$ImplicitSearch.bestImplicit(Implicits.scala:1572)
        at dotty.tools.dotc.typer.Implicits.inferImplicit(Implicits.scala:1060)
        at dotty.tools.dotc.typer.Implicits.inferImplicit$(Implicits.scala:818)
        at dotty.tools.dotc.typer.Typer.inferImplicit(Typer.scala:116)
        at dotty.tools.dotc.typer.Implicits.inferView(Implicits.scala:856)
        at dotty.tools.dotc.typer.Implicits.inferView$(Implicits.scala:818)
        at dotty.tools.dotc.typer.Typer.inferView(Typer.scala:116)
        at dotty.tools.dotc.typer.Implicits.viewExists(Implicits.scala:831)
        at dotty.tools.dotc.typer.Implicits.viewExists$(Implicits.scala:818)
        at dotty.tools.dotc.typer.Typer.viewExists(Typer.scala:116)
        at dotty.tools.dotc.typer.Implicits.ignoredConvertibleImplicits$1$$anonfun$3(Implicits.scala:960)
        at scala.collection.Iterator$$anon$6.hasNext(Iterator.scala:479)
        at scala.collection.Iterator.isEmpty(Iterator.scala:466)
        at scala.collection.Iterator.isEmpty$(Iterator.scala:466)
        at scala.collection.AbstractIterator.isEmpty(Iterator.scala:1300)
        at scala.collection.View$Filter.isEmpty(View.scala:146)
        at scala.collection.IterableOnceOps.nonEmpty(IterableOnce.scala:833)
        at scala.collection.IterableOnceOps.nonEmpty$(IterableOnce.scala:833)
        at scala.collection.AbstractIterable.nonEmpty(Iterable.scala:933)
        at dotty.tools.dotc.reporting.MissingImplicitArgument.noChainConversionsNote$1(messages.scala:2838)
        at dotty.tools.dotc.reporting.MissingImplicitArgument.msgPostscript$$anonfun$4(messages.scala:2846)
        at scala.Option.orElse(Option.scala:477)
        at dotty.tools.dotc.reporting.MissingImplicitArgument.msgPostscript(messages.scala:2846)
        at dotty.tools.dotc.reporting.Message.message$$anonfun$1(Message.scala:345)
        at dotty.tools.dotc.reporting.Message.inMessageContext(Message.scala:341)
        at dotty.tools.dotc.reporting.Message.message(Message.scala:345)
        at dotty.tools.dotc.reporting.Message.isNonSensical(Message.scala:322)
        at dotty.tools.dotc.reporting.HideNonSensicalMessages.isHidden(HideNonSensicalMessages.scala:16)
        at dotty.tools.dotc.reporting.HideNonSensicalMessages.isHidden$(HideNonSensicalMessages.scala:10)
        at dotty.tools.dotc.reporting.AbstractReporter.isHidden(AbstractReporter.scala:8)
        at dotty.tools.dotc.reporting.Reporter.issueUnconfigured(Reporter.scala:156)
        at dotty.tools.dotc.reporting.Reporter.go$1(Reporter.scala:181)
        at dotty.tools.dotc.reporting.Reporter.issueIfNotSuppressed(Reporter.scala:200)
        at dotty.tools.dotc.reporting.Reporter.report(Reporter.scala:203)
        at dotty.tools.dotc.report$.error(report.scala:68)
        at dotty.tools.dotc.typer.Typer.issueErrors$1$$anonfun$1(Typer.scala:3808)
        at scala.runtime.function.JProcedure3.apply(JProcedure3.java:15)
        at scala.runtime.function.JProcedure3.apply(JProcedure3.java:10)
        at scala.collection.LazyZip3.foreach(LazyZipOps.scala:248)
        at dotty.tools.dotc.typer.Typer.issueErrors$1(Typer.scala:3810)
        at dotty.tools.dotc.typer.Typer.addImplicitArgs$1(Typer.scala:3832)
        at dotty.tools.dotc.typer.Typer.adaptNoArgsImplicitMethod$1(Typer.scala:3849)
        at dotty.tools.dotc.typer.Typer.adaptNoArgs$1(Typer.scala:4038)
        at dotty.tools.dotc.typer.Typer.adapt1(Typer.scala:4268)
        at dotty.tools.dotc.typer.Typer.adapt(Typer.scala:3587)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3188)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3300)
        at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:1166)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3056)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3112)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3188)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3300)
        at dotty.tools.dotc.typer.Namer.typedAheadExpr$$anonfun$1(Namer.scala:1653)
        at dotty.tools.dotc.typer.Namer.typedAhead(Namer.scala:1643)
        at dotty.tools.dotc.typer.Namer.typedAheadExpr(Namer.scala:1653)
        at dotty.tools.dotc.typer.Namer.typedAheadRhs$1$$anonfun$1(Namer.scala:1906)
        at dotty.tools.dotc.inlines.PrepareInlineable$.dropInlineIfError(PrepareInlineable.scala:243)
        at dotty.tools.dotc.typer.Namer.typedAheadRhs$1(Namer.scala:1906)
        at dotty.tools.dotc.typer.Namer.rhsType$1(Namer.scala:1914)
        at dotty.tools.dotc.typer.Namer.cookedRhsType$1(Namer.scala:1932)
        at dotty.tools.dotc.typer.Namer.lhsType$1(Namer.scala:1933)
        at dotty.tools.dotc.typer.Namer.inferredResultType(Namer.scala:1944)
        at dotty.tools.dotc.typer.Namer.inferredType$1(Namer.scala:1691)
        at dotty.tools.dotc.typer.Namer.valOrDefDefSig(Namer.scala:1698)
        at dotty.tools.dotc.typer.Namer.defDefSig(Namer.scala:1789)
        at dotty.tools.dotc.typer.Namer$Completer.typeSig(Namer.scala:791)
        at dotty.tools.dotc.typer.Namer$Completer.completeInCreationContext(Namer.scala:934)
        at dotty.tools.dotc.typer.Namer$Completer.complete(Namer.scala:814)
        at dotty.tools.dotc.core.SymDenotations$SymDenotation.completeFrom(SymDenotations.scala:174)
        at dotty.tools.dotc.core.Denotations$Denotation.completeInfo$1(Denotations.scala:187)
        at dotty.tools.dotc.core.Denotations$Denotation.info(Denotations.scala:189)
        at dotty.tools.dotc.core.SymDenotations$SymDenotation.ensureCompleted(SymDenotations.scala:393)
        at dotty.tools.dotc.typer.Typer.retrieveSym(Typer.scala:2989)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:3014)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3111)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3188)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3210)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3256)
        at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:2669)
        at dotty.tools.dotc.typer.Typer.typedTypeOrClassDef$1(Typer.scala:3036)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:3040)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3111)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3188)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3210)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3256)
        at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:2812)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3081)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3112)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3184)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3188)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3300)
        at dotty.tools.dotc.typer.TyperPhase.typeCheck$$anonfun$1(TyperPhase.scala:44)
        at dotty.tools.dotc.typer.TyperPhase.typeCheck$$anonfun$adapted$1(TyperPhase.scala:54)
        at scala.Function0.apply$mcV$sp(Function0.scala:42)
        at dotty.tools.dotc.core.Phases$Phase.monitor(Phases.scala:440)
        at dotty.tools.dotc.typer.TyperPhase.typeCheck(TyperPhase.scala:54)
        at dotty.tools.dotc.typer.TyperPhase.runOn$$anonfun$3(TyperPhase.scala:88)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at dotty.tools.dotc.typer.TyperPhase.runOn(TyperPhase.scala:88)
        at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:246)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
        at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1321)
        at dotty.tools.dotc.Run.runPhases$1(Run.scala:262)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:270)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:279)
        at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:67)
        at dotty.tools.dotc.Run.compileUnits(Run.scala:279)
        at dotty.tools.dotc.Run.compileSources(Run.scala:194)
        at dotty.tools.dotc.Run.compile(Run.scala:179)
        at dotty.tools.dotc.Driver.doCompile(Driver.scala:37)
        at dotty.tools.dotc.Driver.process(Driver.scala:197)
        at dotty.tools.dotc.Driver.process(Driver.scala:165)
        at dotty.tools.dotc.Driver.process(Driver.scala:177)
        at dotty.tools.dotc.Driver.main(Driver.scala:207)
        at dotty.tools.dotc.Main.main(Main.scala)
@p-pavel p-pavel added itype:bug itype:crash stat:needs triage Every issue needs to have an "area" and "itype" label labels Oct 4, 2023
@bishabosha bishabosha added area:typer and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Oct 16, 2023
@bishabosha
Copy link
Member

bishabosha commented Oct 16, 2023 •
edited
Loading

I added the correct stack trace

@bishabosha
Copy link
Member

bishabosha commented Oct 16, 2023 •
edited
Loading

minimized to:

//> using scala 3.3.1

class Church[A]():
  type F[_]
  type Nat = F[(A => A) => (A => A)]

given makeChurch[A]: Church[A] = ??? // necessary to cause crash

@main
def churchTest =
  val c: Church[Int] = ???
  summon[c.Nat =:= ((Int => Int) => (Int => Int))]

@bishabosha bishabosha added the regression This worked in a previous version but doesn't anymore label Oct 16, 2023
@bishabosha
Copy link
Member

bishabosha commented Oct 16, 2023 •
edited
Loading

in 3.3.0 there was no crash, however there was still a type error.

It seems the crashing assertion is to check in tpd.TypeApply that errors were already reported, so either no error was reported, or the kind of tree was unexpected

@bishabosha bishabosha changed the title Compiler crash when trying to summon type equivalence regression: crash when summoning type equivalence Oct 16, 2023
@dwijnand dwijnand mentioned this issue Oct 18, 2023
Merged
odersky added a commit that referenced this issue Oct 19, 2023
@odersky
Fix widen types before checking an implicit view exists (#18719)
bf994f9 
Fixes #18650
@dwijnand dwijnand mentioned this issue Dec 15, 2023
Merged
odersky added a commit that referenced this issue Dec 17, 2023
@odersky
Avoid diagnostic message forcing crashing the compiler (#19113)
10f2c10 
Using issue #18650 as the reference (but issue #18999 is another option)
building on the fix in PR #18719 (refined in PR #18727) as well as the
fix in PR #18760, I'm trying to make a more root change here by making
sure that message forcing only occurs with `hasErrors`/`errorsReported`
is true, so as to avoid assertion errors crashing the compiler.
This was referenced Dec 23, 2023
Closed
Open
@987Nabil 987Nabil mentioned this issue Jan 7, 2024
Closed
dwijnand pushed a commit to dwijnand/scala3 that referenced this issue Feb 21, 2024
@odersky @dwijnand
Avoid diagnostic message forcing crashing the compiler (scala#19113)
2459549 
Using issue scala#18650 as the reference (but issue scala#18999 is another option)
building on the fix in PR scala#18719 (refined in PR scala#18727) as well as the
fix in PR scala#18760, I'm trying to make a more root change here by making
sure that message forcing only occurs with `hasErrors`/`errorsReported`
is true, so as to avoid assertion errors crashing the compiler.

(cherry picked from commit 10f2c10)
dwijnand pushed a commit to dwijnand/scala3 that referenced this issue Mar 5, 2024
@odersky @dwijnand
Avoid diagnostic message forcing crashing the compiler (scala#19113)
e300188 
Using issue scala#18650 as the reference (but issue scala#18999 is another option)
building on the fix in PR scala#18719 (refined in PR scala#18727) as well as the
fix in PR scala#18760, I'm trying to make a more root change here by making
sure that message forcing only occurs with `hasErrors`/`errorsReported`
is true, so as to avoid assertion errors crashing the compiler.

(cherry picked from commit 10f2c10)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@dwijnand dwijnand

Labels
area:typer itype:bug itype:crash regression This worked in a previous version but doesn't anymore
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix widen types before checking an implicit view exists dwijnand/scala3
3 participants
@dwijnand @p-pavel @bishabosha