Keep extra types in AST only when logging is enabled (Follow-up from "Draft: Proto Alpha: remove stack types from kinfo")
!4731 (merged) added extra types in the AST to reconstruct the stack types for logging.
But those types are not strictly necessary for the elaboration or the interpretation.
What should be done:
- wrap them in an option-like type
- ideally a private or abstract type with the only goal to clearly identify them
- pass an extra argument in the elaborator to decide whether they should be kept (first attempt as to result
type_logger
but it may not be the best solution) - never count them in the IR size, even where they are present to be sure to obtain the same result regardless of logging being enabled
(to go further, but probably not wanted: bind the None/Some state of these types to an extra type parameter added to kinstr
to "prove" they are not used in the interpreter)
The following discussion from !4731 (merged) should be addressed:
-
@mbouaziz started a discussion: (+7 comments) For later: we keep the extra types in the AST only when logging is enabled (sparkled with GADTs
😉 )