-
Notifications
You must be signed in to change notification settings - Fork 10
Show warning when erased argument is passed as omega #265
Copy link
Copy link
Open
Labels
derive: entryIssue on the derivation function facing to the end-userIssue on the derivation function facing to the end-userissue: bad messageWhen library reports some problem badlyWhen library reports some problem badlyissue: compilation errorWhen compilation error raises because of the libraryWhen compilation error raises because of the librarypart: derivationRelated to automated derivation of generatorsRelated to automated derivation of generators
Description
Metadata
Metadata
Assignees
Labels
derive: entryIssue on the derivation function facing to the end-userIssue on the derivation function facing to the end-userissue: bad messageWhen library reports some problem badlyWhen library reports some problem badlyissue: compilation errorWhen compilation error raises because of the libraryWhen compilation error raises because of the librarypart: derivationRelated to automated derivation of generatorsRelated to automated derivation of generators
It is known that DepTyCheck derivator does not treat erased arguments properly: their quantity is \omega even if it is never used so. Eventually, it may cause the derivation process to end with the typecheck error
... is not accessible in this contextI suggest to add a warning/error when the derivator is passing an erased parameter as an omega argument in a subgenerator.