Help needed teasing apart compiler bugs

Compiler
1

I don’t know how to report this, and I don’t know where one bug ends and another starts…

See this code.

Language features involved:

  • inline
  • match types
  • dependently typed function types
  • transparent
2

Interestingly, by removing the type assertions for the dependently typed transparent case, then it starts working again. Although you do need to typecast the result since the compiler can’t infer “n’s” type correctly (not sure why though)

transparent inline def transparentInlineDependentlyTypedMod2[N <: NatT](inline n: N): Mod2[N] = inline n match
  case Zero() => Zero().asInstanceOf[Mod2[N]]
  case Succ(Zero()) => Succ(Zero()).asInstanceOf[Mod2[N]]
  case Succ(Succ(predPredN)) => transparentInlineDependentlyTypedMod2(predPredN).asInstanceOf[Mod2[N]]

but in this case, dependent typing is kind of not needed, since “transparent” should refine the type for you.

1 Like
3

ticket