From 3ff9c7c74c904dc3ff71040be3df206c9d67d33a Mon Sep 17 00:00:00 2001
From: Michael Williamson <mike@zwobble.org>
Date: Sat, 30 Sep 2023 18:12:54 +0100
Subject: Add subtyping for sum types

---
 .../org/shedlang/compiler/typechecker/TypeChecker.java |  1 +
 .../compiler/typechecker/TypeCheckerContext.java       | 10 ++++++----
 .../compiler/typechecker/TypeCheckerSubTyping.java     |  8 ++++++++
 .../typechecker/errors/MissingSumTypeInfoError.java    | 18 ++++++++++++++++++
 4 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 src/main/java/org/shedlang/compiler/typechecker/errors/MissingSumTypeInfoError.java

(limited to 'src/main/java')

diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
index c9413be8..d10531ad 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
@@ -928,6 +928,7 @@ public class TypeChecker {
             public TypeCheckerContext defineTypes(TypeCheckerContext context) {
                 var type = context.getLexicalState(SumType.class, untyped.name());
 
+                // TODO: restrict variants to structs. Do we allow other sum types?
                 var variants = untyped.variants().stream()
                     .map(untypedVariant -> typeCheckTypeLevelExpression(
                         TypeSets.META_TYPE,
diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerContext.java b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerContext.java
index 348380cb..7d1f77cc 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerContext.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerContext.java
@@ -5,10 +5,7 @@ import org.pcollections.PMap;
 import org.pcollections.PStack;
 import org.shedlang.compiler.ast.typed.FreeVariables;
 import org.shedlang.compiler.sources.Source;
-import org.shedlang.compiler.typechecker.errors.CannotDefineVariableDeclaredInOuterScopeError;
-import org.shedlang.compiler.typechecker.errors.MissingStructTypeInfoError;
-import org.shedlang.compiler.typechecker.errors.UnknownVariableError;
-import org.shedlang.compiler.typechecker.errors.VariableIsAlreadyDefinedError;
+import org.shedlang.compiler.typechecker.errors.*;
 import org.shedlang.compiler.types.*;
 import org.shedlang.compiler.util.P;
 import org.shedlang.compiler.util.PCollectors;
@@ -362,6 +359,11 @@ public class TypeCheckerContext {
         );
     }
 
+    public SumTypeInfo sumTypeInfo(SumType type, Source source) {
+        return this.typeInfos.sumTypeInfo(type)
+            .orElseThrow(() -> new MissingSumTypeInfoError(type, source));
+    }
+
     public <T> TypeCheckerResult<T> toResult(T value) {
         return new TypeCheckerResult<>(value, this);
     }
diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
index b73011ce..e0d6fe78 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
@@ -1,5 +1,7 @@
 package org.shedlang.compiler.typechecker;
 
+import org.shedlang.compiler.sources.Sources;
+import org.shedlang.compiler.types.SumType;
 import org.shedlang.compiler.types.Type;
 import org.shedlang.compiler.types.Types;
 
@@ -20,6 +22,12 @@ public class TypeCheckerSubTyping {
             return true;
         }
 
+        if (superType instanceof SumType superTypeSum) {
+            var superTypeInfo = context.sumTypeInfo(superTypeSum, Sources.NULL);
+            return superTypeInfo.variants().stream()
+                .anyMatch(superTypeVariant -> isSubType(subType, superTypeVariant, context));
+        }
+
         return false;
     }
 }
diff --git a/src/main/java/org/shedlang/compiler/typechecker/errors/MissingSumTypeInfoError.java b/src/main/java/org/shedlang/compiler/typechecker/errors/MissingSumTypeInfoError.java
new file mode 100644
index 00000000..04eb6c6a
--- /dev/null
+++ b/src/main/java/org/shedlang/compiler/typechecker/errors/MissingSumTypeInfoError.java
@@ -0,0 +1,18 @@
+package org.shedlang.compiler.typechecker.errors;
+
+import org.shedlang.compiler.errors.InternalCompilerError;
+import org.shedlang.compiler.sources.Source;
+import org.shedlang.compiler.types.SumType;
+
+public class MissingSumTypeInfoError extends InternalCompilerError {
+    private final SumType type;
+
+    public MissingSumTypeInfoError(SumType type, Source source) {
+        super("Missing type info for sum type " + type, source);
+        this.type = type;
+    }
+
+    public SumType type() {
+        return type;
+    }
+}
-- 
cgit v1.2.3