Simpler implicit arguments

Rather than using sizeof-rewriting which is slow and error-prone, just
make implicit function arguments explicit, so:

val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(0xFFFF)

would be re-written (by the typechecker itself) into

val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(32, 0xFFFF)

then all we need to do is map implicit -> int in a rewrite, and use
trivial sizeof-rewriting only. We pretty much never want to use the
form of sizeof-rewriting that propagates function arguments through
multiple functions because it's extremely error-prone. Anything that
isn't re-writable via trivial sizeof rewriting should be a type error,
so it would be good to re-write sizeof expressions within the
type-checker.

0 files changed, 0 insertions, 0 deletions