From 48a20b4aa09568dd4c14e8440de6548d5a8b38ad Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sat, 20 Jun 2026 16:48:19 +0200 Subject: [PATCH] tests: add tests for variance inference and subtyping --- midas/checker/types.py | 10 +- tests/cases/checker/07_variance.midas | 59 +++ tests/cases/checker/07_variance.py | 52 ++ tests/cases/checker/07_variance.py.ref.json | 512 ++++++++++++++++++++ 4 files changed, 628 insertions(+), 5 deletions(-) create mode 100644 tests/cases/checker/07_variance.midas create mode 100644 tests/cases/checker/07_variance.py create mode 100644 tests/cases/checker/07_variance.py.ref.json diff --git a/midas/checker/types.py b/midas/checker/types.py index 7b7a6d6..60fb9c7 100644 --- a/midas/checker/types.py +++ b/midas/checker/types.py @@ -1,7 +1,7 @@ from __future__ import annotations from dataclasses import dataclass, field -from enum import Enum, auto +from enum import StrEnum from typing import Optional, assert_never import midas.ast.midas as m @@ -103,10 +103,10 @@ class ExtensionType: return f"{self.base} & {self.extension}" -class Variance(Enum): - INVARIANT = auto() - COVARIANT = auto() - CONTRAVARIANT = auto() +class Variance(StrEnum): + INVARIANT = "INVARIANT" + COVARIANT = "COVARIANT" + CONTRAVARIANT = "CONTRAVARIANT" @dataclass(frozen=True, kw_only=True) diff --git a/tests/cases/checker/07_variance.midas b/tests/cases/checker/07_variance.midas new file mode 100644 index 0000000..c117390 --- /dev/null +++ b/tests/cases/checker/07_variance.midas @@ -0,0 +1,59 @@ +// T is invariant (unused) +type Unused[T] = object + +// T is covariant +type Covariant[T] = object + +// T is contravariant +type Contravariant[T] = object + +// T is invariant +type Invariant[T] = object + +extend Covariant[T] { + def foo: fn() -> T +} + +extend Contravariant[T] { + def foo: fn(T, /) -> None +} + +extend Invariant[T] { + def foo: fn(T, /) -> T +} + +// T is covariant +type Coco[T] = object +extend Coco[T] { + def foo: fn() -> Covariant[T] +} + +// T is contravariant +type Cocontra[T] = object +extend Cocontra[T] { + def foo: fn() -> Contravariant[T] +} + +// T is contravariant +type Contraco[T] = object +extend Contraco[T] { + def foo: fn(Covariant[T], /) -> None +} + +// T is covariant +type Contracontra[T] = object +extend Contracontra[T] { + def foo: fn(Contravariant[T], /) -> None +} + + +type T1[T] = object +type T2[T] = object + +extend T1[T] { + def foo: fn() -> T2[T] +} + +extend T2[T] { + def foo: fn() -> T1[T] +} diff --git a/tests/cases/checker/07_variance.py b/tests/cases/checker/07_variance.py new file mode 100644 index 0000000..9b251da --- /dev/null +++ b/tests/cases/checker/07_variance.py @@ -0,0 +1,52 @@ +from _ import ( + T1, + T2, + Coco, + Cocontra, + Contraco, + Contracontra, + Contravariant, + Covariant, + Invariant, + Unused, +) + +unused: Unused +covariant: Covariant +contravariant: Contravariant +invariant: Invariant +coco: Coco +cocontra: Cocontra +contraco: Contraco +contracontra: Contracontra +t1: T1 +t2: T2 + +# Dummy print to prudce judgements for the expressions +print( + unused, + covariant, + contravariant, + invariant, + coco, + cocontra, + contraco, + contracontra, + t1, + t2, +) + +cov1: Covariant[float] +cov2: Covariant[int] +cov1 = cov2 # Ok because int <: float => Covariant[int] <: Covariant[float] +cov2 = cov1 # Invalid + +contra1: Contravariant[float] +contra2: Contravariant[int] +contra1 = contra2 # Invalid +contra2 = contra1 # Ok because int <: float => Covariant[float] <: Covariant[int] + +inv1: Invariant[float] +inv2: Invariant[int] +inv1 = inv2 # Invalid +inv2 = inv1 # Invalid diff --git a/tests/cases/checker/07_variance.py.ref.json b/tests/cases/checker/07_variance.py.ref.json new file mode 100644 index 0000000..a43b957 --- /dev/null +++ b/tests/cases/checker/07_variance.py.ref.json @@ -0,0 +1,512 @@ +{ + "diagnostics": [ + { + "type": "Error", + "location": { + "start": [ + 28, + 4 + ], + "end": [ + 28, + 13 + ] + }, + "message": "Too many positional arguments" + }, + { + "type": "Error", + "location": { + "start": [ + 42, + 0 + ], + "end": [ + 42, + 11 + ] + }, + "message": "Cannot assign Covariant[float] to variable 'cov2' of type Covariant[int]" + }, + { + "type": "Error", + "location": { + "start": [ + 46, + 0 + ], + "end": [ + 46, + 17 + ] + }, + "message": "Cannot assign Contravariant[int] to variable 'contra1' of type Contravariant[float]" + }, + { + "type": "Error", + "location": { + "start": [ + 51, + 0 + ], + "end": [ + 51, + 11 + ] + }, + "message": "Cannot assign Invariant[int] to variable 'inv1' of type Invariant[float]" + }, + { + "type": "Error", + "location": { + "start": [ + 52, + 0 + ], + "end": [ + 52, + 11 + ] + }, + "message": "Cannot assign Invariant[float] to variable 'inv2' of type Invariant[int]" + } + ], + "judgments": [ + { + "location": { + "from": "L26:0", + "to": "L26:5" + }, + "expr": { + "_type": "VariableExpr", + "name": "print" + }, + "type": { + "pos_args": [ + { + "pos": 0, + "name": "object", + "type": {}, + "required": true + } + ], + "args": [], + "kw_args": [], + "returns": {} + } + }, + { + "location": { + "from": "L27:4", + "to": "L27:10" + }, + "expr": { + "_type": "VariableExpr", + "name": "unused" + }, + "type": { + "name": "Unused", + "params": [ + { + "name": "T", + "bound": null, + "variance": "INVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L28:4", + "to": "L28:13" + }, + "expr": { + "_type": "VariableExpr", + "name": "covariant" + }, + "type": { + "name": "Covariant", + "params": [ + { + "name": "T", + "bound": null, + "variance": "COVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L29:4", + "to": "L29:17" + }, + "expr": { + "_type": "VariableExpr", + "name": "contravariant" + }, + "type": { + "name": "Contravariant", + "params": [ + { + "name": "T", + "bound": null, + "variance": "CONTRAVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L30:4", + "to": "L30:13" + }, + "expr": { + "_type": "VariableExpr", + "name": "invariant" + }, + "type": { + "name": "Invariant", + "params": [ + { + "name": "T", + "bound": null, + "variance": "INVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L31:4", + "to": "L31:8" + }, + "expr": { + "_type": "VariableExpr", + "name": "coco" + }, + "type": { + "name": "Coco", + "params": [ + { + "name": "T", + "bound": null, + "variance": "COVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L32:4", + "to": "L32:12" + }, + "expr": { + "_type": "VariableExpr", + "name": "cocontra" + }, + "type": { + "name": "Cocontra", + "params": [ + { + "name": "T", + "bound": null, + "variance": "CONTRAVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L33:4", + "to": "L33:12" + }, + "expr": { + "_type": "VariableExpr", + "name": "contraco" + }, + "type": { + "name": "Contraco", + "params": [ + { + "name": "T", + "bound": null, + "variance": "CONTRAVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L34:4", + "to": "L34:16" + }, + "expr": { + "_type": "VariableExpr", + "name": "contracontra" + }, + "type": { + "name": "Contracontra", + "params": [ + { + "name": "T", + "bound": null, + "variance": "COVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L35:4", + "to": "L35:6" + }, + "expr": { + "_type": "VariableExpr", + "name": "t1" + }, + "type": { + "name": "T1", + "params": [ + { + "name": "T", + "bound": null, + "variance": "INVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L36:4", + "to": "L36:6" + }, + "expr": { + "_type": "VariableExpr", + "name": "t2" + }, + "type": { + "name": "T2", + "params": [ + { + "name": "T", + "bound": null, + "variance": "INVARIANT" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L26:0", + "to": "L37:1" + }, + "expr": { + "_type": "CallExpr", + "callee": { + "_type": "VariableExpr", + "name": "print" + }, + "arguments": [ + { + "_type": "VariableExpr", + "name": "unused" + }, + { + "_type": "VariableExpr", + "name": "covariant" + }, + { + "_type": "VariableExpr", + "name": "contravariant" + }, + { + "_type": "VariableExpr", + "name": "invariant" + }, + { + "_type": "VariableExpr", + "name": "coco" + }, + { + "_type": "VariableExpr", + "name": "cocontra" + }, + { + "_type": "VariableExpr", + "name": "contraco" + }, + { + "_type": "VariableExpr", + "name": "contracontra" + }, + { + "_type": "VariableExpr", + "name": "t1" + }, + { + "_type": "VariableExpr", + "name": "t2" + } + ], + "keywords": {} + }, + "type": {} + }, + { + "location": { + "from": "L41:7", + "to": "L41:11" + }, + "expr": { + "_type": "VariableExpr", + "name": "cov2" + }, + "type": { + "name": "Covariant", + "args": [ + { + "name": "int" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L42:7", + "to": "L42:11" + }, + "expr": { + "_type": "VariableExpr", + "name": "cov1" + }, + "type": { + "name": "Covariant", + "args": [ + { + "name": "float" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L46:10", + "to": "L46:17" + }, + "expr": { + "_type": "VariableExpr", + "name": "contra2" + }, + "type": { + "name": "Contravariant", + "args": [ + { + "name": "int" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L47:10", + "to": "L47:17" + }, + "expr": { + "_type": "VariableExpr", + "name": "contra1" + }, + "type": { + "name": "Contravariant", + "args": [ + { + "name": "float" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L51:7", + "to": "L51:11" + }, + "expr": { + "_type": "VariableExpr", + "name": "inv2" + }, + "type": { + "name": "Invariant", + "args": [ + { + "name": "int" + } + ], + "body": { + "name": "object" + } + } + }, + { + "location": { + "from": "L52:7", + "to": "L52:11" + }, + "expr": { + "_type": "VariableExpr", + "name": "inv1" + }, + "type": { + "name": "Invariant", + "args": [ + { + "name": "float" + } + ], + "body": { + "name": "object" + } + } + } + ] +} \ No newline at end of file