As a general rule, only abstract types can be refined by matching on GADT-constructors. When defining function operating on GADTs, it is therefore often necessary to use locally abstract types:

```
let get (type a): a t -> a = function
| I n -> n
| S s -> s
```

( If the function is recursive and , the locally abstract notation may need to be combined with the explicit polymorphic notation yielding `let get: type a. a t -> a=âŚ`

.)

However, on your first example, the problem is that your second case is simply impossible: since `i`

has for type `int t`

, the only possible case when matching on `i`

is `Int _`

. Consequently, your example can be rewritten as

```
let () =
let i = I 42 in
match i with
| I n -> Printf.printf "int: %d\n" n
```

And this pattern matching is exhaustive. If you donât feel reassured or if for some extremely imperious reasons you are not using the exhaustiveness check for pattern matching, it is possible to complete the pattern with a refutation case:

```
let () =
let i = I 42 in
match i with
| I n -> Printf.printf "int: %d\n" n
| _ -> .
```

Here the dot `.`

on the right hand side of the case indicates that the pattern on the left hand side should not be reachable and the type-checker will check that it is impossible to produce a value that matches this pattern.