diff --git a/examples/dummy_project/Orchid.toml b/examples/dummy_project/Orchid.toml
deleted file mode 100644
index 130321a..0000000
--- a/examples/dummy_project/Orchid.toml
+++ /dev/null
@@ -1,5 +0,0 @@
-[[target]]
-name = 'Dummy Project'
-type = 'executable'
-
-[target.dependencies]
diff --git a/examples/dummy_project/main.orc b/examples/dummy_project/main.orc
index 5e90275..d85fa6e 100644
--- a/examples/dummy_project/main.orc
+++ b/examples/dummy_project/main.orc
@@ -9,7 +9,6 @@ define Zippable $C:(type -> type) as @:Mappable $C. (
   @T. @U. @V. (T -> U -> V) -> $C T -> $C U -> $C V
 )
 define Default $T:type as $T
--- Is the intersection of typeclasses an operation we need?
 
 --[ Type definition ]--
 define Cons $elem:type as loop \r. Option (Pair T $elem)
diff --git a/examples/vs_haskell/typeclasses.hs b/examples/vs_haskell/typeclasses.hs
new file mode 100644
index 0000000..5df9a2e
--- /dev/null
+++ b/examples/vs_haskell/typeclasses.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE BlockArguments #-}
+import Prelude((>>=), Maybe( Just, Nothing ), return, fmap)
+import Debug.Trace
+
+-- 1
+class Add l r o where
+  add :: l -> r -> o
+  (+) :: l -> r -> o
+  (+) = add
+
+-- 2
+class Mappable c where
+  map :: (i -> o) -> c i -> c o
+
+-- 3
+class Mappable c => Zippable c where
+  zip :: (l -> r -> o) -> c l -> c r -> c o
+
+
+-- 4
+class Default t where
+  def :: t
+
+-- 5
+instance (Zippable c, Add l r o)
+  => Add (c l) (c r) (c o) where
+  add :: (Zippable c, Add l r o) => c l -> c r -> c o
+  add = zip add
+
+
+
+-- 6
+-- newtype List t = List (Maybe (t, List t))
+
+-- instance Mappable List where
+--   map :: (i -> o) -> List i -> List o
+--   map f (List o) = List (fmap (\(h, t) -> (f h, map f t)) o)
+
+-- instance Zippable List where
+--   zip :: (l -> r -> o) -> List l -> List r -> List o
+--   zip f (List l) (List r) = List do
+--     (lh, lt) <- l
+--     (rh, rt) <- r
+--     return (f lh rh, zip f lt rt)
+
+-- instance Add (List e) (List e) (List e) where
+--   add (List l) (List r) = List case l of
+--     Just (head, tail) -> Just (head, add tail r)
+--     Nothing -> r
+
+data List t = Cons t (List t) | End
+
+instance Mappable List where
+  map :: (i -> o) -> List i -> List o
+  map _ End = End
+  map f (Cons head tail) = Cons (f head) (map f tail)
+
+instance Zippable List where
+  zip :: (l -> r -> o) -> List l -> List r -> List o
+  zip _ _ End = End
+  zip _ End _ = End
+  zip f (Cons lhead ltail) (Cons rhead rtail) =
+    Cons (f lhead rhead) (zip f ltail rtail)
+
+instance Add (List e) (List e) (List e) where
+  add End r = r
+  add (Cons head tail) r = Cons head (add tail r)
+
+  
\ No newline at end of file
diff --git a/examples/vs_haskell/typeclasses.orc b/examples/vs_haskell/typeclasses.orc
new file mode 100644
index 0000000..b690804
--- /dev/null
+++ b/examples/vs_haskell/typeclasses.orc
@@ -0,0 +1,65 @@
+
+
+
+
+
+
+
+-- 1
+define Add $L $R $O
+as $L -> $R -> $O
+
+$left:2... + $right:1... =1000=> add ($left...) ($right...)
+
+-- 2
+define Mappable $C:type -> type
+as @I. @O. (I -> O) -> $C I -> $C O
+
+-- 3
+define Zippable $C:type -> type
+as @:Mappable $C.
+  @L. @R. @O. (L -> R -> O) -> $C L -> $C R -> $C O
+
+-- 4
+define Default $T:type as $T
+
+
+-- 5
+impl
+  @C:Type -> Type. @L. @R. @O.
+  @:(Zippable C). @:(Add L R O).
+  Add (C L) (C R) (C O)
+by elementwiseAdd
+via zip add
+
+-- 6
+define List $E as Y \r. Option t[ $E, r ]
+
+impl Mappable List
+via \f.\list. categorise (
+  (Y \repeat. \opt. match opt {
+    Some t[head, tail] => 
+      Some t[f head, repeat tail];
+    None => None;
+  }) (generalise list)
+)
+
+impl Zippable List 
+via \f.\l.\r. categorise (
+  Y \repeat.\lopt.\ropt. do {
+    bind t[lhead, ltail] <- lopt;
+    bind t[rhead, rtail] <- ropt;
+    t[f lhead rhead, repeat ltail rtail]
+  }
+) (generalise l) (generalise r)
+
+impl @T. Add (List T) (List T) (List T)
+by concatListAdd over elementwiseAdd
+via \l.\r.categorise Y \repeat.\l. (
+  match l (
+    Some t[head, tail] =>
+      Some t[head, repeat tail];
+    None => (generalise r)
+  )
+) (generalise l)
+
diff --git a/src/executor/apply_lambda.rs b/src/executor/apply_lambda.rs
index bbf7bbd..6bc1190 100644
--- a/src/executor/apply_lambda.rs
+++ b/src/executor/apply_lambda.rs
@@ -1,53 +1,58 @@
+use itertools::Itertools;
 use mappable_rc::Mrc;
 
 use crate::utils::{collect_to_mrc, to_mrc_slice};
 
