# How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking constructors with parameters which are covariant or contravariant.

I can not see an example of the subtype rule for type constructors with type parameters which are invariant.

For example consider some impure, mutable stack type:

type Stack : * -> *

push : forall a. Stack a -> a -> ()
pop : forall a. Stack a -> a


The type parameter on Stack represents a type that can be inputted and outputted from the stack, which makes it neither covariant nor contravariant.

To implement the subtyping rule for two Stack types could I simply apply the subtyping rule twice? Something like:

C1 |- a <: b -| C2    C2 |- b <: a -| C3
----------------------------------------
C1 |- Stack a <: Stack b -| C3

• Your Stack type is actually covariant. You want an example that either has mutable/IO operations in its type or contains both data and codata. Dec 13 '19 at 17:05