fromRise fails when a type variable should be a basic type (or other constraint)

[Bastacyclop]

Example:

  // average two positive values rounding up
  val avg: Expr = dtFun(dt => dtFun(compute_dt => fun(
    dt ->: dt ->: dt
  )((a, b) => {
    val cast_ = fun(a => cast(a) :: compute_dt)
    cast((cast_(a) + cast_(b) + cast_(l(1))) / cast_(l(2))) :: dt
  })))

  test("failure") {
    shine.DPIA.fromRise(infer(avg(i16)(i32)))
  }

More precisely, the pattern match in fromRise cannot not pass since TypeVariable is not a BasicType:

      case (core.Cast(), lt.FunType(la: lt.BasicType, lb: lt.BasicType))
      =>
        val a = basicType(la)
        val b = basicType(lb)
        fun[ExpType](ExpType(a, read), x =>
          Cast(a, b, x))

This is closely related to rise-lang/rise#11.

[Bastacyclop]

Currently this is issue is fixed by beta-reducing nat dependent lambdas in fromRise. The idea is that we should always have concrete data types when going to code generation and thus we can eliminate all data type variables.

[bastian-koepcke]

Does this mean the issue has been resolved?

[Bastacyclop]

@bastian-koepcke Well, I am happy with this solution. We can close the issue if there is no objection.
@rise-lang/core