Unclear error message #77

New Issue

aniva · 2024-06-06T15:23:55-07:00

aniva commented

2024-06-06 15:23:55 -07:00

If an expression leads to elaboration failure, its message is unclear:

> .lake/build/bin/pantograph Init
goal.start {"expr": "forall (x: Prop), y"}
{"error":"elab","desc":"internal exception #8"}

If an expression leads to elaboration failure, its message is unclear: ```sh > .lake/build/bin/pantograph Init goal.start {"expr": "forall (x: Prop), y"} {"error":"elab","desc":"internal exception #8"} ```

aniva added this to the 0.3 milestone 2024-06-06 15:23:55 -07:00

aniva added the

labels 2024-06-06 15:23:55 -07:00

aniva self-assigned this 2024-06-06 15:23:55 -07:00

aniva commented

2024-06-07 22:05:50 -07:00

This is due to the autoBoundImplicit flag on the elaboration monad. It was there because of our handling of universe levels

This is due to the `autoBoundImplicit` flag on the elaboration monad. It was there because of our handling of universe levels

aniva commented

2024-06-10 13:01:20 -07:00

We likely have to add proper explicit handling of universe levels. This has been the elephant in the room for a year. The downside is that the solver would have to be aware of it. This is not an issue for Trillium, but LLMs may have a hard time.