Disallow covariant subtyping in checker

[darkdrag00nv2]

Issue to be solved

Came out of: https://github.com/onflow/cadence/pull/2523/files#r1361276644

Sorry I forgot some of the details, is it possible to create an InclusiveRange<Integer> in cadence?
i.e: Is following allowed?

let a: Integer = 0
let b: Integer = 10
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

It seems not just the constructor, the checker also allows covariant subtyping:
e.g:

let a: InclusiveRange<Int> = InclusiveRange(0, 10)
let b: InclusiveRange<Integer> = a

This would need to be fixed in the IsSubType() method, which would fix it universally (won't need to special case in multiple places)

[darkdrag00nv2]

@SupunS Need a bit of help.

I looked into the second part of the issue. Basically the following:

let a: InclusiveRange<Int> = InclusiveRange(0, 10)
let b: InclusiveRange<Integer> = a

You are right that it is being allowed in the checker. The code:

cadence/runtime/sema/type.go

Lines 6312 to 6313 in 323b887

	// T<Us> <: V<Ws>
	// if T <: V && |Us| == |Ws| && U_i <: W_i

I have superficial understanding of this but it doesn't seem like a bug and more like a choice. Do we really want to disable covariant subtyping of parameterized types? It might also affect other existing parameterized types.

I am wondering if we can rethink if it is possible to support the covariant sub-typing with InclusiveRange as well. The main constraint we need is that the static type of start, end and step must be equal so that we can do comparisons among them.

Else if we still want to disallow, then may be we need a hard-coded check for InclusiveRange for T = Integer, SignedInteger. It will also help with the below two cases.

let a: Integer = 0
let b: Integer = 10
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

let a: Integer = 0
let b: Integer = Int8(10)
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

cc: @turbolent

[SupunS]

I have superficial understanding of this but it doesn't seem like a bug and more like a choice. Do we really want to disable covariant subtyping of parameterized types? It might also affect other existing parameterized types.

Yes agreed, that it's a choice we made. The problem in this case is that covariance for InclusiveRange is allowed in some places, and not allowed in other places. My suggestion was actually that we should make it consistent and have the same behavior in all places (in constructor, assignment, importing, type-inferring, etc), whichever option we pick.

I think there were a few reasons not to allow covariance, like for example, the runtime needed to check the types (do we do that already?), etc. I don't remember all the details / other reasons, need to dig up the previous discussions.

The main constraint we need is that the static type of start, end and step must be equal so that we can do comparisons among them.

Don't think we can enforce this statically. In the example:

let a: Integer = 0
let b: Integer = Int8(10)
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

The runtime type of a and b can never be guaranteed to be the same statically.

[turbolent]

Given that type parameters can still only be defined for built-in types, would it help add a notion of variance to type parameters? Something along the lines of e.g. Scala

[darkdrag00nv2]

the runtime needed to check the types (do we do that already?), etc

We check the equality of static types of start, end and also step during the creation of InclusiveRange and also during import.

cadence/runtime/stdlib/range.go

Lines 95 to 106 in 7ab492f

	startStaticType := start.StaticType(inter)
	endStaticType := end.StaticType(inter)
	if !startStaticType.Equal(endStaticType) {
	panic(interpreter.InclusiveRangeConstructionError{
	LocationRange: locationRange,
	Message: fmt.Sprintf(
	"start and end are of different types. start: %s and end: %s",
	startStaticType,
	endStaticType,
	),
	})
	}

---

Don't think we can enforce this statically. In the example:

let a: Integer = 0
let b: Integer = Int8(10)
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

The runtime type of a and b can never be guaranteed to be the same statically.

Wouldn't a have a static type of PrimitiveStaticTypeInt and b of PrimitiveStaticTypeInt8? In that case, the check I shared above should be able to detect it.

[SupunS]

Ah, there is a bit of confusion. When I said "can never be guaranteed statically", I meant during the checking time. i.e: just by using the static analysis of the program, without executing it.
The "static type" (the name here can be confusing) is the run-time type of the value.

[SupunS]

So yeah, given the run-time/interpreter already handles it, we can allow it in the checker as well.

But a couple of things to be mindful here is that:

1. if someone writes an invalid code like below, it will only fail dynamically when they execute the program.

   let a: Integer = 0
   let b: Integer = Int8(10)
   var range: InclusiveRange<Integer> = InclusiveRange(a, b)

2. If we allow this now, then in future if we add a notion of variance to type parameters, like Bastian mentioned, we won't be able to undo allowing InclusiveRange<Integer> because it is going to be a breaking change. i.e: We won't be able to enforce using InclusiveRange<only subtype of Integer> since it is a breaking change.

[darkdrag00nv2]

okay, then let me look into the variance idea. It is definitely desirable to catch errors in the checker if possible.

[darkdrag00nv2]

@turbolent @SupunS I looked into the variance idea.

IIUC, if we make InclusiveRange<T> invariant, then it'll help with the following case since InclusiveRange<Int> will not be a sub-type of InclusiveRange<Integer>.

let a: InclusiveRange<Int> = InclusiveRange(0, 10)
let b: InclusiveRange<Integer> = a // will fail

But I don't think it'll help with the following:

let a: Integer = 0
let b: Integer = 10
var range: InclusiveRange<Integer> = InclusiveRange(a, b)

Here on both the sides, we have InclusiveRange<Integer>.

---

What we need is the ability to specify an exclusive type bound. Something that doesn't seem to be commonly supported.

Scala does seem to have some workaround: https://stackoverflow.com/questions/48590195/in-scala-how-do-i-define-upper-type-bounds-that-are-exclusive-of-the-defined-cla

Even with support for exclusive type bound, we would still need to disallow InclusiveRange<SignedInteger> as SignedInteger would be a subtype of Integer.

---

I believe a solution might be to just disallow creation of InclusiveRange<Integer> in the Instantiate function.

cadence/runtime/sema/type.go

Lines 5402 to 5407 in 7ab492f

	func (t *InclusiveRangeType) Instantiate(typeArguments []Type, report func(err error)) Type {
	memberType := typeArguments[0]
	return &InclusiveRangeType{
	MemberType: memberType,
	}
	}

Something like below

if memberType == IntegerType || memberType == SignedIntegerType {
	report(&InvalidTypeArgumentError{})
}

[SupunS]

Sorry, I missed your last suggestion.

I like the last solution. i.e:

I believe a solution might be to just disallow creation of InclusiveRange in the Instantiate function.

I think this requirement exists (at least currently) only for the InclusiveRangeType type. So it is sufficient to reject/ add validation only for that type.
Also, the suggested change is quite simple, and would unblock this feature 👌