diff --git a/pom.xml b/pom.xml
index b6bd176..b7534dd 100644
--- a/pom.xml
+++ b/pom.xml
@@ -92,7 +92,7 @@
         <plugin>
           <groupId>org.jacoco</groupId>
           <artifactId>jacoco-maven-plugin</artifactId>
-          <version>0.8.12</version>
+          <version>0.8.14</version>
           <executions>
             <execution>
               <goals>
diff --git a/src/main/java/com/garciat/typeclasses/processor/OverlappingInstances.java b/src/main/java/com/garciat/typeclasses/processor/OverlappingInstances.java
new file mode 100644
index 0000000..acb0cbb
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/OverlappingInstances.java
@@ -0,0 +1,35 @@
+package com.garciat.typeclasses.processor;
+
+import static com.garciat.typeclasses.api.TypeClass.Witness.Overlap.OVERLAPPABLE;
+import static com.garciat.typeclasses.api.TypeClass.Witness.Overlap.OVERLAPPING;
+
+import java.util.List;
+
+public final class OverlappingInstances {
+  private OverlappingInstances() {}
+
+  /**
+   * @implSpec <a href=
+   *     "https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/instances.html#overlapping-instances">6.8.8.5.
+   *     Overlapping instances</a>
+   */
+  public static List<WitnessConstructor> reduce(List<WitnessConstructor> candidates) {
+    return candidates.stream()
+        .filter(
+            iX ->
+                candidates.stream().filter(iY -> iX != iY).noneMatch(iY -> isOverlappedBy(iX, iY)))
+        .toList();
+  }
+
+  private static boolean isOverlappedBy(WitnessConstructor iX, WitnessConstructor iY) {
+    return (iX.overlap() == OVERLAPPABLE || iY.overlap() == OVERLAPPING)
+        && isSubstitutionInstance(iX, iY)
+        && !isSubstitutionInstance(iY, iX);
+  }
+
+  private static boolean isSubstitutionInstance(
+      WitnessConstructor base, WitnessConstructor reference) {
+    return Unification.unify(base.returnType(), reference.returnType())
+        .fold(() -> false, map -> !map.isEmpty());
+  }
+}
diff --git a/src/main/java/com/garciat/typeclasses/processor/ParsedType.java b/src/main/java/com/garciat/typeclasses/processor/ParsedType.java
new file mode 100644
index 0000000..57bc210
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/ParsedType.java
@@ -0,0 +1,34 @@
+package com.garciat.typeclasses.processor;
+
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.PrimitiveType;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.type.TypeVariable;
+
+public sealed interface ParsedType {
+  record Var(TypeVariable java) implements ParsedType {}
+
+  record App(ParsedType fun, ParsedType arg) implements ParsedType {}
+
+  record ArrayOf(ParsedType elementType) implements ParsedType {}
+
+  record Const(DeclaredType java) implements ParsedType {}
+
+  record Primitive(PrimitiveType java) implements ParsedType {}
+
+  default String format() {
+    return switch (this) {
+      case Var v -> v.java.toString();
+      case Const c ->
+          c.java().asElement().getSimpleName()
+              + c.java().getTypeArguments().stream()
+                  .map(TypeMirror::toString)
+                  .reduce((a, b) -> a + ", " + b)
+                  .map(s -> "[" + s + "]")
+                  .orElse("");
+      case App a -> a.fun.format() + "(" + a.arg.format() + ")";
+      case ArrayOf a -> a.elementType.format() + "[]";
+      case Primitive p -> p.java().toString();
+    };
+  }
+}
diff --git a/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java b/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java
new file mode 100644
index 0000000..8bfe4ee
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/StaticWitnessSystem.java
@@ -0,0 +1,118 @@
+package com.garciat.typeclasses.processor;
+
+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.utils.Lists;
+import com.garciat.typeclasses.types.Maybe;
+import com.garciat.typeclasses.types.Pair;
+import java.util.List;
+import java.util.function.Function;
+import java.util.stream.Stream;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Modifier;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.type.*;
+
+public class StaticWitnessSystem {
+  private static final Class<?> TAG_BASE_CLASS = TagBase.class;
+  private static final Class<?> TAPP_CLASS = TApp.class;
+  private static final Class<?> TPAR_CLASS = TPar.class;
+
+  public StaticWitnessSystem() {}
+
+  public List<WitnessConstructor> findRules(ParsedType target) {
+    return switch (target) {
+      case ParsedType.App(var fun, var arg) -> Lists.concat(findRules(fun), findRules(arg));
+      case ParsedType.Const(var java) ->
+          java.asElement().getEnclosedElements().stream()
+              .flatMap(isInstanceOf(ExecutableElement.class))
+              .flatMap(method -> parseWitnessConstructor(method).stream())
+              .toList();
+      case ParsedType.Var(var ignore) -> List.of();
+      case ParsedType.ArrayOf(var ignore) -> List.of();
+      case ParsedType.Primitive(var ignore) -> List.of();
+    };
+  }
+
+  private Maybe<WitnessConstructor> parseWitnessConstructor(ExecutableElement method) {
+    if (method.getModifiers().contains(Modifier.PUBLIC)
+        && method.getModifiers().contains(Modifier.STATIC)
+        && method.getAnnotation(TypeClass.Witness.class) instanceof TypeClass.Witness witnessAnn) {
+      return Maybe.just(
+          new WitnessConstructor(
+              method,
+              witnessAnn.overlap(),
+              method.getParameters().stream()
+                  .map(VariableElement::asType)
+                  .map(this::parse)
+                  .toList(),
+              parse(method.getReturnType())));
+
+    } else {
+      return Maybe.nothing();
+    }
+  }
+
+  public ParsedType parse(TypeMirror type) {
+    return switch (type) {
+      case TypeVariable tv -> new ParsedType.Var(tv);
+      case ArrayType at -> new ParsedType.ArrayOf(parse(at.getComponentType()));
+      // Store primitive as its boxed type representation, just to have a DeclaredType.
+      case PrimitiveType pt -> new ParsedType.Primitive(pt);
+      case DeclaredType dt
+          when parseTagType(dt) instanceof Maybe.Just<DeclaredType>(var realType) ->
+          new ParsedType.Const(realType);
+      case DeclaredType dt when dt.getTypeArguments().isEmpty() -> new ParsedType.Const(dt);
+      case DeclaredType dt
+          when parseAppType(dt)
+              instanceof
+              Maybe.Just<Pair<TypeMirror, TypeMirror>>(
+                  Pair<TypeMirror, TypeMirror>(var fun, var arg)) ->
+          new ParsedType.App(parse(fun), parse(arg));
+      case DeclaredType dt ->
+          dt.getTypeArguments().stream()
+              .map(this::parse)
+              .reduce(new ParsedType.Const(erasure(dt)), ParsedType.App::new);
+      case WildcardType wt ->
+          throw new IllegalArgumentException("Cannot parse wildcard type: " + wt);
+      default -> throw new IllegalArgumentException("Unsupported type: " + type);
+    };
+  }
+
+  private static Maybe<DeclaredType> parseTagType(DeclaredType t) {
+    if (t.asElement() instanceof TypeElement tag
+        && tag.getEnclosingElement() instanceof TypeElement enclosing
+        && enclosing.asType() instanceof DeclaredType enclosingType
+        && tag.getSuperclass() instanceof DeclaredType tagSuperType
+        && tagSuperType.asElement() instanceof TypeElement tagSuper
+        && tagSuper.getQualifiedName().contentEquals(TAG_BASE_CLASS.getName())) {
+      return Maybe.just(enclosingType);
+    } else {
+      return Maybe.nothing();
+    }
+  }
+
+  private Maybe<Pair<TypeMirror, TypeMirror>> parseAppType(DeclaredType t) {
+    return t.getTypeArguments().size() == 2 && isAppType(erasure(t))
+        ? Maybe.just(new Pair<>(t.getTypeArguments().get(0), t.getTypeArguments().get(1)))
+        : Maybe.nothing();
+  }
+
+  private boolean isAppType(TypeMirror erasure) {
+    return erasure instanceof DeclaredType dt
+        && dt.asElement() instanceof TypeElement te
+        && (te.getQualifiedName().contentEquals(TAPP_CLASS.getName())
+            || te.getQualifiedName().contentEquals(TPAR_CLASS.getName()));
+  }
+
+  private DeclaredType erasure(DeclaredType t) {
+    return t.asElement().asType() instanceof DeclaredType typeCtor ? typeCtor : t;
+  }
+
+  private static <T extends U, U> Function<U, Stream<T>> isInstanceOf(Class<T> cls) {
+    return u -> cls.isInstance(u) ? Stream.of(cls.cast(u)) : Stream.empty();
+  }
+}
diff --git a/src/main/java/com/garciat/typeclasses/processor/Unification.java b/src/main/java/com/garciat/typeclasses/processor/Unification.java
new file mode 100644
index 0000000..e340617
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/Unification.java
@@ -0,0 +1,52 @@
+package com.garciat.typeclasses.processor;
+
+import com.garciat.typeclasses.impl.utils.Maps;
+import com.garciat.typeclasses.types.Maybe;
+import com.garciat.typeclasses.types.Pair;
+import java.util.List;
+import java.util.Map;
+
+public final class Unification {
+  private Unification() {}
+
+  public static Maybe<Map<ParsedType.Var, ParsedType>> unify(ParsedType t1, ParsedType t2) {
+    return switch (Pair.of(t1, t2)) {
+      case Pair<ParsedType, ParsedType>(ParsedType.Var var1, ParsedType.Primitive p) ->
+          Maybe.nothing(); // no primitives in generics
+      case Pair<ParsedType, ParsedType>(ParsedType.Var var1, var t) -> Maybe.just(Map.of(var1, t));
+      case Pair<ParsedType, ParsedType>(ParsedType.Const const1, ParsedType.Const const2)
+          when const1.equals(const2) ->
+          Maybe.just(Map.of());
+      case Pair<ParsedType, ParsedType>(
+              ParsedType.App(var fun1, var arg1),
+              ParsedType.App(var fun2, var arg2)) ->
+          Maybe.apply(Maps::merge, unify(fun1, fun2), unify(arg1, arg2));
+      case Pair<ParsedType, ParsedType>(
+              ParsedType.ArrayOf(var elem1),
+              ParsedType.ArrayOf(var elem2)) ->
+          unify(elem1, elem2);
+      case Pair<ParsedType, ParsedType>(
+              ParsedType.Primitive(var prim1),
+              ParsedType.Primitive(var prim2))
+          when prim1.equals(prim2) ->
+          Maybe.just(Map.of());
+      default -> Maybe.nothing();
+    };
+  }
+
+  public static ParsedType substitute(Map<ParsedType.Var, ParsedType> map, ParsedType type) {
+    return switch (type) {
+      case ParsedType.Var var -> map.getOrDefault(var, var);
+      case ParsedType.App(var fun, var arg) ->
+          new ParsedType.App(substitute(map, fun), substitute(map, arg));
+      case ParsedType.ArrayOf var -> new ParsedType.ArrayOf(substitute(map, var.elementType()));
+      case ParsedType.Primitive p -> p;
+      case ParsedType.Const c -> c;
+    };
+  }
+
+  public static List<ParsedType> substituteAll(
+      Map<ParsedType.Var, ParsedType> map, List<ParsedType> types) {
+    return types.stream().map(t -> substitute(map, t)).toList();
+  }
+}
diff --git a/src/main/java/com/garciat/typeclasses/processor/WitnessConstructor.java b/src/main/java/com/garciat/typeclasses/processor/WitnessConstructor.java
new file mode 100644
index 0000000..d89d7ba
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/WitnessConstructor.java
@@ -0,0 +1,11 @@
+package com.garciat.typeclasses.processor;
+
+import com.garciat.typeclasses.api.TypeClass;
+import java.util.List;
+import javax.lang.model.element.ExecutableElement;
+
+public record WitnessConstructor(
+    ExecutableElement method,
+    TypeClass.Witness.Overlap overlap,
+    List<ParsedType> paramTypes,
+    ParsedType returnType) {}
diff --git a/src/main/java/com/garciat/typeclasses/processor/WitnessResolution.java b/src/main/java/com/garciat/typeclasses/processor/WitnessResolution.java
new file mode 100644
index 0000000..d5a5dd0
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/WitnessResolution.java
@@ -0,0 +1,78 @@
+package com.garciat.typeclasses.processor;
+
+import com.garciat.typeclasses.impl.utils.ZeroOneMore;
+import com.garciat.typeclasses.types.Either;
+import com.garciat.typeclasses.types.Maybe;
+import java.util.List;
+import java.util.stream.Collectors;
+
+public final class WitnessResolution {
+  private WitnessResolution() {}
+
+  /** Resolves a ParsedType into an InstantiationPlan. */
+  public static Either<ResolutionError, InstantiationPlan> resolve(
+      StaticWitnessSystem system, ParsedType target) {
+
+    List<Match> matches =
+        OverlappingInstances.reduce(system.findRules(target)).stream()
+            .flatMap(rule -> tryMatch(rule, target).stream())
+            .toList();
+
+    return switch (ZeroOneMore.of(matches)) {
+      case ZeroOneMore.One<Match>(Match(var rule, var requirements)) ->
+          Either.traverse(requirements, req -> resolve(system, req))
+              .<InstantiationPlan>map(
+                  dependencies -> new InstantiationPlan.PlanStep(rule, dependencies))
+              .mapLeft(error -> new ResolutionError.Nested(target, error));
+      case ZeroOneMore.Zero<Match>() -> Either.left(new ResolutionError.NotFound(target));
+      case ZeroOneMore.More<Match>(var matches2) ->
+          Either.left(
+              new ResolutionError.Ambiguous(target, matches2.stream().map(Match::rule).toList()));
+    };
+  }
+
+  private static Maybe<Match> tryMatch(WitnessConstructor rule, ParsedType target) {
+    return Unification.unify(rule.returnType(), target)
+        .map(map -> Unification.substituteAll(map, rule.paramTypes()))
+        .map(requirements -> new Match(rule, requirements));
+  }
+
+  record Match(WitnessConstructor rule, List<ParsedType> requirements) {}
+
+  /**
+   * Represents the fully resolved instantiation plan. This is a tree structure where each node is a
+   * step in the instantiation process, with dependencies on other steps.
+   */
+  public sealed interface InstantiationPlan {
+    record PlanStep(WitnessConstructor target, List<InstantiationPlan> dependencies)
+        implements InstantiationPlan {}
+  }
+
+  public sealed interface ResolutionError {
+    record NotFound(ParsedType target) implements ResolutionError {}
+
+    record Ambiguous(ParsedType target, List<WitnessConstructor> candidates)
+        implements ResolutionError {}
+
+    record Nested(ParsedType target, ResolutionError cause) implements ResolutionError {}
+
+    default String format() {
+      return switch (this) {
+        case NotFound(ParsedType target) -> "No witness found for type: " + target.format();
+        case Ambiguous(ParsedType target, List<WitnessConstructor> candidates) ->
+            "Ambiguous witnesses found for type: "
+                + target.format()
+                + "\nCandidates:\n"
+                + candidates.stream()
+                    .map(WitnessConstructor::toString)
+                    .collect(Collectors.joining("\n"))
+                    .indent(2);
+        case Nested(ParsedType target, ResolutionError cause) ->
+            "While resolving witness for type: "
+                + target.format()
+                + "\nCaused by: "
+                + cause.format().indent(2);
+      };
+    }
+  }
+}
diff --git a/src/main/java/com/garciat/typeclasses/processor/WitnessResolutionChecker.java b/src/main/java/com/garciat/typeclasses/processor/WitnessResolutionChecker.java
new file mode 100644
index 0000000..a367f43
--- /dev/null
+++ b/src/main/java/com/garciat/typeclasses/processor/WitnessResolutionChecker.java
@@ -0,0 +1,238 @@
+package com.garciat.typeclasses.processor;
+
+import static com.garciat.typeclasses.types.Unit.unit;
+
+import com.garciat.typeclasses.TypeClasses;
+import com.garciat.typeclasses.api.Ty;
+import com.garciat.typeclasses.types.Maybe;
+import com.garciat.typeclasses.types.Unit;
+import com.sun.source.tree.ClassTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.NewClassTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.util.JavacTask;
+import com.sun.source.util.Plugin;
+import com.sun.source.util.TaskEvent;
+import com.sun.source.util.TaskListener;
+import com.sun.source.util.TreePath;
+import com.sun.source.util.TreePathScanner;
+import com.sun.source.util.Trees;
+import java.lang.reflect.Method;
+import java.util.List;
+import java.util.Objects;
+import java.util.function.Function;
+import java.util.function.Predicate;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeMirror;
+import javax.tools.Diagnostic;
+
+public final class WitnessResolutionChecker implements Plugin {
+  private static final Method WITNESS_METHOD;
+
+  static {
+    try {
+      WITNESS_METHOD = TypeClasses.class.getMethod("witness", Ty.class);
+    } catch (NoSuchMethodException e) {
+      throw new RuntimeException(e);
+    }
+  }
+
+  @Override
+  public String getName() {
+    return "WitnessResolutionChecker";
+  }
+
+  @Override
+  public void init(JavacTask task, String... args) {
+    task.addTaskListener(
+        new TaskListener() {
+          @Override
+          public void finished(TaskEvent e) {
+            if (e.getKind() != TaskEvent.Kind.ANALYZE) {
+              return;
+            }
+
+            if (e.getCompilationUnit() == null) {
+              return;
+            }
+
+            new WitnessCallScanner(Trees.instance(task)).scan(e.getCompilationUnit(), null);
+          }
+        });
+  }
+
+  /** Scanner that finds calls to TypeClasses.witness() and validates them. */
+  private static class WitnessCallScanner extends TreePathScanner<Void, Void> {
+    private final Trees trees;
+    private final StaticWitnessSystem system;
+
+    private WitnessCallScanner(Trees trees) {
+      this.trees = trees;
+      this.system = new StaticWitnessSystem();
+    }
+
+    @Override
+    public Void visitMethodInvocation(MethodInvocationTree node, Void arg) {
+      Parser.<MethodInvocationTree>identity()
+          .guard(
+              Parser.<MethodInvocationTree>currentElement()
+                  .flatMap(Parser.methodMatches(WITNESS_METHOD)))
+          .flatMap(Parser.unaryCallArgument())
+          .flatMap(Parser.newAnonymousClassBody())
+          .flatMap(Parser.singleImplementsClause())
+          .flatMap(Parser.treeTypeMirror())
+          .flatMap(Parser.rawTypeMatches(Ty.class))
+          .flatMap(Parser.unaryTypeArgument())
+          .parse(trees, getCurrentPath(), node)
+          .fold(
+              Unit::unit,
+              witnessType ->
+                  WitnessResolution.resolve(system, system.parse(witnessType))
+                      .fold(
+                          error -> {
+                            this.trees.printMessage(
+                                Diagnostic.Kind.ERROR,
+                                "Failed to resolve witness for type: "
+                                    + witnessType
+                                    + "\nReason: "
+                                    + error.format(),
+                                getCurrentPath().getLeaf(),
+                                getCurrentPath().getCompilationUnit());
+                            return unit();
+                          },
+                          plan -> unit()));
+
+      return super.visitMethodInvocation(node, arg);
+    }
+  }
+}
+
+interface Parser<T, R> {
+  Maybe<R> parse(Trees trees, TreePath current, T input);
+
+  default <S> Parser<T, S> flatMap(Parser<R, S> next) {
+    return (trees, current, input) ->
+        this.parse(trees, current, input).flatMap(r -> next.parse(trees, current, r));
+  }
+
+  default <S> Parser<T, S> map(Function<R, S> mapper) {
+    return flatMap(mapping(mapper));
+  }
+
+  default Parser<T, R> filter(Predicate<R> predicate) {
+    return flatMap(filtering(predicate));
+  }
+
+  default Parser<T, R> guard(Parser<R, ?> predicate) {
+    return (trees, current, input) ->
+        this.parse(trees, current, input)
+            .flatMap(r -> predicate.parse(trees, current, r).map(x -> r));
+  }
+
+  static <T> Parser<T, T> identity() {
+    return (trees, current, input) -> Maybe.just(input);
+  }
+
+  static <T, R> Parser<T, R> mapping(Function<T, R> mapper) {
+    return (trees, current, input) -> Maybe.just(mapper.apply(input));
+  }
+
+  static <T> Parser<T, T> filtering(Predicate<T> predicate) {
+    return (trees, current, input) -> {
+      if (predicate.test(input)) {
+        return Maybe.just(input);
+      } else {
+        return Maybe.nothing();
+      }
+    };
+  }
+
+  static <T> Parser<T, T> notNull() {
+    return filtering(Objects::nonNull);
+  }
+
+  static <T, R extends T> Parser<T, R> as(Class<R> cls) {
+    return (trees, current, input) -> {
+      if (cls.isInstance(input)) {
+        return Maybe.just(cls.cast(input));
+      } else {
+        return Maybe.nothing();
+      }
+    };
+  }
+
+  static <A> Parser<A, Element> currentElement() {
+    return (trees, current, input) -> {
+      Element element = trees.getElement(current);
+      if (element != null) {
+        return Maybe.just(element);
+      } else {
+        return Maybe.nothing();
+      }
+    };
+  }
+
+  static Parser<Element, ExecutableElement> methodMatches(Method target) {
+    return Parser.<Element, ExecutableElement>as(ExecutableElement.class)
+        .filter(m -> m.getSimpleName().contentEquals(target.getName()))
+        .guard(
+            mapping(ExecutableElement::getEnclosingElement)
+                .flatMap(as(TypeElement.class))
+                .map(TypeElement::getQualifiedName)
+                .filter(name -> name.contentEquals(target.getDeclaringClass().getName())));
+  }
+
+  static Parser<MethodInvocationTree, ExpressionTree> unaryCallArgument() {
+    return mapping(MethodInvocationTree::getArguments)
+        .filter(list -> list.size() == 1)
+        .map(List::getFirst);
+  }
+
+  static Parser<ExpressionTree, ClassTree> newAnonymousClassBody() {
+    return Parser.<ExpressionTree, NewClassTree>as(NewClassTree.class)
+        .map(NewClassTree::getClassBody)
+        .flatMap(notNull());
+  }
+
+  static Parser<ClassTree, Tree> singleImplementsClause() {
+    return mapping(ClassTree::getImplementsClause)
+        .flatMap(notNull())
+        .filter(list -> list.size() == 1)
+        .map(List::getFirst);
+  }
+
+  static Parser<Tree, TypeMirror> treeTypeMirror() {
+    return (trees, current, input) -> {
+      try {
+        TypeMirror typeMirror =
+            trees.getTypeMirror(trees.getPath(current.getCompilationUnit(), input));
+        return Maybe.just(typeMirror);
+      } catch (IllegalArgumentException e) {
+        return Maybe.nothing();
+      }
+    };
+  }
+
+  static Parser<TypeMirror, DeclaredType> rawTypeMatches(Class<?> cls) {
+    return Parser.<TypeMirror, DeclaredType>as(DeclaredType.class)
+        .guard(
+            declaredTypeElement()
+                .flatMap(as(TypeElement.class))
+                .map(TypeElement::getQualifiedName)
+                .filter(name -> name.contentEquals(cls.getName())));
+  }
+
+  static Parser<DeclaredType, TypeMirror> unaryTypeArgument() {
+    return mapping(DeclaredType::getTypeArguments)
+        .filter(list -> list.size() == 1)
+        .map(List::getFirst);
+  }
+
+  static Parser<DeclaredType, Element> declaredTypeElement() {
+    return mapping(DeclaredType::asElement).flatMap(notNull());
+  }
+}
diff --git a/src/main/resources/META-INF/services/com.sun.source.util.Plugin b/src/main/resources/META-INF/services/com.sun.source.util.Plugin
new file mode 100644
index 0000000..ae61afe
--- /dev/null
+++ b/src/main/resources/META-INF/services/com.sun.source.util.Plugin
@@ -0,0 +1 @@
+com.garciat.typeclasses.processor.WitnessResolutionChecker
\ No newline at end of file
diff --git a/src/test/java/com/garciat/typeclasses/ExamplesTest.java b/src/test/java/com/garciat/typeclasses/ExamplesTest.java
index 1addc77..353ef6e 100644
--- a/src/test/java/com/garciat/typeclasses/ExamplesTest.java
+++ b/src/test/java/com/garciat/typeclasses/ExamplesTest.java
@@ -3,8 +3,21 @@
 import static com.garciat.typeclasses.TypeClasses.witness;
 
 import com.garciat.typeclasses.api.Ty;
