# "-\> ." in pattern matching

**URL:** <https://discuss.ocaml.org/t/in-pattern-matching/2676>\
**Category:** Learning\
**Created:** [October 6, 2018, 12:45pm UTC](https://discuss.ocaml.org/t/in-pattern-matching/2676 "2018-10-06T12:45:27Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![lindig](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/lindig/32/532_2.png) [@lindig](https://discuss.ocaml.org/u/lindig)\
**Post date:** [October 6, 2018, 12:45pm UTC](https://discuss.ocaml.org/t/in-pattern-matching/2676/1 "2018-10-06T12:45:27Z")

</div>

The [OCaml grammar](https://github.com/ocaml/ocaml/blob/trunk/parsing/parser.mly#L2040-L2046) for patterns includes a case for `-> .` as the right hand side. I could not find it in the OCaml manual but it seems to be intended for unreachable patterns. Where is this documented and what is the idiomatic use case?

```auto
match_case:
    pattern MINUSGREATER seq_expr
      { Exp.case $1 $3 }
  | pattern WHEN seq_expr MINUSGREATER seq_expr
      { Exp.case $1 ~guard:$3 $5 }
  | pattern MINUSGREATER DOT
      { Exp.case $1 (Exp.unreachable ~loc:(make_loc $loc($3)) ()) }
;

```

Addendum: The reason I did not find it in the manual is that is a language extension that is described in the [GADT section](http://caml.inria.fr/pub/docs/manual-ocaml-4.07/extn.html#sec255) and doesn’t have an entry in the table of contents by itself.

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [October 6, 2018, 12:59pm UTC](https://discuss.ocaml.org/t/in-pattern-matching/2676/2 "2018-10-06T12:59:38Z")

</div>

Refutation cases are documented [here](http://caml.inria.fr/pub/docs/manual-ocaml-4.07/extn.html#sec255) .  
Briefly, they are useful when fiddling with GADTs to express that a clause is impossible.  
For instance if I have a heterogeneous list defined as

```auto
type empty = |
type 'a hlist = []: empty hlist | (::): 'a * 'b hlist -> ('a->'b) hlist 

```

then if I have a list with type `('a -> 'b) hlist`, I know that the list is non-empty.

```auto
let hd (type a b) : (a -> b) hlist -> a = function
  | a :: _ -> a
  | _ -> .

```

Here `| _ -> .` express the fact that the remaining case, `[]`, is impossible and that the typechecker should be able to prove it.

However, in this case, the typechecker automatically adds a refutation clause `_ -> .` if there is only one clause in a pattern matching. Thus, I could have written the previous example as

```auto
let hd (type a b): (a -> b) hlist -> a = fun (a :: _) -> a

```

but handwritten refutation clause are necessary in more complex cases.

---

<div class="post-metadata">

**Author:** ![2BitSalute](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/2bitsalute/32/2325_2.png) [@2BitSalute](https://discuss.ocaml.org/u/2BitSalute)\
**Post date:** [July 17, 2024, 9:10pm UTC](https://discuss.ocaml.org/t/in-pattern-matching/2676/4 "2024-07-17T21:10:02Z")

</div>

The 404 link should point to [OCaml - Language extensions](https://ocaml.org/manual/5.2/gadts.html) now.