Avoid unnecessary quotation in elaboration #462
Conversation
| let test : Array16 2 () -> Array16 2 () = fun x => x; | ||
| let test : Array32 2 () -> Array32 2 () = fun x => x; | ||
| let test : Array64 2 () -> Array64 2 () = fun x => x; | ||
| let test : Array8 ((1 : U8) + (2 : U8)) () -> Array8 3 () = fun x => x; |
There was a problem hiding this comment.
I think we want simple expressions like this to be reduced in the final output. Maybe allow marking items with #[opaque] to prevent them reducing during quoting or something?
There was a problem hiding this comment.
I dunno - isn’t this reflecting the elaboration input more accurately though? i.e.
There was a problem hiding this comment.
If I write something like
let x : id Bool = false;
x
I would expect the type of x to be displayed as Bool, not id Bool,
and similarly for
def x : id Bool = false;
There was a problem hiding this comment.
Yeah, agreed. I think id Bool would still be displayed as Bool in type errors, as we generally evaluate types before displaying them to the user. This is just the result of fathom elab, which I would expect to be closer to what was originally provided by the user (unless inserted by the elaborator).
There was a problem hiding this comment.
Hmm, I need to think about it more. I do like how it makes the output in the other cases more readable!
There was a problem hiding this comment.
Another thing I’d like to look into at some stage is glued evaluation which is related to this stuff IIUC?
This reduces some bloat in the elaboration output
brendanzab
force-pushed
the
avoid-quotation
branch
from
a9605e8 to
73d3f5a
Compare
This reduces some bloat in the elaboration output