Source modality boxing could be wrong

[amosr]

the current boxing/reboxing for applications might be wrong for this case

countfrom v
 = fold x = v
   then x + 1
 ~> x

countfrom : Int -> Aggregate Int

however, I believe the application rule would let us apply an aggregate to this, because the return type is aggregate.

countfrom 0 : Aggregate Int
countfrom (countfrom 0) : Aggregate Int

countfrom (countfrom 0)
 = fold x = (fold x1 = 0 then x1 + 1 ~> x1)
   then x + 1
 ~> x
 : type error

I must look into this at some point

[amosr]

just thinking about this. when we reimplement the typechecker for Sorbet, we want to distinguish this unbox-rebox case: it is valid for Possibly, but not valid for Temporality. you can unbox a Possibly to a pure thing, but you can't turn back time.