Introduce type arg as distinct from type param

6 files changed, 65 insertions, 28 deletions

diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
index 5eabbdda..ca33cf0a 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeChecker.java
@@ -70,11 +70,22 @@ public class TypeChecker {
         TypeCheckerContext context,
         FunctionType receiverType
     ) {
+        var typeLevelArgs = receiverType.typeLevelParams()
+            .map(typeLevelParams ->
+                typeLevelParams.stream()
+                    .map(param -> new TypeArg(param))
+                    .toList()
+            );
+
         var constraints = TypeCheckerSubTyping.constraints(
-            receiverType.typeLevelParams().orElse(List.of()),
+            typeLevelArgs.orElseGet(List::of),
             context.toTypeInfos()
         );
 
+        if (receiverType.typeLevelParams().isPresent()) {
+            receiverType = receiverType.applyTypeLevelArgs(typeLevelArgs.get());
+        }
+
         if (args.positional().size() != receiverType.positionalParams().size()) {
             throw new WrongNumberOfPositionalArgsError(
                 receiverType.positionalParams().size(),
diff --git a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
index dd12d06b..b17758b3 100644
--- a/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
+++ b/src/main/java/org/shedlang/compiler/typechecker/TypeCheckerSubTyping.java
@@ -41,32 +41,32 @@ public class TypeCheckerSubTyping {
         }
     }
 
-    static Constraints constraints(List<TypeParam> typeLevelParams, TypeInfos typeInfos) {
-        return new Constraints(typeLevelParams, P.map(), typeInfos);
+    static Constraints constraints(List<TypeArg> typeLevelArgs, TypeInfos typeInfos) {
+        return new Constraints(typeLevelArgs, P.map(), typeInfos);
     }
 
     record Constraints(
-        // TODO: typeLevelParams are redundant if we make typeBounds always have those params as keys?
-        List<TypeParam> typeLevelParams,
-        PMap<TypeParam, TypeBounds> typeBounds,
+        // TODO: typeLevelArgs are redundant if we make typeBounds always have those as keys?
+        List<TypeArg> typeLevelArgs,
+        PMap<TypeArg, TypeBounds> typeBounds,
         TypeInfos typeInfos
     ) {
-        public Constraints addLowerBound(TypeParam typeParam, Type lowerBound) {
-            return updateBounds(typeParam, bounds -> bounds.addLowerBound(lowerBound));
+        public Constraints addLowerBound(TypeArg typeArg, Type lowerBound) {
+            return updateBounds(typeArg, bounds -> bounds.addLowerBound(lowerBound));
         }
 
-        public Constraints addUpperBound(TypeParam typeParam, Type upperBound) {
-            return updateBounds(typeParam, bounds -> bounds.addUpperBound(upperBound));
+        public Constraints addUpperBound(TypeArg typeArg, Type upperBound) {
+            return updateBounds(typeArg, bounds -> bounds.addUpperBound(upperBound));
         }
 
         private Constraints updateBounds(
-            TypeParam typeParam,
+            TypeArg typeArg,
             Function<TypeBounds, TypeBounds> update
         ) {
-            var bounds = update.apply(this.typeBounds.getOrDefault(typeParam, TypeBounds.EMPTY));
+            var bounds = update.apply(this.typeBounds.getOrDefault(typeArg, TypeBounds.EMPTY));
             return new Constraints(
-                this.typeLevelParams,
-                this.typeBounds.plus(typeParam, bounds),
+                this.typeLevelArgs,
+                this.typeBounds.plus(typeArg, bounds),
                 this.typeInfos
             );
         }
@@ -74,11 +74,10 @@ public class TypeCheckerSubTyping {
         public TypeSubstitutionMap solve(Source source) {
             // TODO: handle type params that are constrained by other type params
             // TODO: handle unconstrained types
-            // TODO: do we need any special handling for mutual recursion (i.e. do we need separate type params for the parent call and the child call?)
 
-            var map = this.typeLevelParams.stream()
-                .map(typeParam -> {
-                    var typeParamBounds = this.typeBounds.getOrDefault(typeParam, TypeBounds.EMPTY);
+            var map = this.typeLevelArgs.stream()
+                .map(typeArg -> {
+                    var typeParamBounds = this.typeBounds.getOrDefault(typeArg, TypeBounds.EMPTY);
 
                     var lowerBound = Types.BOTTOM;
                     for (var lower : typeParamBounds.lower) {
@@ -99,7 +98,7 @@ public class TypeCheckerSubTyping {
                         ? upperBound
                         : lowerBound;
 
-                    return Map.entry(typeParam, inferredType);
+                    return Map.entry(typeArg.param(), inferredType);
                 })
                 .collect(Collectors.toMap(x -> x.getKey(), x -> x.getValue()));
 
@@ -143,19 +142,19 @@ public class TypeCheckerSubTyping {
         }
 
         if (
-            supertype instanceof TypeParam supertypeTypeParam &&
-            constraints.typeLevelParams.contains(supertypeTypeParam)
+            supertype instanceof TypeArg supertypeTypeArg &&
+            constraints.typeLevelArgs.contains(supertypeTypeArg)
         ) {
-            constraints = constraints.addLowerBound(supertypeTypeParam, subtype);
+            constraints = constraints.addLowerBound(supertypeTypeArg, subtype);
 
             return Optional.of(constraints);
         }
 
         if (
-            subtype instanceof TypeParam subtypeTypeParam &&
-            constraints.typeLevelParams.contains(subtypeTypeParam)
+            subtype instanceof TypeArg subtypeTypeArg &&
+            constraints.typeLevelArgs.contains(subtypeTypeArg)
         ) {
-            constraints = constraints.addUpperBound(subtypeTypeParam, supertype);
+            constraints = constraints.addUpperBound(subtypeTypeArg, supertype);
 
             return Optional.of(constraints);
         }
diff --git a/src/main/java/org/shedlang/compiler/types/FunctionType.java b/src/main/java/org/shedlang/compiler/types/FunctionType.java
index aad68885..621a2364 100644
--- a/src/main/java/org/shedlang/compiler/types/FunctionType.java
+++ b/src/main/java/org/shedlang/compiler/types/FunctionType.java
@@ -55,8 +55,12 @@ public record FunctionType(
     }
 
     public FunctionType withTypeLevelParams(List<TypeParam> typeLevelParams) {
+        return withTypeLevelParams(Optional.of(typeLevelParams));
+    }
+
+    private FunctionType withTypeLevelParams(Optional<List<TypeParam>> typeLevelParams) {
         return new FunctionType(
-            Optional.of(typeLevelParams),
+            typeLevelParams,
             this.positionalParams,
             this.namedParams,
             this.effect,
@@ -74,6 +78,18 @@ public record FunctionType(
         );
     }
 
+    public FunctionType applyTypeLevelArgs(List<TypeArg> typeArgs) {
+        var typeSubstitutionMap = TypeSubstitutionMap.from(
+            this.typeLevelParams.orElseThrow(),
+            typeArgs
+        );
+
+        return TypeSubstitution.substituteFunctionType(
+            this.withTypeLevelParams(Optional.empty()),
+            typeSubstitutionMap
+        );
+    }
+
     public static Builder builder() {
         return new Builder(
             Optional.empty(),
diff --git a/src/main/java/org/shedlang/compiler/types/Type.java b/src/main/java/org/shedlang/compiler/types/Type.java
index a2701446..d2607906 100644
--- a/src/main/java/org/shedlang/compiler/types/Type.java
+++ b/src/main/java/org/shedlang/compiler/types/Type.java
@@ -6,5 +6,5 @@ package org.shedlang.compiler.types;
  * found through auxiliary data.
  */
 public sealed interface Type extends TypeLevelValue
-    permits BoolType, BottomType, ConstructedType, ConstructibleType, FunctionType, IntType, NamespaceType, StringType, StructType, SumType, TopType, TupleType, TypeLevelValueType, TypeParam, UnitType {
+    permits BoolType, BottomType, ConstructedType, ConstructibleType, FunctionType, IntType, NamespaceType, StringType, StructType, SumType, TopType, TupleType, TypeArg, TypeLevelValueType, TypeParam, UnitType {
 }
diff --git a/src/main/java/org/shedlang/compiler/types/TypeArg.java b/src/main/java/org/shedlang/compiler/types/TypeArg.java
new file mode 100644
index 00000000..cbf80b3d
--- /dev/null
+++ b/src/main/java/org/shedlang/compiler/types/TypeArg.java
@@ -0,0 +1,8 @@
+package org.shedlang.compiler.types;
+
+public record TypeArg(TypeParam param) implements Type {
+    @Override
+    public String describe() {
+        return param.name();
+    }
+}
diff --git a/src/main/java/org/shedlang/compiler/types/TypeSubstitution.java b/src/main/java/org/shedlang/compiler/types/TypeSubstitution.java
index b0632b6c..cc7ddbc9 100644
--- a/src/main/java/org/shedlang/compiler/types/TypeSubstitution.java
+++ b/src/main/java/org/shedlang/compiler/types/TypeSubstitution.java
@@ -49,6 +49,9 @@ public class TypeSubstitution {
                         .toList()
                 );
 
+            case TypeArg typeArg ->
+                typeArg;
+
             case TypeLevelValueType typeLevelValueType -> {
                 throw new UnsupportedOperationException("TODO");
             }
@@ -99,7 +102,7 @@ public class TypeSubstitution {
         );
     }
 
-    private static FunctionType substituteFunctionType(
+    public static FunctionType substituteFunctionType(
         FunctionType functionType,
         TypeSubstitutionMap map
     ) {