Naming of typeclass instances

• In Prosa, we have a few typeclasses instances that take non-typeclass parameters.
• The typeclass inference algorithm of Coq can not infer such instances.
• Sometimes such instance definitions are restated at the top of a file with the non typeclass parameters fed to it.
• Examples: in task_intra_interference_bound, in fp_bounded_bi, in the sequential readiness facts file, etc
• In my opinion, the naming employed in these kinds of definitions is bad.
• In the files that import these files, the instance name gets bound to the concrete definition with the nontypeclass parameters fed to it.
• For example, assume I have a file A.v that imports the task_intra_interference_bound file. The output of Check rs_jlfp_interference is

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule ?PState -> Interference ?Job
where
?Job : [ |- JobType]
?PState : [ |- ProcessorState ?Job]
?JLFP : [ |- JLFP_policy ?Job]

while I would have expected

rs_jlfp_interference
     : arrival_sequence ?Job ->
       schedule PState -> JLFP_policy ?Job -> Interference ?Job

• If we need to define a concrete definitions of such instances then we should use Local Definition.

changed the description

I honestly do not see a lot of difference between

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule ?PState -> Interference ?Job
where
?Job : [ |- JobType]
?PState : [ |- ProcessorState ?Job]
?JLFP : [ |- JLFP_policy ?Job]

and

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule PState -> JLFP_policy ?Job -> Interference ?Job

Do you miss JLFP_policy as an explicit parameter in the first case?

(A bit of context maybe relevant for other people)

Let's create a file A.v. And then edit import of rs_jlfp_interference in file task_intra_interference_bound.v.

Current output:

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule ?PState -> Interference ?Job
where
?Job : [ |- JobType]
?PState : [ |- ProcessorState ?Job]
?JLFP : [ |- JLFP_policy ?Job]

Use Local Definition instead of #[local] Instance:

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule ?PState -> JLFP_policy ?Job -> Interference ?Job
where
?Job : [ |- JobType]
?PState : [ |- ProcessorState ?Job]

Use a different name, eg. local_rs_jlfp_interference:

rs_jlfp_interference
     : arrival_sequence ?Job -> schedule ?PState -> JLFP_policy ?Job -> Interference ?Job
where
?Job : [ |- JobType]
?PState : [ |- ProcessorState ?Job]

mentioned in issue #137