diff --git a/client/F.ml b/client/F.ml
index e2d6e2cc59efb80d01817a1df0347fd98be78460..918fc342cb8dc96afea9c3a525459f327911818f 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -70,6 +70,7 @@ type ('a, 'b) term =
   | LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
   | Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
   | Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of range * ('a,'b) typ
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
@@ -223,6 +224,9 @@ module TypeInTerm : DeBruijn.TRAVERSE
         let t' = trav env t
         and brs' = List.map (traverse_branch lookup extend env) brs in
         Match (pos, ty', t', brs')
+    | Absurd (pos, ty) ->
+        let ty' = TypeInType.traverse lookup extend env ty in
+        Absurd (pos, ty')
 
   and traverse_datatype lookup extend env (tid, tyargs) =
     (tid, List.map (TypeInType.traverse lookup extend env) tyargs)
diff --git a/client/F.mli b/client/F.mli
index f97fe63b08b0c75e7c87a6c35ebd57dabb9b59ee..cb9ead6d577e2f420b996b5960fa6abcfae430a0 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -73,6 +73,7 @@ type ('a, 'b) term =
   | LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
   | Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
   | Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of range * ('a,'b) typ
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index 2108b27fb7c2ff38c0f1a44b9cc47a36e388711c..a7f8cf57fe698e92a2cf6e0aa0e3b337a1dd8628 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -86,6 +86,8 @@ let rec translate_term env (t : F.nominal_term) : P.term =
         self env t,
         List.map (translate_branch env) brs
       )
+  | F.Absurd (_, ty) ->
+      P.Absurd (translate_type env ty)
 
 and translate_branch env (pat, t) =
   (translate_pattern env pat, translate_term env t)
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 6c7c5fcc3c561ba4bda751f90f363d9d341ce422..bf61a28e9e2b0c7de1685da885e07f1edb8285be 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -437,6 +437,8 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
       let tys = List.map (typeof_branch datatype_env env scrutinee_ty) brs in
       List.iter (fun ty2 -> (--) ty ty2 env) tys;
       ty
+  | Absurd (_, _ty) ->
+      failwith "todo"
 
 and typeof_variant datatype_env lbl (tid, tyargs) =
   let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
diff --git a/client/P.ml b/client/P.ml
index da9c6425d77788533c894822895cb159a80494aa..0761aaea5fbc88176668d90ada3a5df6467c34cb 100644
--- a/client/P.ml
+++ b/client/P.ml
@@ -34,6 +34,7 @@ type term =
   | Inj of (typ list) option * int * term
   | Variant of Datatype.label_id * datatype option * term option
   | Match of typ option * term * branch list
+  | Absurd of typ
 
 and branch = pattern * term
 
diff --git a/client/Printer.ml b/client/Printer.ml
index 73b2e32608e15f3069bdbf2f01ebccbcd4720b47..92aec0f1c83f276a0054f96acd3b7188dee609f9 100644
--- a/client/Printer.ml
+++ b/client/Printer.ml
@@ -204,6 +204,8 @@ and print_term_atom t =
       print_match ty t brs
   | Annot (t, tyannot) ->
       print_annot (print_term t) tyannot
+  | Absurd _ ->
+      dot
   | TyAbs _ | Let _ | Abs _
   | TyApp _ | App _ | Proj _ | Inj _ | Variant _ as t ->
       parens (print_term t)