after and layout polymorphism

[zilinc]

In a nutshell, defaulting implicit offset to after is not compatible with layout polymorphism. One concrete example is:

type PairBool = { a : Bool, b : Bool }
layout L x = record {a : x, b : x}

id : all (x :~ Bool). PairBool layout (L x) -> PairBool layout (L x)
id x = x

foo : PairBool layout (L 1b) -> PairBool layout (L 1b)
foo x = id x

The foo function's type signature will be expanded to PairBool layout record { a : 1b, b : 1b at 1b } -> ... according to the implicit after semantics. At the call site of id inside foo, the surface TC will explicitly apply types and layout to id, rendering it id [] {{1b}}. When the Core TC sees it, it will infer the type to be PairBool layout record { a : 1b, b : 1b } -> ... by layout substitution, as the core doesn't have after. So the inferred type of id x is different from the type signature.

[zilinc]

The easy solution is to reject after layouts if its offset depends on layout variables. The ultimate solution is to add after to Core.