Showing content from https://github.com/agda/agda/issues/7245 below:
INJECTIVE_FOR_INFERENCE silently ignored on non-functions · Issue #7245 · agda/agda · GitHub
Pragma INJECTIVE_FOR_INFERENCE is currently silently ignored if applied to a non-function.
We would like to be warned about the UselessInjectiveForInferencePragma.
A.InjectiveForInferencePragma x -> markFirstOrder x
Notably, the implementation is framed by cases that make more effort (
StaticPragma
,
NotProjectionLikePragma
,
InlinePragma
):
A.StaticPragma x -> do def <- getConstInfo x case theDef def of Function{} -> markStatic x _ -> typeError $ GenericError "STATIC directive only works on functions" A.InjectivePragma x -> markInjective x A.InjectiveForInferencePragma x -> markFirstOrder x A.NotProjectionLikePragma qn -> do def <- getConstInfo qn case theDef def of it@Function{} -> modifyGlobalDefinition qn $ \def -> def { theDef = it { funProjection = Left NeverProjection } } _ -> typeError $ GenericError "NOT_PROJECTION_LIKE directive only applies to functions" A.InlinePragma b x -> do def <- getConstInfo x case theDef def of Function{} -> markInline b x d@Constructor{ conSrcCon } | copatternMatchingAllowed conSrcCon -> modifyGlobalDefinition x $ set lensTheDef d{ conInline = b } _ -> typeError $ GenericError $ applyUnless b ("NO" ++) "INLINE directive only works on functions or constructors of records that allow copattern matching"
I am saying "more effort" here because these cases have some deficiencies:
- use of
GenericError
- error instead of warning
- unclear what happens for
abstract (because getConstInfo might return AbstractDefn); there should be comments showing that the implementor was aware of abstract and the current implementation works as expected for abstract
ATTN: @WhatisRT @UlfNorell
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4