From 01bd9f9bdfa3d6257d5fd0177c769b30de8f4930 Mon Sep 17 00:00:00 2001
From: Michael Williamson <mike@zwobble.org>
Date: Sat, 10 Jun 2023 14:40:55 +0100
Subject: Encode what type-level value type-level expressions hold

---
 .../shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java  | 4 ++--
 .../shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java   | 6 +++---
 src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java   | 7 ++++---
 3 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'src/main/java')

diff --git a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java
index 4b10483d..469f0bcf 100644
--- a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java
+++ b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelExpressionNode.java
@@ -2,6 +2,6 @@ package org.shedlang.compiler.ast.typed;
 
 import org.shedlang.compiler.types.TypeLevelValue;
 
-public interface TypedTypeLevelExpressionNode extends TypedNode {
-    TypeLevelValue value();
+public interface TypedTypeLevelExpressionNode<T extends TypeLevelValue> extends TypedNode {
+    T value();
 }
diff --git a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java
index 009d0b8b..050061a6 100644
--- a/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java
+++ b/src/main/java/org/shedlang/compiler/ast/typed/TypedTypeLevelReferenceNode.java
@@ -3,9 +3,9 @@ package org.shedlang.compiler.ast.typed;
 import org.shedlang.compiler.sources.Source;
 import org.shedlang.compiler.types.TypeLevelValue;
 
-public record TypedTypeLevelReferenceNode(
+public record TypedTypeLevelReferenceNode<T extends TypeLevelValue>(
     String name,
-    TypeLevelValue value,
+    T value,
     Source source
-) implements TypedTypeLevelExpressionNode {
+) implements TypedTypeLevelExpressionNode<T> {
 }
diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
index f2af9769..63699416 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
@@ -7,6 +7,7 @@ import org.shedlang.compiler.typechecker.errors.*;
 import org.shedlang.compiler.typechecker.typesets.TypeSets;
 import org.shedlang.compiler.types.FunctionType;
 import org.shedlang.compiler.types.Type;
+import org.shedlang.compiler.types.TypeLevelValue;
 import org.shedlang.compiler.types.TypeLevelValueType;
 
 import java.util.HashSet;
@@ -201,7 +202,7 @@ public class TypeChecker {
         );
     }
 
-    static TypedTypeLevelExpressionNode typeCheckTypeLevelExpression(
+    static TypedTypeLevelExpressionNode<TypeLevelValue> typeCheckTypeLevelExpression(
         UntypedTypeLevelExpressionNode untyped,
         TypeCheckerContext context
     ) {
@@ -211,7 +212,7 @@ public class TypeChecker {
         };
     }
 
-    private static TypedTypeLevelExpressionNode typeCheckTypeLevelReference(
+    private static TypedTypeLevelExpressionNode<TypeLevelValue> typeCheckTypeLevelReference(
         UntypedTypeLevelReferenceNode untyped,
         TypeCheckerContext context
     ) {
@@ -221,7 +222,7 @@ public class TypeChecker {
             throw new UnexpectedTypeError(TypeSets.TYPE_LEVEL_VALUE, type, untyped.source());
         }
 
-        return new TypedTypeLevelReferenceNode(
+        return new TypedTypeLevelReferenceNode<>(
             untyped.name(),
             typeLevelValueType.value(),
             untyped.source()
-- 
cgit v1.2.3