-import com.garciat.typeclasses.classes.*;
-import com.garciat.typeclasses.types.*;
+import com.garciat.typeclasses.classes.Arbitrary;
+import com.garciat.typeclasses.classes.Eq;
+import com.garciat.typeclasses.classes.Foldable;
+import com.garciat.typeclasses.classes.Monoid;
+import com.garciat.typeclasses.classes.Ord;
+import com.garciat.typeclasses.classes.PrintAll;
+import com.garciat.typeclasses.classes.Show;
+import com.garciat.typeclasses.classes.SumAllInt;
+import com.garciat.typeclasses.classes.Traversable;
+import com.garciat.typeclasses.types.F3;
+import com.garciat.typeclasses.types.FwdList;
+import com.garciat.typeclasses.types.JavaList;
+import com.garciat.typeclasses.types.Maybe;
+import com.garciat.typeclasses.types.Sum;
+import com.garciat.typeclasses.types.Unit;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
diff --git a/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionProcessorTest.java b/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionProcessorTest.java
new file mode 100644
index 0000000..3569d6c
--- /dev/null
+++ b/src/test/java/com/garciat/typeclasses/processor/WitnessResolutionProcessorTest.java
@@ -0,0 +1,71 @@
+package com.garciat.typeclasses.processor;
+
+import static java.util.Objects.requireNonNull;
+import static org.assertj.core.api.Assertions.assertThat;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.FileVisitResult;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.SimpleFileVisitor;
+import java.nio.file.attribute.BasicFileAttributes;
+import java.util.List;
+import javax.tools.DiagnosticCollector;
+import javax.tools.JavaFileObject;
+import javax.tools.StandardLocation;
+import javax.tools.ToolProvider;
+import org.jspecify.annotations.Nullable;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.io.TempDir;
+
+public class WitnessResolutionProcessorTest {
+  @Nullable @TempDir Path tempDir;
+
+  @Test
+  public void test() throws IOException {
+    requireNonNull(tempDir);
+
+    // Given
+    var compiler = ToolProvider.getSystemJavaCompiler();
+
+    var diagnostics = new DiagnosticCollector<JavaFileObject>();
+
+    var fileManager = compiler.getStandardFileManager(diagnostics, null, null);
+    fileManager.setLocation(StandardLocation.CLASS_OUTPUT, List.of(tempDir.toFile()));
+    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/ExamplesTest.java"));
+
+    Files.walkFileTree(
+        Path.of("src/main/java"),
+        new SimpleFileVisitor<>() {
+          @Override
+          public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) {
+            if (file.toString().endsWith(".java")) {
+              files.add(file.toFile());
+            }
+            return FileVisitResult.CONTINUE;
+          }
+        });
+
+    var compilationUnits = fileManager.getJavaFileObjectsFromFiles(files);
+
+    var task =
+        compiler.getTask(
+            null,
+            fileManager,
+            diagnostics,
+            List.of("-Xplugin:WitnessResolutionChecker"),
+            null,
+            compilationUnits);
+
+    // When
+    boolean success = task.call();
+
+    // Then
+    assertThat(diagnostics.getDiagnostics()).isEmpty();
+    assertThat(success).isTrue();
+  }
+}