Closed andreasabel closed 2 weeks ago
Pragma INJECTIVE_FOR_INFERENCE is currently silently ignored if applied to a non-function. We would like to be warned about the UselessInjectiveForInferencePragma. https://github.com/agda/agda/blob/185d9d4761db0c5a261fd449fbfef04bf9319377/src/full/Agda/TypeChecking/Rules/Decl.hs#L778 Notably, the implementation is framed by cases that make more effort (StaticPragma, NotProjectionLikePragma, InlinePragma): https://github.com/agda/agda/blob/185d9d4761db0c5a261fd449fbfef04bf9319377/src/full/Agda/TypeChecking/Rules/Decl.hs#L772-L791 I am saying "more effort" here because these cases have some deficiencies:
INJECTIVE_FOR_INFERENCE
UselessInjectiveForInferencePragma
StaticPragma
NotProjectionLikePragma
InlinePragma
GenericError
abstract
getConstInfo
AbstractDefn
ATTN: @WhatisRT @UlfNorell
Pragma
INJECTIVE_FOR_INFERENCEis currently silently ignored if applied to a non-function. We would like to be warned about theUselessInjectiveForInferencePragma. https://github.com/agda/agda/blob/185d9d4761db0c5a261fd449fbfef04bf9319377/src/full/Agda/TypeChecking/Rules/Decl.hs#L778 Notably, the implementation is framed by cases that make more effort (StaticPragma,NotProjectionLikePragma,InlinePragma): https://github.com/agda/agda/blob/185d9d4761db0c5a261fd449fbfef04bf9319377/src/full/Agda/TypeChecking/Rules/Decl.hs#L772-L791 I am saying "more effort" here because these cases have some deficiencies:GenericErrorabstract(becausegetConstInfomight returnAbstractDefn); there should be comments showing that the implementor was aware ofabstractand the current implementation works as expected forabstractATTN: @WhatisRT @UlfNorell