No type information is ever passed to a compilation phase lower than the typechecker in the OCaml compiler pipeline.

In the GADTs case, the type system is only used to remove the failure branch. For instance,

    type 'a t = A: int t | B: float t
    let always_a (x:int t) = match x with
    | A -> ()
    | _ -> .

is translated to

  (let (always_a/270 = (function x/272[int] : int 0))

because the typechecker can prove that the `B` case is impossible. In other words, GADTs are yet another instance where the type system can be used to eliminate dead code in the untyped IR.

I see, so you can never really get a match_failure due to type level mismatch with GADT because it would be caught by the compiler.

Makes sense to me.