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.
In a nutshell, defaulting implicit offset to
after
is not compatible with layout polymorphism. One concrete example is:The
foo
function's type signature will be expanded toPairBool layout record { a : 1b, b : 1b at 1b } -> ...
according to the implicitafter
semantics. At the call site ofid
insidefoo
, the surface TC will explicitly apply types and layout toid
, rendering itid [] {{1b}}
. When the Core TC sees it, it will infer the type to bePairBool layout record { a : 1b, b : 1b } -> ...
by layout substitution, as the core doesn't haveafter
. So the inferred type ofid x
is different from the type signature.