Reasons why we want more type information at the KreMLin level

• Being able to remove erased arguments using types rather than a whole-program analysis
• Disjointness information to be carried down to C so that we can rely on restrict
• Generating contracts for functions at the API boundary

[@ contract ]
let f (l: UInt32.t) (b: buffer a{length b = l})

need to figure out what's Ghost (can't be compiled) and what's Tot (can be compiled)...?

• Do we get anything from using f (int x[32]) beyond documentation purposes?