Check type of type-level value

5 files changed, 38 insertions, 17 deletions

diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
index 8bb6ca23..f03de967 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
@@ -4,6 +4,7 @@ import org.shedlang.compiler.ast.typed.*;
 import org.shedlang.compiler.ast.untyped.*;
 import org.shedlang.compiler.sources.Source;
 import org.shedlang.compiler.typechecker.errors.*;
+import org.shedlang.compiler.typechecker.typesets.TypeSetTypeLevelValue;
 import org.shedlang.compiler.typechecker.typesets.TypeSets;
 import org.shedlang.compiler.types.FunctionType;
 import org.shedlang.compiler.types.Type;
@@ -167,7 +168,7 @@ public class TypeChecker {
         UntypedFunctionDefinitionNode untyped,
         TypeCheckerContext context
     ) {
-        var typedReturnType = typeCheckTypeLevelExpression(Type.class, untyped.returnType(), context);
+        var typedReturnType = typeCheckTypeLevelExpression(TypeSets.META_TYPE, untyped.returnType(), context);
 
         return new TypedFunctionDefinitionNode(
             untyped.name(),
@@ -231,32 +232,34 @@ public class TypeChecker {
     }
 
     static <T extends TypeLevelValue> TypedTypeLevelExpressionNode<T> typeCheckTypeLevelExpression(
-        Class<T> valueClass,
+        TypeSetTypeLevelValue<T> valueType,
         UntypedTypeLevelExpressionNode untyped,
         TypeCheckerContext context
     ) {
         return switch (untyped) {
             case UntypedTypeLevelReferenceNode reference ->
-                typeCheckTypeLevelReference(valueClass, reference, context);
+                typeCheckTypeLevelReference(valueType, reference, context);
         };
     }
 
     private static <T extends TypeLevelValue> TypedTypeLevelExpressionNode<T> typeCheckTypeLevelReference(
-        Class<T> valueClass,
+        TypeSetTypeLevelValue<T> valueType,
         UntypedTypeLevelReferenceNode untyped,
         TypeCheckerContext context
     ) {
         var type = lookupVariable(untyped.name(), untyped.source(), context);
 
         if (!(type instanceof TypeLevelValueType typeLevelValueType)) {
-            throw new UnexpectedTypeError(TypeSets.TYPE_LEVEL_VALUE, type, untyped.source());
+            throw new UnexpectedTypeError(valueType, type, untyped.source());
         }
 
-        // TODO: check instance and raise proper error
+        if (!valueType.valueClass().isInstance(typeLevelValueType.value())) {
+            throw new UnexpectedTypeError(valueType, type, untyped.source());
+        }
 
         return new TypedTypeLevelReferenceNode<>(
             untyped.name(),
-            (T)typeLevelValueType.value(),
+            valueType.valueClass().cast(typeLevelValueType.value()),
             untyped.source()
         );
     }
diff --git a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetMetaType.java b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetMetaType.java
new file mode 100644
index 00000000..095c5c82
--- /dev/null
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetMetaType.java
@@ -0,0 +1,20 @@
+package org.shedlang.compiler.typechecker.typesets;
+
+import org.shedlang.compiler.types.Type;
+
+public final class TypeSetMetaType implements TypeSetTypeLevelValue<Type> {
+    private TypeSetMetaType() {
+    }
+
+    static final TypeSetMetaType INSTANCE = new TypeSetMetaType();
+
+    @Override
+    public String describe() {
+        return "metatype";
+    }
+
+    @Override
+    public Class<Type> valueClass() {
+        return Type.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 791ec37a..c4389aee 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSetTypeLevelValue.java
@@ -1,13 +1,7 @@
 package org.shedlang.compiler.typechecker.typesets;
 
-public final class TypeSetTypeLevelValue implements TypeSet {
-    private TypeSetTypeLevelValue() {
-    }
+import org.shedlang.compiler.types.TypeLevelValue;
 
-    static final TypeSetTypeLevelValue INSTANCE = new TypeSetTypeLevelValue();
-
-    @Override
-    public String describe() {
-        return "type-level value";
-    }
+public sealed interface TypeSetTypeLevelValue<T extends TypeLevelValue> extends TypeSet permits TypeSetMetaType {
+    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 6bb13f7a..633bff86 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/typesets/TypeSets.java
@@ -7,7 +7,7 @@ public class TypeSets {
     }
 
     public static final TypeSet FUNCTION = TypeSetFunction.INSTANCE;
-    public static final TypeSet TYPE_LEVEL_VALUE = TypeSetTypeLevelValue.INSTANCE;
+    public static final TypeSetMetaType META_TYPE = TypeSetMetaType.INSTANCE;
 
     public static TypeSet type(Type type) {
         return new TypeSetType(type);
diff --git a/src/main/java/org/shedlang/compiler/types/Types.java b/src/main/java/org/shedlang/compiler/types/Types.java
index cb734272..ad9d0547 100644
--- a/src/main/java/org/shedlang/compiler/types/Types.java
+++ b/src/main/java/org/shedlang/compiler/types/Types.java
@@ -12,4 +12,8 @@ public class Types {
     public static Type metaType(Type type) {
         return new TypeLevelValueType(type);
     }
+
+    public static Type effectType(Effect effect) {
+        return new TypeLevelValueType(effect);
+    }
 }