diff --git a/lib/common/Subst.ml b/lib/common/Subst.ml
index d87acea..250b153 100644
--- a/lib/common/Subst.ml
+++ b/lib/common/Subst.ml
@@ -2,6 +2,7 @@ type t = Type.t Variable.Map.t
 
 let empty = Variable.Map.empty
 let add = Variable.Map.add
+let remove = Variable.Map.remove
 
 let rec apply (env : Type.Env.t) t =
   let substitute ty = apply env t ty in
diff --git a/lib/common/Subst.mli b/lib/common/Subst.mli
index 04fd367..28b5cb5 100644
--- a/lib/common/Subst.mli
+++ b/lib/common/Subst.mli
@@ -2,6 +2,7 @@ type t = Type.t Variable.Map.t
 
 val empty : t
 val add : Variable.t -> Type.t -> t -> t
+val remove : Variable.t -> t -> t
 
 val apply : Type.Env.t -> t -> Type.t -> Type.t
 val simplify : Type.Env.t -> Variable.Set.t -> t -> t
diff --git a/lib/unification/Env.ml b/lib/unification/Env.ml
index b367cd4..f5ece41 100644
--- a/lib/unification/Env.ml
+++ b/lib/unification/Env.ml
@@ -29,6 +29,7 @@ let tyenv t = t.tyenv
 let gen flags e : Variable.t = Variable.Gen.gen flags e.tyenv.var_gen
     
 let add e v ty = e.vars <- Subst.add v ty e.vars
+let remove e v = e.vars <- Subst.remove v e.vars
 
 let init_partial e v =
   e.partials <- Variable.Map.update v
diff --git a/lib/unification/Env.mli b/lib/unification/Env.mli
index 713950b..418ab9e 100644
--- a/lib/unification/Env.mli
+++ b/lib/unification/Env.mli
@@ -20,6 +20,7 @@ val representative : t -> Variable.t -> representative
 val push_tuple : t -> ACTerm.t -> ACTerm.t -> unit
 val push_arrow : t -> ArrowTerm.t -> ArrowTerm.t -> unit
 val add : t -> Variable.t -> Type.t -> unit
+val remove : t -> Variable.t -> unit
 val init_partial : t -> Variable.t -> unit
 val extend_partial : ?by:int -> t -> Variable.t -> Type.t -> unit
 
diff --git a/lib/unification/Occur_check.ml b/lib/unification/Occur_check.ml
new file mode 100644
index 0000000..ec195e8
--- /dev/null
+++ b/lib/unification/Occur_check.ml
@@ -0,0 +1,29 @@
+open CCOption.Infix
+
+type state = Done | Seen | Fresh
+
+exception Cycle of Variable.t list
+
+let find_cycle graph =
+  let states = Variable.HMap.create 10 in
+  Variable.Map.iter (fun v _ -> Variable.HMap.add states v Fresh) graph;
+  let rec dfs v =
+    match Variable.HMap.get_or ~default:Fresh states v with
+    | Fresh ->
+        Variable.HMap.add states v Seen;
+        let res =
+          let t = Variable.Map.get_or ~default:Type.dummy v graph in
+          Iter.find_map dfs (Type.iter_vars t)
+        in
+        Variable.HMap.add states v Done;
+        let+ u, path = res in
+        if Variable.equal u v then raise (Cycle (u :: path)) else (u, v :: path)
+    | Seen -> Some (v, [v])
+    | Done -> None
+  in
+  try
+    Variable.Map.iter (fun v _ -> assert (CCOption.is_none (dfs v))) graph;
+    None
+  with Cycle l -> Some l
+
+let occur_check env = find_cycle (Env.vars env)
diff --git a/lib/unification/Syntactic.ml b/lib/unification/Syntactic.ml
index 8d0c609..08e2299 100644
--- a/lib/unification/Syntactic.ml
+++ b/lib/unification/Syntactic.ml
@@ -53,7 +53,7 @@ include Infix
 (** Checking for cycles *)
 
 (* TO OPTIM/MEASURE *)
-let occur_check env : return =
+let _occur_check env : return =
   Trace.with_span ~__FUNCTION__ ~__LINE__ ~__FILE__ __FUNCTION__ (fun _sp ->
   debug (fun m -> m "@[<v>Occur check in@,%a@]" Env.pp env);
   let nb_predecessors = Variable.HMap.create 17 in
@@ -104,9 +104,47 @@ let occur_check env : return =
   in
   loop 0 vars_without_predecessors)
 
+let rec occur_check env : return =
+  match Occur_check.occur_check env with
+  | None -> Done
+  | Some l ->
+      Logs.debug (fun m -> m "Occur check in: %a" Env.pp env);
+      Logs.debug (fun m -> m "Cycle: %a" (CCList.pp Variable.pp) l);
+      let rec collapse stack = function
+        | u::v::tl -> (
+          match Env.representative env u with
+          | Env.V _ -> failwith "Impossible"
+          | Env.E (_, t) ->
+              match t with
+              | Type.Var _ | FrozenVar _ | Other _ -> failwith "Impossible"
+              | Constr _ | Arrow _ -> None
+              | Tuple l ->
+                  let stack =
+                    Type.NSet.fold
+                      (fun t stack ->
+                        match t with
+                        | Type.Var v' when Variable.equal v v' -> stack
+                        | t ->
+                          Stack.push stack t
+                            (Type.tuple (Env.tyenv env) Type.NSet.empty)(*unit*))
+                      l stack
+                  in
+                  collapse stack tl
+                  )
+        | _ -> Some stack
+      in
+      match collapse Stack.empty l with
+      | None -> FailedOccurCheck env
+      | Some stack ->
+        let v = List.hd l in
+        List.iter (fun u -> Env.add env u (Type.var (Env.tyenv env) v)) (List.tl l);
+        Env.remove env v;
+        let* () = process_stack env stack in
+        occur_check env
+
 (** Main process *)
 
-let rec process_stack env (stack : Stack.t) : return =
+and process_stack env (stack : Stack.t) : return =
   Trace.with_span ~__FUNCTION__ ~__LINE__ ~__FILE__ __FUNCTION__ (fun _sp ->
   debug (fun m -> m "Process_stack");
   Timeout.check ();