-use super::super::representations::typed::{Clause, Expr};
+use crate::representations::typed::{Clause, Expr};
 
-pub fn apply_lambda(id: u64, value: Mrc<Expr>, body: Mrc<Expr>) -> Mrc<Expr> {
-  apply_lambda_expr_rec(id, value, Mrc::clone(&body))
-    .unwrap_or(body)
+#[derive(Clone)]
+struct Application<'a> {
+  id: u64,
+  value: &'a Expr,
+  types: bool
 }
 
+// pub fn apply_lambda(app: Application, body: Expr) -> Expr {
+//   apply_lambda_expr_rec(id, value, body)
+//     .unwrap_or(body)
+// }
+
 fn apply_lambda_expr_rec(
-  id: u64, value: Mrc<Expr>, expr: Mrc<Expr>
-) -> Option<Mrc<Expr>> {
-  let Expr(clause, typ) = expr.as_ref();
+  app@Application{ id, types, value }: Application, expr: &Expr
+) -> Option<Expr> {
+  let Expr(clause, typ) = expr;
   match clause {
     Clause::LambdaArg(arg_id) | Clause::AutoArg(arg_id) if *arg_id == id => {
-      let full_typ = collect_to_mrc(
+      let full_typ = 
         value.1.iter()
         .chain(typ.iter())
-        .cloned()
-      );
-      Some(Mrc::new(Expr(value.0.to_owned(), full_typ)))
+        .cloned().collect_vec();
+      Some(Expr(value.0.to_owned(), full_typ))
     }
     cl => {
-      apply_lambda_clause_rec(id, value, cl.clone())
-        .map(|c| Mrc::new(Expr(c, Mrc::clone(typ))))
+      let new_cl = apply_lambda_clause_rec(app, cl);
+      let new_typ = if !types {None} else {
+        typ.
+      }
     }
   }
 }
 
 fn apply_lambda_clause_rec(
-  id: u64, value: Mrc<Expr>, clause: Clause
+  app: Application, clause: &Clause
 ) -> Option<Clause> {
   match clause {
     // Only element actually manipulated
-    Clause::LambdaArg(_) | Clause::AutoArg(_) => Some(clause),
+    Clause::LambdaArg(_) | Clause::AutoArg(_) => None,
     // Traverse, yield Some if either had changed.
     Clause::Apply(f, x) => {
-      let new_f = apply_lambda_expr_rec(
-        id, Mrc::clone(&value), Mrc::clone(&f)
-      );
-      let new_x = apply_lambda_expr_rec(
-        id, value, Mrc::clone(&x)
-      );
+      let new_f = apply_lambda_expr_rec(app, f.as_ref());
+      let new_x = apply_lambda_expr_rec(app, x.as_ref());
       match (new_f, new_x) { // Mind the shadows
         (None, None) => None,
-        (None, Some(x)) => Some(Clause::Apply(f, x)),
-        (Some(f), None) => Some(Clause::Apply(f, x)),
-        (Some(f), Some(x)) => Some(Clause::Apply(f, x))
+        (None, Some(x)) => Some(Clause::Apply(f.clone(), Box::new(x))),
+        (Some(f), None) => Some(Clause::Apply(Box::new(f), x.clone())),
+        (Some(f), Some(x)) => Some(Clause::Apply(Box::new(f), Box::new(x)))
       }
     },
     Clause::Lambda(own_id, t, b) => apply_lambda__traverse_param(id, value, own_id, t, b, Clause::Lambda),
diff --git a/src/executor/mod.rs b/src/executor/mod.rs
index bc76c6f..5430922 100644
--- a/src/executor/mod.rs
+++ b/src/executor/mod.rs
@@ -2,4 +2,5 @@ mod normalize;
 mod partial_hash;
 mod reduction_tree;
 mod apply_lambda;
+pub use apply_lambda::apply_lambda;
 mod syntax_eq;
\ No newline at end of file
diff --git a/src/representations/typed.rs b/src/representations/typed.rs
index bde1b24..7ccc3ce 100644
--- a/src/representations/typed.rs
+++ b/src/representations/typed.rs
@@ -1,28 +1,30 @@
 use mappable_rc::Mrc;
+use crate::executor::apply_lambda;
 use crate::foreign::{Atom, ExternFn};
 use crate::utils::{to_mrc_slice, one_mrc_slice};
 use crate::utils::string_from_charset;
 
-use super::{Literal, ast_to_typed};
+use super::get_name::get_name;
+use super::{Literal, ast_to_typed, get_name};
 use super::ast;
 
 use std::fmt::{Debug, Write};
 
 /// Indicates whether either side needs to be wrapped. Syntax whose end is ambiguous on that side
 /// must use parentheses, or forward the flag
-#[derive(PartialEq, Eq)]
+#[derive(PartialEq, Eq, Clone, Copy)]
 struct Wrap(bool, bool);
 
-#[derive(PartialEq, Eq, Hash)]
-pub struct Expr(pub Clause, pub Mrc<[Clause]>);
+#[derive(PartialEq, Eq, Hash, Clone)]
+pub struct Expr(pub Clause, pub Vec<Clause>);
 impl Expr {
   fn deep_fmt(&self, f: &mut std::fmt::Formatter<'_>, tr: Wrap) -> std::fmt::Result {
     let Expr(val, typ) = self;
     if typ.len() > 0 {
       val.deep_fmt(f, Wrap(true, true))?;
-      for typ in typ.as_ref() {
+      for typterm in typ {
         f.write_char(':')?;
-        typ.deep_fmt(f, Wrap(true, true))?;
+        typterm.deep_fmt(f, Wrap(true, true))?;
       }
     } else {
       val.deep_fmt(f, tr)?;
@@ -31,12 +33,6 @@ impl Expr {
   }
 }
 
-impl Clone for Expr {
-  fn clone(&self) -> Self {
-    Self(self.0.clone(), Mrc::clone(&self.1))
-  }
-}
-
 impl Debug for Expr {
   fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
     self.deep_fmt(f, Wrap(false, false))
@@ -46,9 +42,9 @@ impl Debug for Expr {
 #[derive(PartialEq, Eq, Hash)]
 pub enum Clause {
   Literal(Literal),
-  Apply(Mrc<Expr>, Mrc<Expr>),
-  Lambda(u64, Mrc<[Clause]>, Mrc<Expr>),
-  Auto(u64, Mrc<[Clause]>, Mrc<Expr>),
+  Apply(Box<Expr>, Box<Expr>),
+  Lambda(u64, Box<[Clause]>, Box<Expr>),
+  Auto(u64, Box<[Clause]>, Box<Expr>),
   LambdaArg(u64), AutoArg(u64),
   ExternFn(ExternFn),
   Atom(Atom)
@@ -58,7 +54,7 @@ const ARGNAME_CHARSET: &str = "abcdefghijklmnopqrstuvwxyz";
 
 fn parametric_fmt(
   f: &mut std::fmt::Formatter<'_>,
-  prefix: &str, argtyp: Mrc<[Clause]>, body: Mrc<Expr>, uid: u64, wrap_right: bool
+  prefix: &str, argtyp: &[Clause], body: &Expr, uid: u64, wrap_right: bool
 ) -> std::fmt::Result {
   if wrap_right { f.write_char('(')?; }
   f.write_str(prefix)?;
@@ -80,12 +76,8 @@ impl Clause {
       Self::Literal(arg0) => write!(f, "{arg0:?}"),
       Self::ExternFn(nc) => write!(f, "{nc:?}"),
       Self::Atom(a) => write!(f, "{a:?}"),
-      Self::Lambda(uid, argtyp, body) => parametric_fmt(f,
-        "\\", Mrc::clone(argtyp), Mrc::clone(body), *uid, wr
-      ),
-      Self::Auto(uid, argtyp, body) => parametric_fmt(f,
-        "@", Mrc::clone(argtyp), Mrc::clone(body), *uid, wr
-      ),
+      Self::Lambda(uid, argtyp, body) => parametric_fmt(f, "\\", argtyp, body, *uid, wr),
+      Self::Auto(uid, argtyp, body) => parametric_fmt(f, "@", argtyp, body, *uid, wr),
       Self::LambdaArg(uid) | Self::AutoArg(uid) => f.write_str(&
         string_from_charset(*uid, ARGNAME_CHARSET)
       ),
@@ -99,19 +91,27 @@ impl Clause {
       }
     }
   }
-  pub fn wrap(self) -> Mrc<Expr> { Mrc::new(Expr(self, to_mrc_slice(vec![]))) }
-  pub fn wrap_t(self, t: Clause) -> Mrc<Expr> { Mrc::new(Expr(self, one_mrc_slice(t))) }
+  pub fn wrap(self) -> Box<Expr> { Box::new(Expr(self, vec![])) }
+  pub fn wrap_t(self, t: Clause) -> Box<Expr> { Box::new(Expr(self, vec![t])) }
 }
 
 impl Clone for Clause {
   fn clone(&self) -> Self {
     match self {
-      Clause::Auto(uid,t, b) => Clause::Auto(*uid, Mrc::clone(t), Mrc::clone(b)),
-      Clause::Lambda(uid, t, b) => Clause::Lambda(*uid, Mrc::clone(t), Mrc::clone(b)),
+      Clause::Auto(uid, t, b) => {
+        let new_id = get_name();
+        let new_body = apply_lambda(*uid, Clause::AutoArg(new_id).wrap(), b.clone());
+        Clause::Auto(new_id, t.clone(), new_body)
+      },
+      Clause::Lambda(uid, t, b) => {
+        let new_id = get_name();
+        let new_body = apply_lambda(*uid, Clause::LambdaArg(new_id).wrap(), b.clone());
+        Clause::Lambda(new_id, t.clone(), new_body)
+      },
       Clause::Literal(l) => Clause::Literal(l.clone()),
       Clause::ExternFn(nc) => Clause::ExternFn(nc.clone()),
       Clause::Atom(a) => Clause::Atom(a.clone()),
-      Clause::Apply(f, x) => Clause::Apply(Mrc::clone(f), Mrc::clone(x)),
+      Clause::Apply(f, x) => Clause::Apply(Box::clone(&f), x.clone()),
       Clause::LambdaArg(id) => Clause::LambdaArg(*id),
       Clause::AutoArg(id) => Clause::AutoArg(*id)
     }
@@ -138,4 +138,26 @@ impl TryFrom<&ast::Clause> for Clause {
   }
 }
 
-pub fn count_references(id: u64, clause: &Clause)
\ No newline at end of file
+pub fn is_used_clause(id: u64, is_auto: bool, clause: &Clause) -> bool {
+  match clause {
+    Clause::Atom(_) | Clause::ExternFn(_) | Clause::Literal(_) => false,
+    Clause::AutoArg(x) => is_auto && *x == id,
+    Clause::LambdaArg(x) => !is_auto && *x == id,
+    Clause::Apply(f, x) => is_used_expr(id, is_auto, &f) || is_used_expr(id, is_auto, &x),
+    Clause::Auto(n, t, b) => {
+      assert!(*n != id, "Shadowing should have been eliminated");
+      if is_auto && t.iter().any(|c| is_used_clause(id, is_auto, c)) {return true};
+      is_used_expr(id, is_auto, b)
+    }
+    Clause::Lambda(n, t, b) => {
+      assert!(*n != id, "Shadowing should have been eliminated");
+      if is_auto && t.iter().any(|c| is_used_clause(id, is_auto, c)) {return true};
+      is_used_expr(id, is_auto, b)
+    }
+  }
+}
+
+pub fn is_used_expr(id: u64, is_auto: bool, Expr(val, typ): &Expr) -> bool {
+  if is_auto && typ.iter().any(|c| is_used_clause(id, is_auto, c)) {return true};
+  is_used_clause(id, is_auto, val)
+}
\ No newline at end of file