You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Here ?fun_rhs is being solved when checking the Refl and then substituted into fun with 'erased as an argument instead of arg-0. This also happens when _ or ? is used in place of ?fun_rhs.
Observed Behavior
The code compiles without error or warning and crashes with Exception in : erased is not a number (and s similar message on javasacript).
Expected Behavior
I believe correct code should be produced or a warning / error should be presented. I'm not sure if we intend for named holes to be solved. I see a SolvedNameHole error in Idris, but it is never thrown.
If _ and ? are allowed to be used at a non-erased quantity, we should get the arguments right. Otherwise, we should emit an error when they are used at a non-erased quantity.
Are named holes allowed to be solved? And are we allowed to use _ and ? to be used in unerased contexts?
The text was updated successfully, but these errors were encountered:
Steps to Reproduce
The compiler produces produces bad scheme code for the following:
The scheme output is:
Here
?fun_rhs
is being solved when checking theRefl
and then substituted intofun
with'erased
as an argument instead ofarg-0
. This also happens when_
or?
is used in place of?fun_rhs
.Observed Behavior
The code compiles without error or warning and crashes with
Exception in : erased is not a number
(and s similar message on javasacript).Expected Behavior
I believe correct code should be produced or a warning / error should be presented. I'm not sure if we intend for named holes to be solved. I see a
SolvedNameHole
error in Idris, but it is never thrown.If
_
and?
are allowed to be used at a non-erased quantity, we should get the arguments right. Otherwise, we should emit an error when they are used at a non-erased quantity.Are named holes allowed to be solved? And are we allowed to use
_
and?
to be used in unerased contexts?The text was updated successfully, but these errors were encountered: