3 ms·
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
by octachron 5y ago
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.
- whimsicalism 5y agoI 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.