Hello! I’ve been playing with GADTs and I found a very interesting problem. I seem to be getting `Warning 8: this pattern-matching is not exhaustive.`

, when the pattern-matching should be exhaustive.

Here is my minimal example:

```
module FailsWithWarning = struct
module Nat = struct
type zero
type positive
type 'n s = S : 'n -> 'n s
type ('m, 'n, 'typ) t =
| Z : ('m, 'm, zero) t
| S : ('m, 'n, 'any) t -> ('m, 'n s, positive) t
end
type ('a, 'length) hlist =
| [] : ('b, ('m, 'm, Nat.zero) Nat.t) hlist
| ( :: ) :
'a * ('b, ('m, 'l, 'typ) Nat.t) hlist
-> ('a -> 'b, ('m, 'l Nat.s, Nat.positive) Nat.t) hlist
let safe_head :
type a. (a -> 'b, ('m, 'l Nat.s, Nat.positive) Nat.t) hlist -> a = function
| x :: _ -> x
end
module NoWarning = struct
type zero
type positive
type 'n s = S : 'n -> 'n s
type ('m, 'n, 'typ) t =
| Z : ('m, 'm, zero) t
| S : ('m, 'n, 'any) t -> ('m, 'n s, positive) t
type ('a, 'length) hlist =
| [] : ('b, ('m, 'm, zero) t) hlist
| ( :: ) :
'a * ('b, ('m, 'l, 'typ) t) hlist
-> ('a -> 'b, ('m, 'l s, positive) t) hlist
let safe_head :
type a. (a -> 'b, ('m, 'l s, positive) t) hlist -> a = function
| x :: _ -> x
end
```

I’m guessing that the type unification must have some module bounds. It can infer it correctly when all types are in the same module but not across modules.

Any idea what could be causing the issue?