From c4498af1d2fb1f9456d16a39daba9e841d3537b9 Mon Sep 17 00:00:00 2001
From: Michael Williamson <mike@zwobble.org>
Date: Sat, 23 Dec 2023 23:12:57 +0000
Subject: Add basic type checking for constructed types

---
 .../ast/typed/TypedConstructedTypeNode.java        | 10 +++++++
 .../shedlang/compiler/typechecker/TypeChecker.java | 33 ++++++++++++++++++++--
 .../typesets/TypeSetTypeConstructor.java           | 20 +++++++++++++
 .../typesets/TypeSetTypeLevelValue.java            |  2 +-
 .../compiler/typechecker/typesets/TypeSets.java    |  1 +
 .../java/org/shedlang/compiler/types/Types.java    |  7 +++++
 6 files changed, 69 insertions(+), 4 deletions(-)
 create mode 100644 src/main/java/org/shedlang/compiler/ast/typed/TypedConstructedTypeNode.java
 create mode 100644 src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeConstructor.java

(limited to 'src/main/java')

diff --git a/src/main/java/org/shedlang/compiler/ast/typed/TypedConstructedTypeNode.java b/src/main/java/org/shedlang/compiler/ast/typed/TypedConstructedTypeNode.java
new file mode 100644
index 00000000..e8c45011
--- /dev/null
+++ b/src/main/java/org/shedlang/compiler/ast/typed/TypedConstructedTypeNode.java
@@ -0,0 +1,10 @@
+package org.shedlang.compiler.ast.typed;
+
+import org.shedlang.compiler.sources.Source;
+import org.shedlang.compiler.types.ConstructedType;
+
+public record TypedConstructedTypeNode(
+    ConstructedType<?> value,
+    Source source
+) implements TypedTypeLevelExpressionNode<ConstructedType<?>> {
+}
diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
index 668a005c..c9d4f811 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
@@ -1554,7 +1554,14 @@ public class TypeChecker {
         };
     }
 
-    private static TypedTypeLevelExpressionNode<Type> typeCheckTypeExpression(
+    static TypeConstructor<?> typeCheckTypeConstructor(
+        UntypedTypeLevelExpressionNode untyped,
+        TypeCheckerContext context
+    ) {
+        return typeCheckTypeLevelExpression(TypeSets.TYPE_CONSTRUCTOR, untyped, context).value();
+    }
+
+    static TypedTypeLevelExpressionNode<Type> typeCheckTypeExpression(
         UntypedTypeLevelExpressionNode untyped,
         TypeCheckerContext context
     ) {
@@ -1568,8 +1575,28 @@ public class TypeChecker {
         TypeCheckerContext context
     ) {
         return switch (untyped) {
-            case UntypedConstructedTypeNode constructedType ->
-                throw new UnsupportedOperationException("TODO");
+            case UntypedConstructedTypeNode constructedTypeNode -> {
+                // TODO: check number of args
+                var constructor = typeCheckTypeConstructor(constructedTypeNode.receiver(), context);
+                var args = constructedTypeNode.args().stream()
+                    .map(arg -> typeCheckTypeExpression(arg, context).value())
+                    .toList();
+                var constructedType = new ConstructedType<>(constructor, args);
+
+                // TODO: tidy this (and other similar checks in this function) up
+                if (valueType.valueClass().equals(Type.class)) {
+                    yield (TypedTypeLevelExpressionNode<T>) new TypedConstructedTypeNode(
+                        constructedType,
+                        constructedTypeNode.source()
+                    );
+                } else {
+                    throw new UnexpectedTypeError(
+                        valueType,
+                        Types.metaType(constructedType),
+                        untyped.source()
+                    );
+                }
+            }
 
             case UntypedFunctionTypeNode functionType -> {
                 var typedFunctionTypeNode = typeCheckFunctionType(functionType, context);
diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeConstructor.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeConstructor.java
new file mode 100644
index 00000000..4a5f5ad3
--- /dev/null
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeConstructor.java
@@ -0,0 +1,20 @@
+package org.shedlang.compiler.typechecker.typesets;
+
+import org.shedlang.compiler.types.TypeConstructor;
+
+public final class TypeSetTypeConstructor implements TypeSetTypeLevelValue<TypeConstructor> {
+    private TypeSetTypeConstructor() {
+    }
+
+    static final TypeSetTypeConstructor INSTANCE = new TypeSetTypeConstructor();
+
+    @Override
+    public String describe() {
+        return "type constructor";
+    }
+
+    @Override
+    public Class<TypeConstructor> valueClass() {
+        return TypeConstructor.class;
+    }
+}
diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java
index a0a6d43a..9159a2d5 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java
@@ -2,6 +2,6 @@ package org.shedlang.compiler.typechecker.typesets;
 
 import org.shedlang.compiler.types.TypeLevelValue;
 
-public sealed interface TypeSetTypeLevelValue<T extends TypeLevelValue> extends TypeSet permits TypeSetEffect, TypeSetMetaType, TypeSetStructMetaType, TypeSetUserDefinedEffect {
+public sealed interface TypeSetTypeLevelValue<T extends TypeLevelValue> extends TypeSet permits TypeSetEffect, TypeSetMetaType, TypeSetStructMetaType, TypeSetTypeConstructor, TypeSetUserDefinedEffect {
     Class<T> valueClass();
 }
diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java
index 57002c37..89c00898 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java
@@ -11,6 +11,7 @@ public class TypeSets {
     public static final TypeSetMetaType META_TYPE = TypeSetMetaType.INSTANCE;
     public static final TypeSetStructMetaType STRUCT_META_TYPE = TypeSetStructMetaType.INSTANCE;
     public static final TypeSetTuple TUPLE = TypeSetTuple.INSTANCE;
+    public static final TypeSetTypeConstructor TYPE_CONSTRUCTOR = TypeSetTypeConstructor.INSTANCE;
     public static final TypeSetUserDefinedEffect USER_DEFINED_EFFECT = TypeSetUserDefinedEffect.INSTANCE;
 
     public static TypeSet type(Type type) {
diff --git a/src/main/java/org/shedlang/compiler/types/Types.java b/src/main/java/org/shedlang/compiler/types/Types.java
index 76c02f07..c3c25853 100644
--- a/src/main/java/org/shedlang/compiler/types/Types.java
+++ b/src/main/java/org/shedlang/compiler/types/Types.java
@@ -42,6 +42,13 @@ public class Types {
         return new TypeLevelValueType(typeConstructor);
     }
 
+    public static <T extends StructuredType> TypeConstructor<T> typeConstructor(
+        List<TypeParam> params,
+        T genericType
+    ) {
+        return new TypeConstructor<>(params, genericType);
+    }
+
     public static Type commonSupertype(List<Type> subtypes) {
         var uniqueSubtypes = subtypes.stream()
             .filter(subtype -> subtype != Types.BOTTOM)
-- 
cgit v1.2.3