diff --git a/.travis.yml b/.travis.yml
index 09d88d1..84bb550 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -5,7 +5,7 @@ services:
 - docker
 env:
   global:
-  - PINS="lambda:."
+  - PINS="lambda:. crowbar:--dev"
   - DISTRO="debian-stable"
   matrix:
-  - PACKAGE="lambda" OCAML_VERSION="4.06.0"
+  - PACKAGE="lambda" OCAML_VERSION="4.05.0"
diff --git a/fuzz/idempotent.ml b/fuzz/idempotent.ml
new file mode 100644
index 0000000..84584e9
--- /dev/null
+++ b/fuzz/idempotent.ml
@@ -0,0 +1,16 @@
+open Lambda.Fuzzer
+open Crowbar
+
+let pp ppf _ = assert false
+
+let () =
+  add_test ~name:"idempotent" [ unsafe_expr_gen ] @@ fun unsafe_expr ->
+  match Lambda.typ unsafe_expr with
+  | Error _ -> bad_test ()
+  | Ok (Lambda.Expr.V (expr, ty)) ->
+    let unsafe_expr' = Lambda.Expr.untype expr in
+    match Lambda.typ unsafe_expr' with
+    | Error err -> Crowbar.fail (Fmt.strf "type(untype(type(expr))): %a" (Fmt.hvbox Lambda.pp_error) err)
+    | Ok (Lambda.Expr.V (expr', ty')) ->
+      check_eq ~pp:Lambda.Parsetree.pp ~eq:Lambda.Parsetree.equal
+        (Lambda.Expr.untype expr) (Lambda.Expr.untype expr')
diff --git a/fuzz/jbuild b/fuzz/jbuild
new file mode 100644
index 0000000..aef8f17
--- /dev/null
+++ b/fuzz/jbuild
@@ -0,0 +1,5 @@
+(jbuild_version 1)
+
+(executable
+ ((name idempotent)
+  (libraries (lambda))))
diff --git a/lambda.opam b/lambda.opam
index c5b089e..184b1d3 100644
--- a/lambda.opam
+++ b/lambda.opam
@@ -15,8 +15,6 @@ depends: [
   "menhir"
   "higher"
   "ppx_deriving"
+  "crowbar"
   "alcotest" {test}
 ]
-available: [
-  ocaml-version >= "4.06.0"
-]
diff --git a/src/fuzzer.ml b/src/fuzzer.ml
new file mode 100644
index 0000000..d35c375
--- /dev/null
+++ b/src/fuzzer.ml
@@ -0,0 +1,141 @@
+let unsafe_type_gen : Parsetree.Type.t Crowbar.gen =
+  let open Parsetree in
+
+  Crowbar.fix @@ fun unsafe_type_gen ->
+  Crowbar.choose
+    [ Crowbar.const Type.unit
+    ; Crowbar.const Type.int
+    ; Crowbar.const Type.int32
+    ; Crowbar.const Type.int64
+    ; Crowbar.const Type.bool
+    ; Crowbar.const Type.string
+    ; Crowbar.map [ unsafe_type_gen ] (fun t -> Type.list t)
+    ; Crowbar.map [ unsafe_type_gen ] (fun t -> Type.array t)
+    ; Crowbar.map [ unsafe_type_gen ] (fun t -> Type.option t)
+    ; Crowbar.map [ unsafe_type_gen; unsafe_type_gen ] (fun ta tb -> Type.either ta tb)
+    ; Crowbar.map [ unsafe_type_gen; unsafe_type_gen ] (fun ta tb -> Type.result ta tb)
+    ; Crowbar.map [ unsafe_type_gen; ] (fun t -> Type.apply t Type.lwt)
+    ; Crowbar.map [ Crowbar.bytes ] (fun name -> Type.abstract (Eq.witness name))
+        (* XXX(dinosaure): lol je suis vraiment pas sûr. *)
+    ; Crowbar.map [ unsafe_type_gen; unsafe_type_gen ] (fun ta tb -> Type.(ta ** tb))
+    ; Crowbar.map [ unsafe_type_gen; unsafe_type_gen ] (fun ta tb -> Type.(ta @-> tb)) ]
+
+let type_gen = Crowbar.map [ unsafe_type_gen ] Typedtree.Type.typ
+
+let pp_unit ppf () = Fmt.string ppf "()"
+let pp_either ppa ppb ppf = function
+  | T.L a -> Fmt.pf ppf "(L %a)" ppa a
+  | T.R b -> Fmt.pf ppf "(R %a)" ppb b
+let eq_int : int -> int -> bool = (=)
+let eq_bool : bool -> bool -> bool = (=)
+
+let value t pp eq v = Parsetree.V { v; t; pp; eq; }
+
+let (<.>) f g = fun x -> f (g x)
+
+let pp : type a. a T.t -> Parsetree.value -> a Fmt.t = fun witness -> function
+  | Parsetree.V { pp; t; v; _ } -> match T.equal t witness with
+    | Some Eq.Refl -> pp
+    | None -> Fmt.invalid_arg "Type %a does not match with value %a." Typedtree.Type.pp witness pp v
+
+let eq: type a. a T.t -> Parsetree.value -> a Parsetree.eq = fun witness -> function
+  | Parsetree.V { pp; eq; t; v; } -> match T.equal t witness with
+    | Some Eq.Refl -> eq
+    | None -> Fmt.invalid_arg "Type %a does not match with value %a." Typedtree.Type.pp witness pp v
+
+let to_list witness l =
+  let rec map : type a. a T.t -> Parsetree.value list -> a list -> a list = fun witness l a -> match l with
+    | [] -> List.rev a
+    | Parsetree.V { v; t; _ } :: r -> match T.equal t witness with
+      | Some Eq.Refl -> map witness r (v :: a)
+      | None -> map witness r a in
+  map witness l []
+
+let rec value_gen : type a. a T.t -> Parsetree.value Crowbar.gen = fun ty ->
+  match ty with
+  | T.Unit     -> Crowbar.const (value ty pp_unit (fun () () -> true) ())
+  | T.Int      -> Crowbar.(map [ int ] (value ty Fmt.int eq_int))
+  | T.Int32    -> Crowbar.(map [ int32 ] (value ty Fmt.int32 Int32.equal))
+  | T.Int64    -> Crowbar.(map [ int64 ] (value ty Fmt.int64 Int64.equal))
+  | T.Bool     -> Crowbar.(map [ bool ] (value ty Fmt.bool eq_bool))
+  | T.String   -> Crowbar.(map [ bytes ] (value ty Fmt.string String.equal))
+  | T.List ta  ->
+    let cmp = Typedtree.Type.eq_val ty in
+    Crowbar.(map [ list (value_gen ta); (value_gen ta) ]) (fun l x -> value ty Fmt.(list (pp ta x)) cmp (to_list ta l))
+  | T.Array ta ->
+    let cmp = Typedtree.Type.eq_val ty in
+    Crowbar.(map [ list (value_gen ta); (value_gen ta) ]) (fun l x -> value ty Fmt.(array (pp ta x)) cmp (Array.of_list @@ to_list ta l))
+  | T.Option ta ->
+    Crowbar.(map [ bool; (value_gen ta) ])
+      (fun o x ->
+         let pp = Fmt.(option (pp ta x)) in
+         let cmp = Typedtree.Type.eq_val ty in
+
+         match o with
+         | true -> value ty pp cmp (Some (Typedtree.Value.cast x ta)) 
+         | false -> value ty pp cmp None)
+  | T.Pair (ta, tb) ->
+    Crowbar.(map [ (value_gen ta); (value_gen tb) ])
+      (fun va vb ->
+         let ppa = pp ta va in
+         let ppb = pp tb vb in
+         let cmp = Typedtree.Type.eq_val ty in
+
+         value ty Fmt.(pair ppa ppb) cmp (Typedtree.Value.cast va ta, Typedtree.Value.cast vb tb))
+  | T.Either (ta, tb) ->
+    Crowbar.(map [ bool; (value_gen ta); (value_gen tb) ])
+      (fun c va vb ->
+         let ppa = pp ta va in
+         let ppb = pp tb vb in
+         let pp = pp_either ppa ppb in
+         let cmp = Typedtree.Type.eq_val ty in
+
+         match c with
+         | true -> value ty pp cmp (T.L (Typedtree.Value.cast va ta))
+         | false -> value ty pp cmp (T.R (Typedtree.Value.cast vb tb)))
+  | T.Result (ta, tb) ->
+    Crowbar.(map [ bool; (value_gen ta); (value_gen tb) ])
+      (fun c va vb ->
+         let ppa = pp ta va in
+         let ppb = pp tb vb in
+         let pp = Fmt.result ~ok:ppa ~error:ppb in
+         let cmp = Typedtree.Type.eq_val ty in
+
+         match c with
+         | true -> value ty pp cmp (Ok (Typedtree.Value.cast va ta))
+         | false -> value ty pp cmp (Error (Typedtree.Value.cast vb tb)))
+  | T.Lwt        -> Crowbar.bad_test ()
+  | T.Apply _    -> Crowbar.bad_test ()
+  | T.Abstract _ -> Crowbar.bad_test ()
+  | T.Arrow _    -> Crowbar.bad_test ()
+
+let pair_gen : 'a Crowbar.gen -> 'b Crowbar.gen ->  ('a * 'b) Crowbar.gen = fun a b -> Crowbar.map [a; b] (fun a b -> (a, b))
+
+let unsafe_expr_gen : Parsetree.expr Crowbar.gen =
+  Crowbar.fix @@ fun unsafe_expr_gen ->
+  Crowbar.choose
+    [ Crowbar.dynamic_bind type_gen (fun (Typedtree.Type.V ty) -> Crowbar.map [ (value_gen ty) ] Parsetree.of_value)
+    ; Crowbar.map [ Crowbar.int ] Parsetree.var
+    ; Crowbar.(map [ unsafe_type_gen; list unsafe_expr_gen ]) (fun typ expr -> Parsetree.list ~typ expr)
+    ; Crowbar.(map [ unsafe_type_gen; list unsafe_expr_gen ]) (fun typ expr -> Parsetree.array ~typ (Array.of_list expr))
+    ; Crowbar.(map [ unsafe_type_gen ] (fun ty -> Parsetree.none ty))
+    ; Crowbar.(map [ unsafe_expr_gen ]) Parsetree.some
+    ; Crowbar.(map [ unsafe_type_gen; unsafe_expr_gen ]) Parsetree.ok
+    ; Crowbar.(map [ unsafe_type_gen; unsafe_expr_gen ]) Parsetree.error
+    ; Crowbar.(map [ list (pair_gen bytes unsafe_type_gen); unsafe_expr_gen ]) Parsetree.lambda
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.pair
+    ; Crowbar.(map [ unsafe_expr_gen ]) Parsetree.fst
+    ; Crowbar.(map [ unsafe_expr_gen ]) Parsetree.snd
+    ; Crowbar.(map [ unsafe_type_gen; unsafe_expr_gen ]) Parsetree.left
+    ; Crowbar.(map [ unsafe_type_gen; unsafe_expr_gen ]) Parsetree.right
+    ; Crowbar.(map [ unsafe_type_gen; bytes; unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.let_var
+    ; Crowbar.(map [ unsafe_type_gen; bytes; list (pair_gen bytes unsafe_type_gen); unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.let_fun
+    ; Crowbar.(map [ unsafe_type_gen; bytes; pair_gen bytes unsafe_type_gen; unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.let_rec
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.if_
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.match_
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.apply
+    ; Crowbar.(map [ pair_gen bytes unsafe_type_gen; unsafe_type_gen; unsafe_expr_gen ]) Parsetree.fix
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.( = )
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.( + )
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.( - )
+    ; Crowbar.(map [ unsafe_expr_gen; unsafe_expr_gen ]) Parsetree.( * ) ]
diff --git a/src/jbuild b/src/jbuild
index 5a1641d..9c2ef0f 100644
--- a/src/jbuild
+++ b/src/jbuild
@@ -1,7 +1,7 @@
 (library
  ((name        lambda)
   (public_name lambda)
-  (libraries   (fmt logs lwt higher))
+  (libraries   (crowbar fmt logs lwt higher))
   (preprocess  (pps (ppx_deriving.show ppx_deriving.eq ppx_deriving.ord)))))
 
 (ocamllex (lexer))
diff --git a/src/lambda.ml b/src/lambda.ml
index e7a78d6..92d12ee 100644
--- a/src/lambda.ml
+++ b/src/lambda.ml
@@ -48,6 +48,7 @@ let parse_exn ?file ?primitives str =
 (* Typer *)
 
 module Parsetree = Parsetree
+module Fuzzer = Fuzzer
 
 module Type = Typedtree.Type
 module Var = Typedtree.Var
diff --git a/src/lambda.mli b/src/lambda.mli
index a7b07ee..84bf314 100644
--- a/src/lambda.mli
+++ b/src/lambda.mli
@@ -16,6 +16,7 @@
  *)
 
 module Parsetree = Parsetree
+module Fuzzer = Fuzzer
 
 module Type = Typedtree.Type
 module Var = Typedtree.Var
diff --git a/src/typedtree.ml b/src/typedtree.ml
index 6938c6f..c7ca8ac 100644
--- a/src/typedtree.ml
+++ b/src/typedtree.ml
@@ -662,7 +662,11 @@ module Expr = struct
                 (match Type.equal t t1, Type.equal ta t2, Env.eq g0 g1, Env.eq g0 g2 with
                  | Some Eq.Refl, Some Eq.Refl, Some Eq.Refl, Some Eq.Refl ->
                    Expr (Nar (Arr t, e1 :: e2), g0, ta)
-                 | _, _, _, _ -> assert false)
+                 | _, _, _, _ ->
+                   error e g [ TypMismatch {a=Type.V t; b=Type.V t1}
+                             ; TypMismatch {a=Type.V ta; b=Type.V t2}
+                             ; EnvMismatch {g=Env.V g0; g'=Env.V g1}
+                             ; EnvMismatch {g=Env.V g0; g'=Env.V g2} ])
               | _, _ -> assert false in
           aux_a (Array.to_list a) in
         typ_array t a g