I was looking for work on GADTs in the presence of subtyping and found this 2013 paper GADTs meet subtyping of Gabriel Scherer and Didier RÃ©my.

**Abstract**. While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.

The running example of the paper is (can you guess?) an expression type. One thing that I was looking for specifically that I didn't find addressed in the paper is how to interpret e.g. `even exp`

, where `even`

is a subtype of `int`

(in a more dependently typed language). Any thoughts on this or another other aspect of the paper?

## Recent comments

1 hour 8 min ago

2 hours 25 sec ago

4 hours 15 min ago

4 hours 41 min ago

7 hours 43 min ago

8 hours 5 min ago

8 hours 18 min ago

9 hours 15 min ago

21 hours 56 min ago

22 hours 23 min ago