diff --git a/core/src/main/java/com/garciat/typeclasses/TypeClasses.java b/core/src/main/java/com/garciat/typeclasses/TypeClasses.java
index fd4894f..c0da10e 100644
--- a/core/src/main/java/com/garciat/typeclasses/TypeClasses.java
+++ b/core/src/main/java/com/garciat/typeclasses/TypeClasses.java
@@ -1,32 +1,65 @@
 package com.garciat.typeclasses;
 
+import com.garciat.typeclasses.api.Lazy;
 import com.garciat.typeclasses.api.Ty;
 import com.garciat.typeclasses.impl.Match;
+import com.garciat.typeclasses.impl.ParsedType;
+import com.garciat.typeclasses.impl.Resolution;
 import com.garciat.typeclasses.impl.utils.Either;
 import com.garciat.typeclasses.runtime.Runtime;
 import com.garciat.typeclasses.runtime.RuntimeWitnessSystem;
 import java.lang.reflect.InvocationTargetException;
-import java.util.List;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
 
 public final class TypeClasses {
   private TypeClasses() {}
 
   public static <T> T witness(Ty<T> ty) {
-    Object instance =
-        switch (RuntimeWitnessSystem.resolve(ty.type(), TypeClasses::invoke)) {
+    Resolution.Result<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim> methodTree =
+        switch (RuntimeWitnessSystem.resolve(ty.type())) {
           case Either.Right(var r) -> r;
           case Either.Left(var error) -> throw new WitnessResolutionException(error.format());
         };
 
+    Object instance = walk(new HashMap<>(), methodTree);
+
     @SuppressWarnings("unchecked")
     T typedInstance = (T) instance;
     return typedInstance;
   }
 
+  private static Object walk(
+      Map<ParsedType<Runtime.Var, Runtime.Const, Runtime.Prim>, Object> cache,
+      Resolution.Result<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim> tree) {
+    return switch (tree) {
+      case Resolution.Result.Node(var match, var dependencies) -> {
+        Object[] args = dependencies.stream().map(dep -> walk(cache, dep)).toArray();
+
+        Object instance = invoke(match, args);
+
+        cache.put(match.witnessType(), instance);
+
+        yield instance;
+      }
+      case Resolution.Result.LazyLookup(var target) ->
+          (Lazy<Object>)
+              () ->
+                  Optional.ofNullable(cache.get(target))
+                      .orElseThrow(
+                          () ->
+                              new WitnessResolutionException(
+                                  "BUG: expected cached instance for %s"
+                                      .formatted(target.format())));
+      case Resolution.Result.LazyWrap(var under) -> (Lazy<Object>) () -> walk(cache, under);
+    };
+  }
+
   private static Object invoke(
-      Match<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim> match, List<Object> args) {
+      Match<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim> match, Object[] args) {
     try {
-      return match.ctor().method().java().invoke(null, args.toArray());
+      return match.ctor().method().java().invoke(null, args);
     } catch (IllegalAccessException e) {
       throw new IllegalStateException("BUG: expected witness constructor method to be public", e);
     } catch (InvocationTargetException e) {
diff --git a/core/src/main/java/com/garciat/typeclasses/api/Lazy.java b/core/src/main/java/com/garciat/typeclasses/api/Lazy.java
new file mode 100644
index 0000000..3f5dac2
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/api/Lazy.java
@@ -0,0 +1,5 @@
+package com.garciat.typeclasses.api;
+
+public interface Lazy<A> {
+  A get();
+}
diff --git a/core/src/main/java/com/garciat/typeclasses/api/Out.java b/core/src/main/java/com/garciat/typeclasses/api/Out.java
new file mode 100644
index 0000000..690b829
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/api/Out.java
@@ -0,0 +1,10 @@
+package com.garciat.typeclasses.api;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_PARAMETER})
+public @interface Out {}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/ParsedType.java b/core/src/main/java/com/garciat/typeclasses/impl/ParsedType.java
index 8e0dfe2..e1e755e 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/ParsedType.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/ParsedType.java
@@ -3,26 +3,42 @@
 import java.util.List;
 
 public sealed interface ParsedType<V, C, P> {
-  record Var<V, C, P>(V repr) implements ParsedType<V, C, P> {}
+  record Var<V, C, P>(TyParam<V> ref) implements ParsedType<V, C, P> {}
+
+  record Out<V, C, P>(ParsedType<V, C, P> under) implements ParsedType<V, C, P> {}
 
   record App<V, C, P>(ParsedType<V, C, P> fun, ParsedType<V, C, P> arg)
       implements ParsedType<V, C, P> {}
 
   record ArrayOf<V, C, P>(ParsedType<V, C, P> elementType) implements ParsedType<V, C, P> {}
 
-  record Const<V, C, P>(C repr, List<Var<V, C, P>> typeParams) implements ParsedType<V, C, P> {}
+  record Const<V, C, P>(C repr, List<TyParam<V>> typeParams) implements ParsedType<V, C, P> {}
 
   record Primitive<V, C, P>(P repr) implements ParsedType<V, C, P> {}
 
   record Wildcard<V, C, P>() implements ParsedType<V, C, P> {}
 
+  record Lazy<V, C, P>(ParsedType<V, C, P> under) implements ParsedType<V, C, P> {}
+
+  record TyParam<V>(V repr, boolean isOut) {
+    public <C, P> ParsedType<V, C, P> wrapOut(ParsedType<V, C, P> under) {
+      return isOut ? new Out<>(under) : under;
+    }
+
+    @Override
+    public String toString() {
+      return (isOut ? "&" : "") + repr;
+    }
+  }
+
   default String format() {
     return switch (this) {
       case Var(var repr) -> repr.toString();
+      case Out(var under) -> "Out<" + under.format() + ">";
       case Const(var repr, var typeParams) ->
           repr.toString()
               + typeParams.stream()
-                  .map(ParsedType::format)
+                  .map(TyParam::toString)
                   .reduce((a, b) -> a + ", " + b)
                   .map(s -> "[" + s + "]")
                   .orElse("");
@@ -30,6 +46,7 @@ case Const(var repr, var typeParams) ->
       case ArrayOf(var elem) -> elem.format() + "[]";
       case Primitive(var repr) -> repr.toString();
       case Wildcard() -> "?";
+      case Lazy(var repr) -> "Lazy<" + repr.format() + ">";
     };
   }
 }
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/Resolution.java b/core/src/main/java/com/garciat/typeclasses/impl/Resolution.java
index 6158b01..5839d15 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/Resolution.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/Resolution.java
@@ -1,59 +1,276 @@
 package com.garciat.typeclasses.impl;
 
+import static com.garciat.typeclasses.impl.utils.AutoCloseables.around;
+import static java.util.stream.Collectors.groupingBy;
+import static java.util.stream.Collectors.toUnmodifiableList;
+import static java.util.stream.Collectors.toUnmodifiableSet;
+
+import com.garciat.typeclasses.impl.ParsedType.Var;
 import com.garciat.typeclasses.impl.utils.Either;
 import com.garciat.typeclasses.impl.utils.Lists;
 import com.garciat.typeclasses.impl.utils.Maybe;
+import com.garciat.typeclasses.impl.utils.Sets;
 import com.garciat.typeclasses.impl.utils.ZeroOneMore;
+import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
-import java.util.function.BiFunction;
+import java.util.Map;
+import java.util.Set;
+import java.util.TreeMap;
 import java.util.function.Function;
 import java.util.stream.Collectors;
 
 public final class Resolution {
   private Resolution() {}
 
-  public static <M, V, C, P, R> Either<Failure<M, V, C, P>, R> resolve(
-      Function<ParsedType.Const<V, C, P>, List<WitnessConstructor<M, V, C, P>>> constructors,
-      BiFunction<Match<M, V, C, P>, List<R>, R> build,
+  public sealed interface Result<M, V, C, P> {
+    record Node<M, V, C, P>(Match<M, V, C, P> match, List<Result<M, V, C, P>> children)
+        implements Result<M, V, C, P> {}
+
+    record LazyLookup<M, V, C, P>(ParsedType<V, C, P> target) implements Result<M, V, C, P> {}
+
+    record LazyWrap<M, V, C, P>(Result<M, V, C, P> under) implements Result<M, V, C, P> {}
+  }
+
+  public static <M, V, C, P> Either<Failure<M, V, C, P>, Result<M, V, C, P>> resolve(
+      Function<C, List<WitnessConstructor<M, V, C, P>>> constructors, ParsedType<V, C, P> target) {
+    return resolveRec(new HashSet<>(), constructors, target);
+  }
+
+  private static <M, V, C, P> Either<Failure<M, V, C, P>, Result<M, V, C, P>> resolveRec(
+      Set<ParsedType<V, C, P>> seen,
+      Function<C, List<WitnessConstructor<M, V, C, P>>> constructors,
       ParsedType<V, C, P> target) {
-    var candidates =
-        OverlappingInstances.reduce(
-            Maybe.mapMaybe(findWitnesses(target, constructors), ctor -> match(ctor, target)));
+    if (target instanceof ParsedType.Lazy(var under)) {
+      if (seen.contains(under)) {
+        return Either.right(new Result.LazyLookup<>(under));
+      } else {
+        try (var _ = around(() -> seen.add(under), () -> seen.remove(under))) {
+          return resolveRec(seen, constructors, under).map(Result.LazyWrap::new);
+        }
+      }
+    }
+
+    var attempts =
+        Either.partition(
+            Lists.map(
+                Witnesses.findWitnesses(constructors, target),
+                ctor -> match(seen, constructors, ctor, target)));
+
+    var candidates = OverlappingInstances.reduce(attempts.snd());
 
     return switch (ZeroOneMore.of(candidates)) {
-      case ZeroOneMore.Zero() -> Either.left(new Failure.NotFound<>(target));
+      case ZeroOneMore.Zero() ->
+          Either.left(new Failure.NoMatch<>(target, attempts.fst(), attempts.snd()));
       case ZeroOneMore.More(var matches) -> Either.left(new Failure.Ambiguous<>(target, matches));
-      case ZeroOneMore.One(var c) ->
-          Either.traverse(c.dependencies(), t -> resolve(constructors, build, t))
-              .map(children -> build.apply(c, children))
+      case ZeroOneMore.One(var match) ->
+          Either.traverse(match.dependencies(), t -> resolveRec(seen, constructors, t))
+              .<Result<M, V, C, P>>map(children -> new Result.Node<>(match, children))
               .mapLeft(f -> new Failure.Nested<>(target, f));
     };
   }
 
-  private static <M, V, C, P> List<WitnessConstructor<M, V, C, P>> findWitnesses(
-      ParsedType<V, C, P> target,
-      Function<ParsedType.Const<V, C, P>, List<WitnessConstructor<M, V, C, P>>> constructors) {
-    return switch (target) {
-      case ParsedType.App(var fun, var arg) ->
-          Lists.concat(findWitnesses(fun, constructors), findWitnesses(arg, constructors));
-      case ParsedType.Const<V, C, P> c -> constructors.apply(c);
-      case ParsedType.Var(_),
-          ParsedType.ArrayOf(_),
-          ParsedType.Primitive(_),
-          ParsedType.Wildcard() ->
-          List.of();
+  private static <M, V, C, P> Either<MatchFailure<M, V, C, P>, Match<M, V, C, P>> match(
+      Set<ParsedType<V, C, P>> seen,
+      Function<C, List<WitnessConstructor<M, V, C, P>>> constructors,
+      WitnessConstructor<M, V, C, P> ctor,
+      ParsedType<V, C, P> target) {
+    return switch (Unification.unify(ctor.returnType(), target)) {
+      case Maybe.Nothing() -> Either.left(new MatchFailure.HeadMismatch<>(ctor));
+      case Maybe.Just(var returnSubst) -> {
+        List<ParsedType<V, C, P>> dependencies =
+            Unification.substituteAll(returnSubst, ctor.paramTypes());
+
+        TreeMap<Integer, List<Node<V, C, P>>> nodesByInDegree =
+            dependencies.stream()
+                .map(Resolution::parseNode)
+                .collect(groupingBy(n -> n.in().size(), TreeMap::new, toUnmodifiableList()));
+
+        if (!nodesByInDegree.isEmpty() && nodesByInDegree.firstKey() != 0) {
+          // There is a cycle in the dependency graph
+          yield Either.left(new MatchFailure.Cycle<>(ctor, dependencies));
+        }
+
+        Map<Var<V, C, P>, ParsedType<V, C, P>> substitution = new HashMap<>(returnSubst);
+
+        for (List<Node<V, C, P>> stratum : nodesByInDegree.sequencedValues()) {
+          for (Node<V, C, P> node : stratum) {
+            {
+              var missing = Sets.difference(node.in(), substitution.keySet());
+              if (!missing.isEmpty()) {
+                // Some input variable has not been satisfied yet
+                yield Either.left(new MatchFailure.UnboundVariables<>(ctor, missing));
+              }
+            }
+
+            switch (flatten(
+                resolveRec(
+                    seen, constructors, Unification.substitute(substitution, node.type())))) {
+              case Either.Right(Result.Node(var possible, _)) -> {
+                switch (Unification.unify(
+                    Types.unwrapOut1(node.type()), Types.unwrapOut1(possible.witnessType()))) {
+                  case Maybe.Just(var childSubst) -> {
+                    {
+                      var missing = Sets.difference(node.out(), childSubst.keySet());
+                      if (!missing.isEmpty()) {
+                        // Some output variable has not been satisfied
+                        yield Either.left(new MatchFailure.UnproductiveConstraint<>(ctor, missing));
+                      }
+                    }
+
+                    for (Var<V, C, P> out : childSubst.keySet()) {
+                      ParsedType<V, C, P> outT = childSubst.get(out);
+
+                      if (substitution.get(out) instanceof ParsedType<V, C, P> existingT
+                          && !existingT.equals(outT)) {
+                        // Conflicting substitutions
+                        yield Either.left(
+                            new MatchFailure.ConflictingSubstitution<>(ctor, out, existingT, outT));
+                      }
+
+                      substitution.put(out, outT);
+                    }
+                  }
+                  case Maybe.Nothing() -> {
+                    // Child witness does not match expected type
+                    yield Either.left(
+                        new MatchFailure.ResolvedConstraintMismatch<>(
+                            ctor,
+                            Types.unwrapOut1(node.type()),
+                            Types.unwrapOut1(possible.witnessType())));
+                  }
+                }
+              }
+              case Either.Right(Result.LazyWrap(_)) ->
+                  throw new IllegalStateException(
+                      "flatten should have eliminated LazyWrap cases here");
+              case Either.Right(Result.LazyLookup(_)) -> {
+                // For now, we just treat them as resolved constraints :shrug:
+              }
+              case Either.Left(var error) -> {
+                // Could not resolve child witness
+                yield Either.left(
+                    new MatchFailure.UnresolvedConstraint<>(ctor, node.type(), error));
+              }
+            }
+          }
+        }
+
+        yield Either.right(
+            new Match<>(
+                ctor,
+                Unification.substituteAll(substitution, ctor.paramTypes()),
+                Unification.substitute(substitution, ctor.returnType())));
+      }
     };
   }
 
-  private static <M, V, C, P> Maybe<Match<M, V, C, P>> match(
-      WitnessConstructor<M, V, C, P> ctor, ParsedType<V, C, P> target) {
-    return Unification.unify(ctor.returnType(), target)
-        .map(map -> Unification.substituteAll(map, ctor.paramTypes()))
-        .map(dependencies -> new Match<>(ctor, dependencies, target));
+  private static <V, C, P> Node<V, C, P> parseNode(ParsedType<V, C, P> type) {
+    return new Node<>(
+        type,
+        Types.findOutVars(type).collect(toUnmodifiableSet()),
+        Types.findVars(type).collect(toUnmodifiableSet()));
+  }
+
+  private static <M, V, C, P> Either<Failure<M, V, C, P>, Result<M, V, C, P>> flatten(
+      Either<Failure<M, V, C, P>, Result<M, V, C, P>> result) {
+    return switch (result) {
+      case Either.Right(Result.LazyWrap(var under)) -> flatten(Either.right(under));
+      default -> result;
+    };
+  }
+
+  private record Node<V, C, P>(
+      ParsedType<V, C, P> type, Set<Var<V, C, P>> out, Set<Var<V, C, P>> in) {}
+
+  public sealed interface MatchFailure<M, V, C, P> {
+    record HeadMismatch<M, V, C, P>(WitnessConstructor<M, V, C, P> ctor)
+        implements MatchFailure<M, V, C, P> {}
+
+    record Cycle<M, V, C, P>(WitnessConstructor<M, V, C, P> ctor, List<ParsedType<V, C, P>> types)
+        implements MatchFailure<M, V, C, P> {}
+
+    record UnresolvedConstraint<M, V, C, P>(
+        WitnessConstructor<M, V, C, P> ctor,
+        ParsedType<V, C, P> constraint,
+        Failure<M, V, C, P> cause)
+        implements MatchFailure<M, V, C, P> {}
+
+    record ResolvedConstraintMismatch<M, V, C, P>(
+        WitnessConstructor<M, V, C, P> ctor,
+        ParsedType<V, C, P> expected,
+        ParsedType<V, C, P> actual)
+        implements MatchFailure<M, V, C, P> {}
+
+    record UnboundVariables<M, V, C, P>(
+        WitnessConstructor<M, V, C, P> ctor, Set<Var<V, C, P>> variables)
+        implements MatchFailure<M, V, C, P> {}
+
+    record UnproductiveConstraint<M, V, C, P>(
+        WitnessConstructor<M, V, C, P> ctor, Set<Var<V, C, P>> variables)
+        implements MatchFailure<M, V, C, P> {}
+
+    record ConflictingSubstitution<M, V, C, P>(
+        WitnessConstructor<M, V, C, P> ctor,
+        Var<V, C, P> variable,
+        ParsedType<V, C, P> existing,
+        ParsedType<V, C, P> conflicting)
+        implements MatchFailure<M, V, C, P> {}
+
+    default String format() {
+      return switch (this) {
+        case HeadMismatch(var ctor) ->
+            "Witness constructor " + ctor.format() + " does not match the target type.";
+        case Cycle(var ctor, var types) ->
+            "Witness constructor "
+                + ctor.format()
+                + " has cyclic dependencies: "
+                + types.stream().map(ParsedType::format).collect(Collectors.joining(", "));
+        case UnresolvedConstraint(var ctor, var constraint, var cause) ->
+            "Could not resolve constraint "
+                + constraint.format()
+                + " for witness constructor "
+                + ctor.format()
+                + ":\nCaused by: "
+                + cause.format().indent(2);
+        case ResolvedConstraintMismatch(var ctor, var expected, var actual) ->
+            "Resolved constraint for witness constructor "
+                + ctor.format()
+                + " does not match expected type: expected "
+                + expected.format()
+                + ", got "
+                + actual.format()
+                + ".";
+        case UnboundVariables(var ctor, var variables) ->
+            "Witness constructor "
+                + ctor.format()
+                + " has unbound input variables: "
+                + variables.stream().map(Var::format).collect(Collectors.joining(", "));
+        case UnproductiveConstraint(var ctor, var variables) ->
+            "Witness constructor "
+                + ctor.format()
+                + " has unproductive output variables: "
+                + variables.stream().map(Var::format).collect(Collectors.joining(", "));
+        case ConflictingSubstitution(var ctor, var variable, var existing, var conflicting) ->
+            "Witness constructor "
+                + ctor.format()
+                + " has conflicting substitutions for variable "
+                + variable.format()
+                + ": existing substitution "
+                + existing.format()
+                + ", conflicting substitution "
+                + conflicting.format()
+                + ".";
+      };
+    }
   }
 
   public sealed interface Failure<M, V, C, P> {
-    record NotFound<M, V, C, P>(ParsedType<V, C, P> target) implements Failure<M, V, C, P> {}
+    record NoMatch<M, V, C, P>(
+        ParsedType<V, C, P> target,
+        List<MatchFailure<M, V, C, P>> failures,
+        List<Match<M, V, C, P>> matches)
+        implements Failure<M, V, C, P> {}
 
     record Ambiguous<M, V, C, P>(ParsedType<V, C, P> target, List<Match<M, V, C, P>> candidates)
         implements Failure<M, V, C, P> {}
@@ -63,7 +280,22 @@ record Nested<M, V, C, P>(ParsedType<V, C, P> target, Failure<M, V, C, P> cause)
 
     default String format() {
       return switch (this) {
-        case NotFound(var target) -> "No witness found for type: " + target.format();
+        case NoMatch(var target, var failures, var matches) ->
+            "No witnesses found for type: "
+                + target.format()
+                + "\nFailures:\n"
+                + failures.stream()
+                    .map(MatchFailure::format)
+                    .collect(Collectors.joining("\n"))
+                    .indent(2)
+                + (matches.isEmpty()
+                    ? ""
+                    : "\nPartial matches:\n"
+                        + matches.stream()
+                            .map(Match::ctor)
+                            .map(WitnessConstructor::format)
+                            .collect(Collectors.joining("\n"))
+                            .indent(2));
         case Ambiguous(var target, var candidates) ->
             "Ambiguous witnesses found for type: "
                 + target.format()
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/Types.java b/core/src/main/java/com/garciat/typeclasses/impl/Types.java
new file mode 100644
index 0000000..c03eb56
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/impl/Types.java
@@ -0,0 +1,45 @@
+package com.garciat.typeclasses.impl;
+
+import java.util.stream.Stream;
+
+public final class Types {
+  private Types() {}
+
+  public static <V, C, P> Stream<ParsedType.Var<V, C, P>> findOutVars(ParsedType<V, C, P> type) {
+    return switch (type) {
+      case ParsedType.Var(_) -> Stream.of();
+      case ParsedType.Out(ParsedType.Var<V, C, P> v) -> Stream.of(v);
+      case ParsedType.Out(_) -> Stream.of();
+      case ParsedType.App(var fun, var arg) -> Stream.concat(findOutVars(fun), findOutVars(arg));
+      case ParsedType.ArrayOf(var elem) -> findOutVars(elem);
+      case ParsedType.Lazy(var under) -> findOutVars(under);
+      case ParsedType.Const(_, _), ParsedType.Primitive(_), ParsedType.Wildcard() -> Stream.of();
+    };
+  }
+
+  public static <V, C, P> Stream<ParsedType.Var<V, C, P>> findVars(ParsedType<V, C, P> type) {
+    return switch (type) {
+      case ParsedType.Var<V, C, P> v -> Stream.of(v);
+      case ParsedType.Out(_) -> Stream.of();
+      case ParsedType.App(var fun, var arg) -> Stream.concat(findVars(fun), findVars(arg));
+      case ParsedType.ArrayOf(var elem) -> findVars(elem);
+      case ParsedType.Lazy(var under) -> findVars(under);
+      case ParsedType.Const(_, _), ParsedType.Primitive(_), ParsedType.Wildcard() -> Stream.of();
+    };
+  }
+
+  /** Unwraps one level of Out from the given type. */
+  public static <C, P, V> ParsedType<V, C, P> unwrapOut1(ParsedType<V, C, P> type) {
+    return switch (type) {
+      case ParsedType.Out(var under) -> under;
+      case ParsedType.App(var fun, var arg) ->
+          new ParsedType.App<>(unwrapOut1(fun), unwrapOut1(arg));
+      case ParsedType.ArrayOf(var elem) -> new ParsedType.ArrayOf<>(unwrapOut1(elem));
+      case ParsedType.Lazy(var t) -> new ParsedType.Lazy<>(unwrapOut1(t));
+      case ParsedType.Var<V, C, P> v -> v;
+      case ParsedType.Primitive<V, C, P> p -> p;
+      case ParsedType.Const<V, C, P> c -> c;
+      case ParsedType.Wildcard<V, C, P> w -> w;
+    };
+  }
+}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/Unification.java b/core/src/main/java/com/garciat/typeclasses/impl/Unification.java
index 250c976..e3a88aa 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/Unification.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/Unification.java
@@ -3,6 +3,8 @@
 import com.garciat.typeclasses.impl.ParsedType.App;
 import com.garciat.typeclasses.impl.ParsedType.ArrayOf;
 import com.garciat.typeclasses.impl.ParsedType.Const;
+import com.garciat.typeclasses.impl.ParsedType.Lazy;
+import com.garciat.typeclasses.impl.ParsedType.Out;
 import com.garciat.typeclasses.impl.ParsedType.Primitive;
 import com.garciat.typeclasses.impl.ParsedType.Var;
 import com.garciat.typeclasses.impl.ParsedType.Wildcard;
@@ -22,6 +24,8 @@ private Unification() {}
   public static <V, C, P> Maybe<Map<Var<V, C, P>, ParsedType<V, C, P>>> unify(
       ParsedType<V, C, P> t1, ParsedType<V, C, P> t2) {
     return switch (Pair.of(t1, t2)) {
+      case Pair(Lazy(var x), var t) -> unify(x, t);
+      case Pair(var t, Lazy(var x)) -> unify(t, x);
       case Pair(Var(_), Primitive(_)) -> Maybe.nothing(); // no primitives in generics
       case Pair(Var<V, C, P> v, var t) -> Maybe.just(Map.of(v, t));
       case Pair(Const(var repr1, _), Const(var repr2, _)) when repr1.equals(repr2) ->
@@ -31,8 +35,12 @@ case Pair(App(var fun1, var arg1), App(var fun2, var arg2)) ->
       case Pair(ArrayOf(var elem1), ArrayOf(var elem2)) -> unify(elem1, elem2);
       case Pair(Primitive(var prim1), Primitive(var prim2)) when prim1.equals(prim2) ->
           Maybe.just(Map.of());
+      // Wildcards can match anything
       case Pair(Wildcard(), _) -> Maybe.just(Map.of());
-      default -> Maybe.nothing();
+      // Out types match each other, regardless of their inner types
+      // The resolution algorithm will check compatibility later
+      case Pair(Out(_), Out(_)) -> Maybe.just(Map.of());
+      case Pair(_, _) -> Maybe.nothing();
     };
   }
 
@@ -40,8 +48,10 @@ public static <V, C, P> ParsedType<V, C, P> substitute(
       Map<Var<V, C, P>, ParsedType<V, C, P>> map, ParsedType<V, C, P> type) {
     return switch (type) {
       case Var<V, C, P> var -> map.getOrDefault(var, var);
+      case Out(var under) -> new Out<>(substitute(map, under));
       case App(var fun, var arg) -> new App<>(substitute(map, fun), substitute(map, arg));
       case ArrayOf(var elem) -> new ArrayOf<>(substitute(map, elem));
+      case Lazy(var t) -> new Lazy<>(substitute(map, t));
       case Primitive<V, C, P> p -> p;
       case Const<V, C, P> c -> c;
       case Wildcard<V, C, P> w -> w;
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/WitnessConstructor.java b/core/src/main/java/com/garciat/typeclasses/impl/WitnessConstructor.java
index 0f30d0d..5b43d17 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/WitnessConstructor.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/WitnessConstructor.java
@@ -7,14 +7,15 @@
 public record WitnessConstructor<M, V, C, P>(
     M method,
     TypeClass.Witness.Overlap overlap,
-    List<ParsedType.Var<V, C, P>> typeParams,
+    List<ParsedType.TyParam<V>> typeParams,
     List<ParsedType<V, C, P>> paramTypes,
     ParsedType<V, C, P> returnType) {
   public String format() {
     return String.format(
-        "%s%s -> %s",
+        "%s = %s%s -> %s",
+        method.toString(),
         typeParams().stream()
-            .map(ParsedType::format)
+            .map(ParsedType.TyParam::toString)
             .reduce((a, b) -> a + " " + b)
             .map("∀ %s. "::formatted)
             .orElse(""),
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/Witnesses.java b/core/src/main/java/com/garciat/typeclasses/impl/Witnesses.java
new file mode 100644
index 0000000..f6a8777
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/impl/Witnesses.java
@@ -0,0 +1,27 @@
+package com.garciat.typeclasses.impl;
+
+import com.garciat.typeclasses.impl.utils.Lists;
+import java.util.List;
+import java.util.function.Function;
+
+final class Witnesses {
+  private Witnesses() {}
+
+  static <M, V, C, P> List<WitnessConstructor<M, V, C, P>> findWitnesses(
+      Function<C, List<WitnessConstructor<M, V, C, P>>> constructors, ParsedType<V, C, P> target) {
+    return switch (target) {
+      case ParsedType.App(var fun1, ParsedType.App(var fun2, _)) ->
+          Lists.concat(findWitnesses(constructors, fun1), findWitnesses(constructors, fun2));
+      case ParsedType.App(var fun, var arg) ->
+          Lists.concat(findWitnesses(constructors, fun), findWitnesses(constructors, arg));
+      case ParsedType.Const<V, C, P> c -> constructors.apply(c.repr());
+      case ParsedType.Lazy(var under) -> findWitnesses(constructors, under);
+      case ParsedType.Var(_),
+          ParsedType.Out(_),
+          ParsedType.ArrayOf(_),
+          ParsedType.Primitive(_),
+          ParsedType.Wildcard() ->
+          List.of();
+    };
+  }
+}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/AutoCloseables.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/AutoCloseables.java
new file mode 100644
index 0000000..c28e628
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/impl/utils/AutoCloseables.java
@@ -0,0 +1,23 @@
+package com.garciat.typeclasses.impl.utils;
+
+public final class AutoCloseables {
+  private AutoCloseables() {}
+
+  public static SafeAutoCloseable around(Runnable before, Runnable after) {
+    return new SafeAutoCloseable() {
+      {
+        before.run();
+      }
+
+      @Override
+      public void close() {
+        after.run();
+      }
+    };
+  }
+
+  public interface SafeAutoCloseable extends AutoCloseable {
+    @Override
+    void close();
+  }
+}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/Either.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/Either.java
index 823dd34..235cfd4 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/utils/Either.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/utils/Either.java
@@ -2,7 +2,6 @@
 
 import java.util.ArrayList;
 import java.util.List;
-import java.util.concurrent.Callable;
 import java.util.function.Function;
 
 public sealed interface Either<L, R> {
@@ -18,14 +17,6 @@ static <L, R> Either<L, R> right(R value) {
     return new Right<>(value);
   }
 
-  static <A> Either<Exception, A> call(Callable<A> callable) {
-    try {
-      return right(callable.call());
-    } catch (Exception e) {
-      return left(e);
-    }
-  }
-
   default <X> Either<L, X> map(Function<? super R, ? extends X> f) {
     return fold(Either::left, f.andThen(Either::right));
   }
@@ -60,4 +51,20 @@ case Right(R value) -> {
     }
     return right(result);
   }
+
+  static <L, R> Pair<List<L>, List<R>> partition(List<Either<L, R>> eithers) {
+    List<L> lefts = new ArrayList<>();
+    List<R> rights = new ArrayList<>();
+    for (Either<L, R> either : eithers) {
+      switch (either) {
+        case Left(L value) -> {
+          lefts.add(value);
+        }
+        case Right(R value) -> {
+          rights.add(value);
+        }
+      }
+    }
+    return new Pair<>(lefts, rights);
+  }
 }
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/Formatter.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/Formatter.java
deleted file mode 100644
index 3e97bbd..0000000
--- a/core/src/main/java/com/garciat/typeclasses/impl/utils/Formatter.java
+++ /dev/null
@@ -1,5 +0,0 @@
-package com.garciat.typeclasses.impl.utils;
-
-import java.util.function.Function;
-
-public interface Formatter<A> extends Function<A, String> {}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/Lists.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/Lists.java
index d25373c..e3378aa 100644
--- a/core/src/main/java/com/garciat/typeclasses/impl/utils/Lists.java
+++ b/core/src/main/java/com/garciat/typeclasses/impl/utils/Lists.java
@@ -2,8 +2,10 @@
 
 import java.util.Arrays;
 import java.util.List;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.stream.Collectors;
+import java.util.stream.IntStream;
 
 public final class Lists {
   private Lists() {}
@@ -12,6 +14,17 @@ public static <A, B> List<B> map(List<A> list, Function<? super A, ? extends B>
     return list.stream().map(f).collect(Collectors.toList());
   }
 
+  public static <A, B, C> List<C> zip(
+      List<A> list1, List<B> list2, BiFunction<? super A, ? super B, ? extends C> f) {
+    if (list1.size() != list2.size()) {
+      throw new IllegalArgumentException("Lists must have the same size to be zipped.");
+    }
+    int size = list1.size();
+    return IntStream.range(0, size)
+        .mapToObj(i -> f.apply(list1.get(i), list2.get(i)))
+        .collect(Collectors.toList());
+  }
+
   @SafeVarargs
   public static <A> List<A> concat(List<A>... lists) {
     return Arrays.stream(lists).flatMap(List::stream).toList();
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/Rose.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/Rose.java
deleted file mode 100644
index ca6b5cd..0000000
--- a/core/src/main/java/com/garciat/typeclasses/impl/utils/Rose.java
+++ /dev/null
@@ -1,11 +0,0 @@
-package com.garciat.typeclasses.impl.utils;
-
-import java.util.List;
-
-public sealed interface Rose<A> {
-  record Node<A>(A value, List<Rose<A>> children) implements Rose<A> {}
-
-  static <A> Rose<A> of(A value, List<Rose<A>> children) {
-    return new Node<>(value, children);
-  }
-}
diff --git a/core/src/main/java/com/garciat/typeclasses/impl/utils/Sets.java b/core/src/main/java/com/garciat/typeclasses/impl/utils/Sets.java
new file mode 100644
index 0000000..8a4ba2d
--- /dev/null
+++ b/core/src/main/java/com/garciat/typeclasses/impl/utils/Sets.java
@@ -0,0 +1,13 @@
+package com.garciat.typeclasses.impl.utils;
+
+import java.util.Set;
+
+public final class Sets {
+  private Sets() {}
+
+  public static <T> Set<T> difference(Set<T> a, Set<T> b) {
+    Set<T> result = new java.util.HashSet<>(a);
+    result.removeAll(b);
+    return result;
+  }
+}
diff --git a/core/src/main/java/com/garciat/typeclasses/processor/Static.java b/core/src/main/java/com/garciat/typeclasses/processor/Static.java
index 5f224d0..18429a4 100644
--- a/core/src/main/java/com/garciat/typeclasses/processor/Static.java
+++ b/core/src/main/java/com/garciat/typeclasses/processor/Static.java
@@ -8,7 +8,12 @@
 public final class Static {
   private Static() {}
 
-  public record Method(ExecutableElement java) {}
+  public record Method(ExecutableElement java) {
+    @Override
+    public String toString() {
+      return java.getEnclosingElement().getSimpleName() + "." + java.getSimpleName();
+    }
+  }
 
   public record Var(TypeVariable java) {
     @Override
diff --git a/core/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java b/core/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java
index 80379c9..c8d9de7 100644
--- a/core/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java
+++ b/core/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java
@@ -2,30 +2,32 @@
 
 import static com.garciat.typeclasses.impl.utils.Streams.isInstanceOf;
 
+import com.garciat.typeclasses.api.Lazy;
+import com.garciat.typeclasses.api.Out;
 import com.garciat.typeclasses.api.TypeClass;
 import com.garciat.typeclasses.api.hkt.TApp;
 import com.garciat.typeclasses.api.hkt.TPar;
 import com.garciat.typeclasses.api.hkt.TagBase;
-import com.garciat.typeclasses.impl.Match;
 import com.garciat.typeclasses.impl.ParsedType;
 import com.garciat.typeclasses.impl.ParsedType.App;
 import com.garciat.typeclasses.impl.ParsedType.ArrayOf;
 import com.garciat.typeclasses.impl.ParsedType.Const;
 import com.garciat.typeclasses.impl.ParsedType.Primitive;
+import com.garciat.typeclasses.impl.ParsedType.TyParam;
 import com.garciat.typeclasses.impl.ParsedType.Var;
 import com.garciat.typeclasses.impl.ParsedType.Wildcard;
 import com.garciat.typeclasses.impl.Resolution;
 import com.garciat.typeclasses.impl.WitnessConstructor;
 import com.garciat.typeclasses.impl.utils.Either;
+import com.garciat.typeclasses.impl.utils.Lists;
 import com.garciat.typeclasses.impl.utils.Maybe;
 import com.garciat.typeclasses.impl.utils.Pair;
-import com.garciat.typeclasses.impl.utils.Rose;
 import java.util.List;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.Modifier;
 import javax.lang.model.element.Parameterizable;
 import javax.lang.model.element.TypeElement;
-import javax.lang.model.element.VariableElement;
+import javax.lang.model.element.TypeParameterElement;
 import javax.lang.model.type.ArrayType;
 import javax.lang.model.type.DeclaredType;
 import javax.lang.model.type.PrimitiveType;
@@ -38,14 +40,14 @@ private StaticWitnessSystem() {}
 
   public static Either<
           Resolution.Failure<Static.Method, Static.Var, Static.Const, Static.Prim>,
-          Rose<Match<Static.Method, Static.Var, Static.Const, Static.Prim>>>
+          Resolution.Result<Static.Method, Static.Var, Static.Const, Static.Prim>>
       resolve(TypeMirror target) {
-    return Resolution.resolve(StaticWitnessSystem::findWitnesses, Rose::of, parse(target));
+    return Resolution.resolve(StaticWitnessSystem::findWitnesses, parse(target));
   }
 
   private static List<WitnessConstructor<Static.Method, Static.Var, Static.Const, Static.Prim>>
-      findWitnesses(ParsedType.Const<Static.Var, Static.Const, Static.Prim> target) {
-    return target.repr().java().getEnclosedElements().stream()
+      findWitnesses(Static.Const target) {
+    return target.java().getEnclosedElements().stream()
         .flatMap(isInstanceOf(ExecutableElement.class))
         .flatMap(method -> parseWitnessConstructor(method).stream())
         .toList();
@@ -61,10 +63,7 @@ private StaticWitnessSystem() {}
               new Static.Method(method),
               witnessAnn.overlap(),
               typeParams(method),
-              method.getParameters().stream()
-                  .map(VariableElement::asType)
-                  .map(StaticWitnessSystem::parse)
-                  .toList(),
+              Lists.map(method.getParameters(), p -> parse(p.asType())),
               parse(method.getReturnType())));
 
     } else {
@@ -74,17 +73,23 @@ private StaticWitnessSystem() {}
 
   private static ParsedType<Static.Var, Static.Const, Static.Prim> parse(TypeMirror type) {
     return switch (type) {
-      case TypeVariable tv -> new Var<>(new Static.Var(tv));
+      case TypeVariable tv -> new Var<>(typeParam((TypeParameterElement) tv.asElement()));
       case ArrayType at -> new ArrayOf<>(parse(at.getComponentType()));
       case PrimitiveType pt -> new Primitive<>(new Static.Prim(pt));
       case DeclaredType dt when parseTagType(dt) instanceof Maybe.Just(var realType) ->
           constType(realType);
       case DeclaredType dt when parseAppType(dt) instanceof Maybe.Just(Pair(var fun, var arg)) ->
           new App<>(parse(fun), parse(arg));
-      case DeclaredType dt ->
-          dt.getTypeArguments().stream()
-              .map(StaticWitnessSystem::parse)
-              .reduce(constType(erasure(dt)), App::new);
+      case DeclaredType dt when parseLazyType(dt) instanceof Maybe.Just(var under) ->
+          new ParsedType.Lazy<>(parse(under));
+      case DeclaredType dt -> {
+        Const<Static.Var, Static.Const, Static.Prim> decl = constType(erasure(dt));
+
+        List<ParsedType<Static.Var, Static.Const, Static.Prim>> args =
+            dt.getTypeArguments().stream().map(StaticWitnessSystem::parse).toList();
+
+        yield Lists.zip(decl.typeParams(), args, TyParam::wrapOut).stream().reduce(decl, App::new);
+      }
       case WildcardType _ -> new Wildcard<>();
       default -> throw new IllegalArgumentException("Unsupported type: " + type);
     };
@@ -94,13 +99,23 @@ private static Const<Static.Var, Static.Const, Static.Prim> constType(TypeElemen
     return new Const<>(new Static.Const(typeElement), typeParams(typeElement));
   }
 
-  private static List<Var<Static.Var, Static.Const, Static.Prim>> typeParams(Parameterizable tp) {
-    return tp.getTypeParameters().stream()
-        .map(
-            tpe ->
-                new Var<Static.Var, Static.Const, Static.Prim>(
-                    new Static.Var((TypeVariable) tpe.asType())))
-        .toList();
+  private static List<TyParam<Static.Var>> typeParams(Parameterizable tp) {
+    return Lists.map(tp.getTypeParameters(), StaticWitnessSystem::typeParam);
+  }
+
+  private static TyParam<Static.Var> typeParam(TypeParameterElement element) {
+    return new TyParam<>(
+        new Static.Var((TypeVariable) element.asType()), element.getAnnotation(Out.class) != null);
+  }
+
+  private static Maybe<TypeMirror> parseLazyType(DeclaredType t) {
+    if (t.asElement() instanceof TypeElement te
+        && te.getQualifiedName().contentEquals(Lazy.class.getName())
+        && t.getTypeArguments().size() == 1) {
+      return Maybe.just(t.getTypeArguments().getFirst());
+    } else {
+      return Maybe.nothing();
+    }
   }
 
   private static Maybe<TypeElement> parseTagType(DeclaredType t) {
diff --git a/core/src/main/java/com/garciat/typeclasses/runtime/Runtime.java b/core/src/main/java/com/garciat/typeclasses/runtime/Runtime.java
index eecea57..1d4f8a9 100644
--- a/core/src/main/java/com/garciat/typeclasses/runtime/Runtime.java
+++ b/core/src/main/java/com/garciat/typeclasses/runtime/Runtime.java
@@ -3,7 +3,12 @@
 public final class Runtime {
   private Runtime() {}
 
-  public record Method(java.lang.reflect.Method java) {}
+  public record Method(java.lang.reflect.Method java) {
+    @Override
+    public String toString() {
+      return java.getDeclaringClass().getSimpleName() + "." + java.getName();
+    }
+  }
 
   public record Var(java.lang.reflect.TypeVariable<?> java) {
     @Override
diff --git a/core/src/main/java/com/garciat/typeclasses/runtime/RuntimeWitnessSystem.java b/core/src/main/java/com/garciat/typeclasses/runtime/RuntimeWitnessSystem.java
index 436b927..a702f7c 100644
--- a/core/src/main/java/com/garciat/typeclasses/runtime/RuntimeWitnessSystem.java
+++ b/core/src/main/java/com/garciat/typeclasses/runtime/RuntimeWitnessSystem.java
@@ -1,20 +1,22 @@
 package com.garciat.typeclasses.runtime;
 
+import com.garciat.typeclasses.api.Out;
 import com.garciat.typeclasses.api.TypeClass;
 import com.garciat.typeclasses.api.hkt.TApp;
 import com.garciat.typeclasses.api.hkt.TPar;
 import com.garciat.typeclasses.api.hkt.TagBase;
-import com.garciat.typeclasses.impl.Match;
 import com.garciat.typeclasses.impl.ParsedType;
 import com.garciat.typeclasses.impl.ParsedType.App;
 import com.garciat.typeclasses.impl.ParsedType.ArrayOf;
 import com.garciat.typeclasses.impl.ParsedType.Const;
 import com.garciat.typeclasses.impl.ParsedType.Primitive;
+import com.garciat.typeclasses.impl.ParsedType.TyParam;
 import com.garciat.typeclasses.impl.ParsedType.Var;
 import com.garciat.typeclasses.impl.ParsedType.Wildcard;
 import com.garciat.typeclasses.impl.Resolution;
 import com.garciat.typeclasses.impl.WitnessConstructor;
 import com.garciat.typeclasses.impl.utils.Either;
+import com.garciat.typeclasses.impl.utils.Lists;
 import com.garciat.typeclasses.impl.utils.Maybe;
 import com.garciat.typeclasses.impl.utils.Pair;
 import java.lang.reflect.GenericArrayType;
@@ -27,24 +29,20 @@
 import java.lang.reflect.WildcardType;
 import java.util.Arrays;
 import java.util.List;
-import java.util.function.BiFunction;
 
 public final class RuntimeWitnessSystem {
   private RuntimeWitnessSystem() {}
 
-  public static <R>
-      Either<Resolution.Failure<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim>, R>
-          resolve(
-              Type type,
-              BiFunction<
-                      Match<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim>, List<R>, R>
-                  build) {
-    return Resolution.resolve(RuntimeWitnessSystem::findWitnesses, build, parse(type));
+  public static Either<
+          Resolution.Failure<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim>,
+          Resolution.Result<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim>>
+      resolve(Type type) {
+    return Resolution.resolve(RuntimeWitnessSystem::findWitnesses, parse(type));
   }
 
   private static List<WitnessConstructor<Runtime.Method, Runtime.Var, Runtime.Const, Runtime.Prim>>
-      findWitnesses(ParsedType.Const<Runtime.Var, Runtime.Const, Runtime.Prim> target) {
-    return Arrays.stream(target.repr().java().getDeclaredMethods())
+      findWitnesses(Runtime.Const target) {
+    return Arrays.stream(target.java().getDeclaredMethods())
         .flatMap(m -> parseWitnessConstructor(m).stream())
         .toList();
   }
@@ -68,20 +66,26 @@ private RuntimeWitnessSystem() {}
     }
   }
 
-  private static ParsedType<Runtime.Var, Runtime.Const, Runtime.Prim> parse(Type java) {
+  public static ParsedType<Runtime.Var, Runtime.Const, Runtime.Prim> parse(Type java) {
     return switch (java) {
       case Class<?> tag when parseTagType(tag) instanceof Maybe.Just(var tagged) ->
           constType(tagged);
       case Class<?> arr when arr.isArray() -> new ArrayOf<>(parse(arr.getComponentType()));
       case Class<?> prim when prim.isPrimitive() -> new Primitive<>(new Runtime.Prim(prim));
       case Class<?> c -> constType(c);
-      case TypeVariable<?> v -> new Var<>(new Runtime.Var(v));
+      case TypeVariable<?> v -> new Var<>(typeParam(v));
       case ParameterizedType p when parseAppType(p) instanceof Maybe.Just(Pair(var fun, var arg)) ->
           new App<>(parse(fun), parse(arg));
-      case ParameterizedType p ->
-          Arrays.stream(p.getActualTypeArguments())
-              .map(RuntimeWitnessSystem::parse)
-              .reduce(parse(p.getRawType()), App::new);
+      case ParameterizedType p when parseLazyType(p) instanceof Maybe.Just(var under) ->
+          new ParsedType.Lazy<>(parse(under));
+      case ParameterizedType p -> {
+        Const<Runtime.Var, Runtime.Const, Runtime.Prim> decl = constType((Class<?>) p.getRawType());
+
+        List<ParsedType<Runtime.Var, Runtime.Const, Runtime.Prim>> args =
+            Arrays.stream(p.getActualTypeArguments()).map(RuntimeWitnessSystem::parse).toList();
+
+        yield Lists.zip(decl.typeParams(), args, TyParam::wrapOut).stream().reduce(decl, App::new);
+      }
       case GenericArrayType a -> new ArrayOf<>(parse(a.getGenericComponentType()));
       case WildcardType _ -> new Wildcard<>();
       default -> throw new IllegalArgumentException("Unsupported type: " + java);
@@ -92,16 +96,27 @@ private static Const<Runtime.Var, Runtime.Const, Runtime.Prim> constType(Class<?
     return new Const<>(new Runtime.Const(tagged), typeParams(tagged));
   }
 
-  private static List<Var<Runtime.Var, Runtime.Const, Runtime.Prim>> typeParams(
-      GenericDeclaration cls) {
-    return Arrays.stream(cls.getTypeParameters())
-        .map(t -> new Var<Runtime.Var, Runtime.Const, Runtime.Prim>(new Runtime.Var(t)))
-        .toList();
+  private static List<TyParam<Runtime.Var>> typeParams(GenericDeclaration cls) {
+    return Arrays.stream(cls.getTypeParameters()).map(RuntimeWitnessSystem::typeParam).toList();
+  }
+
+  private static TyParam<Runtime.Var> typeParam(TypeVariable<?> t) {
+    return new TyParam<>(new Runtime.Var(t), t.isAnnotationPresent(Out.class));
+  }
+
+  private static Maybe<Type> parseLazyType(ParameterizedType t) {
+    return switch (t.getRawType()) {
+      case Class<?> raw when raw.equals(com.garciat.typeclasses.api.Lazy.class) ->
+          Maybe.just(t.getActualTypeArguments()[0]);
+      default -> Maybe.nothing();
+    };
   }
 
   private static Maybe<Class<?>> parseTagType(Class<?> c) {
     return switch (c.getEnclosingClass()) {
-      case Class<?> enclosing when c.getSuperclass().equals(TagBase.class) -> Maybe.just(enclosing);
+      case Class<?> enclosing
+          when c.getSuperclass() instanceof Class<?> sup && sup.equals(TagBase.class) ->
+          Maybe.just(enclosing);
       case null, default -> Maybe.nothing();
     };
   }
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example1.java b/core/src/test/java/com/garciat/typeclasses/examples/Example1.java
new file mode 100644
index 0000000..0b54c8f
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example1.java
@@ -0,0 +1,47 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import java.util.List;
+import java.util.stream.Collectors;
+import org.junit.jupiter.api.Test;
+
+public class Example1 {
+  @Test
+  void main() {
+    Pair<Integer, List<Integer>> value = new Pair<>(1, List.of(2, 3, 4));
+
+    String s = Show.show(witness(new Ty<>() {}), value);
+
+    assertThat(s).isEqualTo("(1, [2, 3, 4])");
+  }
+
+  @TypeClass
+  public interface Show<T> {
+    String show(T value);
+
+    static <T> String show(Show<T> showT, T value) {
+      return showT.show(value);
+    }
+
+    @TypeClass.Witness
+    static Show<Integer> integerShow() {
+      return i -> Integer.toString(i);
+    }
+
+    @TypeClass.Witness
+    static <A> Show<List<A>> listShow(Show<A> showA) {
+      return listA -> listA.stream().map(showA::show).collect(Collectors.joining(", ", "[", "]"));
+    }
+  }
+
+  public record Pair<A, B>(A first, B second) {
+    @TypeClass.Witness
+    public static <A, B> Show<Pair<A, B>> pairShow(Show<A> showA, Show<B> showB) {
+      return pair -> "(" + showA.show(pair.first()) + ", " + showB.show(pair.second()) + ")";
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example2.java b/core/src/test/java/com/garciat/typeclasses/examples/Example2.java
new file mode 100644
index 0000000..2b86ed1
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example2.java
@@ -0,0 +1,50 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import com.garciat.typeclasses.examples.Example2.TList.TCons;
+import com.garciat.typeclasses.examples.Example2.TList.TNil;
+import org.junit.jupiter.api.Test;
+
+/// Based on:
+///
+/// ```haskell
+/// class In (xs :: [k]) (x :: k)
+///
+/// instance In (x ': xs) x
+///
+/// instance {-# OVERLAPPABLE #-} In xs y => In (x ': xs) y
+///
+/// example :: In '[Int, Bool, Char] Bool => ()
+/// example = ()
+/// ```
+public class Example2 {
+  @Test
+  void main() {
+    In<TCons<Byte, TCons<Short, TCons<Integer, TNil>>>, Short> w = witness(new Ty<>() {});
+
+    assertThat(w).isNotNull();
+  }
+
+  public interface TList<T extends TList<T>> {
+    record TNil() implements TList<TNil> {}
+
+    record TCons<T, TS extends TList<TS>>() implements TList<TCons<T, TS>> {}
+  }
+
+  @TypeClass
+  public interface In<TS extends TList<TS>, Y> {
+    @TypeClass.Witness
+    static <X, XS extends TList<XS>> In<TCons<X, XS>, X> here() {
+      return new In<>() {};
+    }
+
+    @TypeClass.Witness(overlap = TypeClass.Witness.Overlap.OVERLAPPABLE)
+    static <X, XS extends TList<XS>, Y> In<TCons<X, XS>, Y> there(In<XS, Y> there) {
+      return new In<>() {};
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example3.java b/core/src/test/java/com/garciat/typeclasses/examples/Example3.java
new file mode 100644
index 0000000..5f65826
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example3.java
@@ -0,0 +1,145 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Lazy;
+import com.garciat.typeclasses.api.Out;
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import com.garciat.typeclasses.examples.Example3.TyRep.K1;
+import com.garciat.typeclasses.examples.Example3.TyRep.Prod;
+import com.garciat.typeclasses.examples.Example3.TyRep.Sum;
+import com.garciat.typeclasses.examples.Example3.TyRep.Sum.L1;
+import com.garciat.typeclasses.examples.Example3.TyRep.Sum.R1;
+import java.util.List;
+import org.junit.jupiter.api.Test;
+
+public final class Example3 {
+  @Test
+  void example() {
+    Tree.Node<Integer> tree =
+        new Tree.Node<>(
+            new Tree.Leaf<>(1), new Tree.Node<>(new Tree.Leaf<>(2), new Tree.Leaf<>(3)));
+
+    ToJson<Tree<Integer>> toJsonTree = witness(new Ty<>() {});
+
+    assertThat(toJsonTree.toJson(tree)).isEqualTo(array(value(1), array(value(2), value(3))));
+  }
+
+  private static JsonValue array(JsonValue... values) {
+    return new JsonValue.JsonArray(List.of(values));
+  }
+
+  private static JsonValue value(int value) {
+    return new JsonValue.JsonInteger(value);
+  }
+
+  @TypeClass
+  public interface Generic<A, @Out Rep> {
+    Rep from(A a);
+
+    A to(Rep rep);
+  }
+
+  public interface TyRep {
+    record K1<A>(A value) {}
+
+    sealed interface Sum<A, B> {
+      record L1<A, B>(A left) implements Sum<A, B> {}
+
+      record R1<A, B>(B right) implements Sum<A, B> {}
+    }
+
+    record Prod<A, B>(A first, B second) {}
+  }
+
+  public interface JsonValue {
+    record JsonString(String value) implements JsonValue {}
+
+    record JsonInteger(int value) implements JsonValue {}
+
+    record JsonObject(List<Prop> props) implements JsonValue {}
+
+    record JsonArray(List<JsonValue> values) implements JsonValue {}
+
+    record Prop(String key, JsonValue value) {}
+  }
+
+  @TypeClass
+  public interface ToJson<A> {
+    JsonValue toJson(A a);
+
+    @TypeClass.Witness
+    static ToJson<Integer> toJsonInteger() {
+      return JsonValue.JsonInteger::new;
+    }
+  }
+
+  @TypeClass
+  public interface ToJsonGeneric<Rep> {
+    JsonValue toJson(Rep rep);
+
+    static <A, Rep> ToJsonGeneric<Rep> toJsonGeneric(Generic<A, Rep> generic, ToJson<A> toJsonA) {
+      return rep -> toJsonA.toJson(generic.to(rep));
+    }
+
+    @TypeClass.Witness
+    static <A> ToJsonGeneric<K1<A>> k1(Lazy<ToJson<A>> toJsonA) {
+      return rep -> toJsonA.get().toJson(rep.value());
+    }
+
+    @TypeClass.Witness
+    static <A, B> ToJsonGeneric<Prod<A, B>> prod(
+        ToJsonGeneric<A> toJsonA, ToJsonGeneric<B> toJsonB) {
+      return rep ->
+          new JsonValue.JsonArray(
+              List.of(toJsonA.toJson(rep.first()), toJsonB.toJson(rep.second())));
+    }
+
+    @TypeClass.Witness
+    static <A, B> ToJsonGeneric<Sum<A, B>> sum(ToJsonGeneric<A> toJsonA, ToJsonGeneric<B> toJsonB) {
+      return rep ->
+          switch (rep) {
+            case L1(var value) -> toJsonA.toJson(value);
+            case R1(var value) -> toJsonB.toJson(value);
+          };
+    }
+  }
+
+  public sealed interface Tree<A> {
+    record Leaf<A>(A value) implements Tree<A> {}
+
+    record Node<A>(Tree<A> left, Tree<A> right) implements Tree<A> {}
+
+    @TypeClass.Witness
+    static <A, Rep> ToJson<Tree<A>> toJson(
+        Generic<Tree<A>, Rep> generic, ToJsonGeneric<Rep> toJsonGeneric) {
+      return tree -> toJsonGeneric.toJson(generic.from(tree));
+    }
+
+    @TypeClass.Witness
+    static <A> Generic<Tree<A>, Sum<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>>> generic() {
+      return new Generic<>() {
+        @Override
+        public Sum<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>> from(Tree<A> tree) {
+          return switch (tree) {
+            case Leaf<A> leaf ->
+                new L1<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>>(new K1<>(leaf.value));
+            case Node<A> node ->
+                new R1<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>>(
+                    new Prod<>(new K1<>(node.left), new K1<>(node.right)));
+          };
+        }
+
+        @Override
+        public Tree<A> to(Sum<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>> rep) {
+          return switch (rep) {
+            case L1(K1(var value)) -> new Leaf<>(value);
+            case R1(Prod(K1(var left), K1(var right))) -> new Node<>(left, right);
+          };
+        }
+      };
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example4.java b/core/src/test/java/com/garciat/typeclasses/examples/Example4.java
new file mode 100644
index 0000000..8547c74
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example4.java
@@ -0,0 +1,55 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Out;
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import java.util.List;
+import org.junit.jupiter.api.Test;
+
+/// Based on:
+///
+/// ```haskell
+/// type family ElementOf a where
+///   ElementOf [[a]] = ElementOf [a]
+///   ElementOf [a]   = a
+///
+/// class Flatten a where
+///   flatten :: a -> [ElementOf a]
+///
+/// instance Flatten [a] where
+///   flatten x = x
+///
+/// instance {-# OVERLAPPING #-} Flatten [a] => Flatten [[a]] where
+///   flatten x = flatten (concat x)
+/// ```
+///
+/// From: "An introduction to typeclass metaprogramming" by Alexis King
+public class Example4 {
+  @Test
+  void main() {
+    Flatten<List<List<String>>, String> e1 = witness(new Ty<>() {});
+    Flatten<List<String>, String> e2 = witness(new Ty<>() {});
+
+    assertThat(e1.flatten(List.of(List.of("a", "b"), List.of("c"))))
+        .isEqualTo(List.of("a", "b", "c"));
+    assertThat(e2.flatten(List.of("a", "b", "c"))).isEqualTo(List.of("a", "b", "c"));
+  }
+
+  @TypeClass
+  public interface Flatten<A, @Out T> {
+    List<T> flatten(A list);
+
+    @TypeClass.Witness
+    static <A> Flatten<List<A>, A> here() {
+      return list -> list;
+    }
+
+    @TypeClass.Witness(overlap = TypeClass.Witness.Overlap.OVERLAPPING)
+    static <A, R> Flatten<List<List<A>>, R> there(Flatten<List<A>, R> e) {
+      return list -> list.stream().flatMap(innerList -> e.flatten(innerList).stream()).toList();
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example5.java b/core/src/test/java/com/garciat/typeclasses/examples/Example5.java
new file mode 100644
index 0000000..c11aea3
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example5.java
@@ -0,0 +1,98 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Out;
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import com.garciat.typeclasses.examples.Example5.Nat.S;
+import com.garciat.typeclasses.examples.Example5.Nat.Z;
+import com.garciat.typeclasses.impl.utils.Unit;
+import org.junit.jupiter.api.Test;
+
+/// Based on:
+///
+/// ```haskell
+/// data Nat = Z | S Nat
+///
+/// class ReifyNat (a :: Nat) where
+///   reifyNat :: Natural
+///
+/// instance ReifyNat 'Z where
+///   reifyNat = 0
+///
+/// instance ReifyNat a => ReifyNat ('S a) where
+///   reifyNat = 1 + reifyNat @a
+/// ```
+public class Example5 {
+  @Test
+  void test1() {
+    ReifyNat<S<S<S<Z>>>> reifier = witness(new Ty<>() {});
+
+    assertThat(reifier.reify()).isEqualTo(3);
+  }
+
+  @Test
+  void test2() {
+    NatAdd<S<S<Z>>, S<S<S<Z>>>, S<S<S<S<S<Z>>>>>> adder = witness(new Ty<>() {});
+
+    assertThat(adder).isNotNull();
+  }
+
+  @Test
+  void test3() {
+    ReifyNatAdd<S<S<Z>>, S<S<S<Z>>>> reifyAdd = witness(new Ty<>() {});
+
+    assertThat(reifyAdd.reify()).isEqualTo(5);
+  }
+
+  public sealed interface Nat<N extends Nat<N>> {
+    record Z() implements Nat<Z> {}
+
+    // Note that we don't store the predecessor!
+    record S<N extends Nat<N>>() implements Nat<S<N>> {}
+  }
+
+  @TypeClass
+  public interface ReifyNat<N extends Nat<N>> {
+    int reify();
+
+    @TypeClass.Witness
+    static ReifyNat<Z> reifyZ() {
+      return () -> 0;
+    }
+
+    @TypeClass.Witness
+    static <N extends Nat<N>> ReifyNat<S<N>> reifyS(ReifyNat<N> rn) {
+      return () -> 1 + rn.reify();
+    }
+  }
+
+  @TypeClass
+  public interface NatAdd<A, B, @Out C> {
+    Unit trivial();
+
+    @TypeClass.Witness
+    static <B extends Nat<B>> NatAdd<Z, B, B> addZ() {
+      return Unit::unit;
+    }
+
+    @TypeClass.Witness
+    static <A extends Nat<A>, B extends Nat<B>, C extends Nat<C>> NatAdd<S<A>, B, S<C>> addS(
+        NatAdd<A, B, C> prev) {
+      return Unit::unit;
+    }
+  }
+
+  @TypeClass
+  public interface ReifyNatAdd<A, B> {
+    int reify();
+
+    @TypeClass.Witness
+    static <A extends Nat<A>, B extends Nat<B>, C extends Nat<C>> ReifyNatAdd<A, B> reifyAddS(
+        NatAdd<A, B, C> addAB, ReifyNat<C> reifyC) {
+      return reifyC::reify;
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/examples/Example6.java b/core/src/test/java/com/garciat/typeclasses/examples/Example6.java
new file mode 100644
index 0000000..519a940
--- /dev/null
+++ b/core/src/test/java/com/garciat/typeclasses/examples/Example6.java
@@ -0,0 +1,132 @@
+package com.garciat.typeclasses.examples;
+
+import static com.garciat.typeclasses.TypeClasses.witness;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import com.garciat.typeclasses.api.Out;
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.api.TypeClass;
+import com.garciat.typeclasses.impl.utils.Unit;
+import org.junit.jupiter.api.Test;
+
+public class Example6 {
+  @Test
+  void test1() {
+    var expr = new Expr.Add<>(new Expr.Int(1), new Expr.Add<>(new Expr.Int(2), new Expr.Int(3)));
+
+    boolean result = ReifiedContainsVoid.containsVoid(witness(new Ty<>() {}), expr);
+
+    assertThat(result).isFalse();
+  }
+
+  @Test
+  void test2() {
+    var expr = new Expr.Add<>(new Expr.Int(1), new Expr.Add<>(new Expr.Void(), new Expr.Int(3)));
+
+    boolean result = ReifiedContainsVoid.containsVoid(witness(new Ty<>() {}), expr);
+
+    assertThat(result).isTrue();
+  }
+
+  public sealed interface Fact {
+    record True() implements Fact {}
+
+    record False() implements Fact {}
+  }
+
+  @TypeClass
+  public interface FactOr<A, B, @Out R> {
+    Unit trivial();
+
+    @TypeClass.Witness(overlap = TypeClass.Witness.Overlap.OVERLAPPING)
+    static FactOr<Fact.False, Fact.False, Fact.False> here() {
+      return Unit::unit;
+    }
+
+    @TypeClass.Witness
+    static <A, B> FactOr<A, B, Fact.True> notHere() {
+      return Unit::unit;
+    }
+  }
+
+  @TypeClass
+  public interface FactNot<B, @Out R> {
+    Unit trivial();
+
+    @TypeClass.Witness
+    static FactNot<Fact.True, Fact.False> factNotTrue() {
+      return Unit::unit;
+    }
+
+    @TypeClass.Witness
+    static FactNot<Fact.False, Fact.True> factNotFalse() {
+      return Unit::unit;
+    }
+  }
+
+  @TypeClass
+  public interface ReifiedFact<B> {
+    boolean reify();
+
+    @TypeClass.Witness
+    static ReifiedFact<Fact.True> reifiedTrue() {
+      return () -> true;
+    }
+
+    @TypeClass.Witness
+    static ReifiedFact<Fact.False> reifiedFalse() {
+      return () -> false;
+    }
+  }
+
+  public sealed interface Expr<T extends Expr<T>> {
+    record Void() implements Expr<Void> {}
+
+    record Int(int value) implements Expr<Int> {}
+
+    record Add<T1 extends Expr<T1>, T2 extends Expr<T2>>(Expr<T1> left, Expr<T2> right)
+        implements Expr<Add<T1, T2>> {}
+  }
+
+  @TypeClass
+  public interface ContainsVoid<E extends Expr<E>, @Out R> {
+    Unit trivial();
+
+    @TypeClass.Witness
+    static ContainsVoid<Expr.Void, Fact.True> here() {
+      return Unit::unit;
+    }
+
+    @TypeClass.Witness
+    static ContainsVoid<Expr.Int, Fact.False> notHereInt() {
+      return Unit::unit;
+    }
+
+    @TypeClass.Witness
+    static <
+            T1 extends Expr<T1>,
+            T2 extends Expr<T2>,
+            FL extends Fact,
+            FR extends Fact,
+            F extends Fact>
+        ContainsVoid<Expr.Add<T1, T2>, F> add(
+            ContainsVoid<T1, FL> left, ContainsVoid<T2, FR> right, FactOr<FL, FR, F> factOr) {
+      return Unit::unit;
+    }
+  }
+
+  @TypeClass
+  public interface ReifiedContainsVoid<E extends Expr<E>> {
+    boolean reify();
+
+    static <E extends Expr<E>> boolean containsVoid(ReifiedContainsVoid<E> containsVoid, E ignore) {
+      return containsVoid.reify();
+    }
+
+    @TypeClass.Witness
+    static <E extends Expr<E>, F> ReifiedContainsVoid<E> reifiedHere(
+        ContainsVoid<E, F> here, ReifiedFact<F> fact) {
+      return fact::reify;
+    }
+  }
+}
diff --git a/core/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionCheckerTest.java b/core/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionCheckerTest.java
index 0a04c98..8db23b2 100644
--- a/core/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionCheckerTest.java
+++ b/core/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionCheckerTest.java
@@ -20,7 +20,15 @@ public class WitnessResolutionCheckerTest {
   @Nullable @TempDir Path tempDir;
 
   @ParameterizedTest
-  @ValueSource(strings = {"Example1.java", "Example2.java"})
+  @ValueSource(
+      strings = {
+        "Example1.java",
+        "Example2.java",
+        "Example3.java",
+        "Example4.java",
+        "Example5.java",
+        "Example6.java",
+      })
   public void checkExample(String fileName) throws IOException {
     requireNonNull(tempDir);
 
@@ -34,7 +42,7 @@ public void checkExample(String fileName) throws IOException {
     fileManager.setLocation(StandardLocation.SOURCE_OUTPUT, List.of(tempDir.toFile()));
 
     var files = new java.util.ArrayList<File>();
-    files.add(new File("src/test/java/com/garciat/typeclasses/processor/examples/" + fileName));
+    files.add(new File("src/test/java/com/garciat/typeclasses/examples/" + fileName));
 
     var compilationUnits = fileManager.getJavaFileObjectsFromFiles(files);
 
diff --git a/core/src/test/java/com/garciat/typeclasses/processor/examples/Example1.java b/core/src/test/java/com/garciat/typeclasses/processor/examples/Example1.java
deleted file mode 100644
index 4c29c65..0000000
--- a/core/src/test/java/com/garciat/typeclasses/processor/examples/Example1.java
+++ /dev/null
@@ -1,44 +0,0 @@
-package com.garciat.typeclasses.processor.examples;
-
-import static com.garciat.typeclasses.TypeClasses.witness;
-
-import com.garciat.typeclasses.api.Ty;
-import com.garciat.typeclasses.api.TypeClass;
-import java.util.List;
-import java.util.stream.Collectors;
-
-@TypeClass
-interface Show<T> {
-  String show(T value);
-
-  static <T> String show(Show<T> showT, T value) {
-    return showT.show(value);
-  }
-
-  @TypeClass.Witness
-  static Show<Integer> integerShow() {
-    return i -> Integer.toString(i);
-  }
-
-  @TypeClass.Witness
-  static <A> Show<List<A>> listShow(Show<A> showA) {
-    return listA -> listA.stream().map(showA::show).collect(Collectors.joining(", ", "[", "]"));
-  }
-}
-
-record Pair<A, B>(A first, B second) {
-  @TypeClass.Witness
-  public static <A, B> Show<Pair<A, B>> pairShow(Show<A> showA, Show<B> showB) {
-    return pair -> "(" + showA.show(pair.first()) + ", " + showB.show(pair.second()) + ")";
-  }
-}
-
-public class Example1 {
-  void main() {
-    Pair<Integer, List<Integer>> value = new Pair<>(1, List.of(2, 3, 4));
-
-    String s = Show.show(witness(new Ty<>() {}), value);
-
-    System.out.println(s);
-  }
-}
diff --git a/core/src/test/java/com/garciat/typeclasses/processor/examples/Example2.java b/core/src/test/java/com/garciat/typeclasses/processor/examples/Example2.java
deleted file mode 100644
index 2eeda7e..0000000
--- a/core/src/test/java/com/garciat/typeclasses/processor/examples/Example2.java
+++ /dev/null
@@ -1,45 +0,0 @@
-package com.garciat.typeclasses.processor.examples;
-
-import static com.garciat.typeclasses.TypeClasses.witness;
-
-import com.garciat.typeclasses.api.Ty;
-import com.garciat.typeclasses.api.TypeClass;
-import com.garciat.typeclasses.processor.examples.TList.TCons;
-import com.garciat.typeclasses.processor.examples.TList.TNil;
-
-interface TList<T extends TList<T>> {
-  record TNil() implements TList<TNil> {}
-
-  record TCons<T, TS extends TList<TS>>() implements TList<TCons<T, TS>> {}
-}
-
-@TypeClass
-interface In<TS extends TList<TS>, Y> {
-  @TypeClass.Witness
-  static <X, XS extends TList<XS>> In<TCons<X, XS>, X> here() {
-    return new In<>() {};
-  }
-
-  @TypeClass.Witness(overlap = TypeClass.Witness.Overlap.OVERLAPPABLE)
-  static <X, XS extends TList<XS>, Y> In<TCons<X, XS>, Y> there(In<XS, Y> there) {
-    return new In<>() {};
-  }
-}
-
-/// Based on:
-///
-/// ```haskell
-/// class In (xs :: [k]) (x :: k)
-///
-/// instance In (x ': xs) x
-///
-/// instance {-# OVERLAPPABLE #-} In xs y => In (x ': xs) y
-///
-/// example :: In '[Int, Bool, Char] Bool => ()
-/// example = ()
-/// ```
-public class Example2 {
-  void main() {
-    In<TCons<Byte, TCons<Short, TCons<Integer, TNil>>>, Short> _ = witness(new Ty<>() {});
-  }
-}