Field access for record newtypes in a constraint based type checker

I was thinking about how to implement newtypes in polaris. I want these to work mostly like they do in Haskell, but with one small change.

To make newtypes over records actually somewhat pleasant to use, I would like to be able to access fields ‘through’ the newtype like this (as long as the constructor is public)

newtype Blah = Blah { x : Int, y : Bool }

let blah = Blah { x = 1, y = true }

blah.x # I want this to typecheck and return an integer!

The issue here is that polaris’ type checker is constraint based, so this is less obvious than it looks.

With a single pass typechecker, this would be pretty easy! Instead of a more traditional row polymorphic rule for record access¹,

$\frac {\Gamma \vdash e \;{\color{blue}\Leftarrow}\; \{ x : \tau \;|\; \rho \} } {\Gamma \vdash e.x \;{\color{red}\Rightarrow}\; \tau} (\text{AccessTraditional})$ I could just infer the type of e and do some ad-hoc magic if it is known to be a record newtype at this point.

This immediately breaks down with constraints though. Consider this example:

let blah = Blah { x = 1, y = true }

let ohno = id(blah)

ohno.x

With the system above, this would not be accepted. id(blah) instantiates the polymorphic function id, so ohno is assigned the type α and a constraint α ~ Blah is emitted.

Because constraints are not solved immediately, this means that when inferring the type for ohno.x, ohno still has type α and the typechecker cannot know that it will have type Blah in the future!

I have a solution for this, but it feels a bit hacky. If there is a better way to do this, I would love to hear about it!

So, just like in the revised rule above, this rule for record access infers the type of e, but instead of immediately looking at the type or checking against a record type, it emits a new kind of constraint.

$\frac {\Gamma \vdash e \;{\color{red}\Rightarrow}\; \tau_r \;\;\; (x : \tau) \in \tau_r} {\Gamma \vdash e.x \;{\color{red}\Rightarrow}\; \tau} (\text{AccessConstraint})$

Where the constraint solver rules for these (x : τ) ∈ τ constraints look something like this

$\begin{align*} \text{solve}((x : \tau_1) \in C) &= \text{solve}((x : \tau) \in \rho) \text{ if } C \text{ is a newtype over a record type }\rho\\ \text{solve}((x : \tau_1) \in \{x : \tau_2 \;|\; \rho\}) &= \text{solve}(\tau_1 \sim \tau_2)\\ \text{solve}((x_1 : \tau_1) \in \{x_2 : \tau_2 \;|\; \rho\}) &= \text{solve}((x_1 : \tau_1) \in \rho)\\ \text{solve}((x : \tau) \in \alpha) &= \text{solve}(\alpha \sim \{ x : \tau \;|\; \rho \}) \end{align*}$

The last line essentially defaults to a record type, so that expressions like \r -> r.x still infer the regular row polymorphic type forall a. { x : a | r } -> a

Apologies for the off-center latex. I couldn’t get webtex to accept \begin{center}↩︎

Prophet

@prophet

Field access for record newtypes in a constraint based type checker