[ fix #3474 ] Fix implicit arguments in interface methods #3475
Conversation
spcfox
force-pushed
the
fix-argument-method
branch
from
51938ae to
74124b8
Compare
| namesToRawImp bind (nm@(UN{}) :: xs) fn = | ||
| namesToRawImp bind xs $ INamedApp vfc fn nm $ | ||
| if bind | ||
| then IBindVar vfc $ nameRoot nm |
There was a problem hiding this comment.
IBindVar is needed so that using capitalized names does not produce an error. Such names occur in the interface010 and interface011 tests.
To avoid a name conflict, I'd like to use machine generated names, but IBindVar takes a string.
| collectImplicitNames : RawImp -> List Name | ||
| collectImplicitNames (IPi _ _ Explicit _ _ ty) = [] | ||
| collectImplicitNames (IPi _ _ _ (Just n) _ ty) = n :: collectImplicitNames ty | ||
| collectImplicitNames (IPi _ _ _ Nothing _ ty) = collectImplicitNames ty |
There was a problem hiding this comment.
Skipping implicit arguments without names can cause an error, but I'm not sure how to handle them properly
There was a problem hiding this comment.
Example with an error:
interface Iface where
method : {_ : Type} -> TypeThere was a problem hiding this comment.
As far as I know, an implicit argument without a name cannot be passed. It might be useful to add a “disable implicits” mode as suggested in Discord and use it this. It could also be useful in user code
| collectImplicitNames (IPi _ _ _ Nothing _ ty) = collectImplicitNames ty | ||
| collectImplicitNames _ = [] | ||
|
|
||
| namesToRawImp : Bool -> List Name -> RawImp -> RawImp |
There was a problem hiding this comment.
This function is based on a similar function from processRecord. It may be worth making a global function for it
There was a problem hiding this comment.
In processRecord it is also useful to add IBindVar in LHS to avoid problems with capitalized names. But first I would like to get feedback on this solution
Description
fix #3474
This fix is inspired by #3468. It has the same problems:
Should this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).