Solving premises with an already existing _solution_

[FissoreD]

In the following example, The class C has a parameter of type class. The instance c would produce the premise D (Ofe nat), however, as shown in the goal (activate the elpi tracer to see it), the unification of C (ofe_nat) H would produce the recursive call D (Ofe nat) H where H is a ground term: here we have 2 potential problems:

1. we solve a premise which already has a solution

2. as in the example, this may cause further unification problems (elpi can't unify D ofe_nat with D (Ofe nat))

   
   Module CS7.
   
   Structure ofe := Ofe { ofe_car : Type;  }.
   
   Class D (I : ofe).
   Class C (X : ofe) (I : D X).
   
   Definition ofe_nat : ofe := Ofe nat.
   Instance c : forall (H : D (Ofe nat)), C ofe_nat H := {}.
   
   Goal forall (H : D ofe_nat), C (ofe_nat) H.
   Fail apply _.
   Abort.

End CS7.

[FissoreD]

A possible solution:

• when compiling an instance $i$,
• if a premise $p$ of $i$ is a TC, and $p$ is used in the conclusion of $i$,
• then do not add $p$ as premise in the elpi rule

[FissoreD]

Note however, in the example below, not adding the premise, would produce a sealed goal:

Structure ofe := Ofe { ofe_car : Type; }.

Class D (I : ofe).

Class C (X : ofe) (I : D X).

Definition ofe_nat : ofe := Ofe nat.

Instance c : forall (H : D (Ofe nat)), C ofe_nat H := {}.

Goal forall (H : D ofe_nat), True -> exists H, C (ofe_nat) H.
  intros.
  notypeclasses refine (ex_intro _ _ _ ).
  apply _.
  Unshelve. (* Here the shelved goal `D ofe_nat` *)
  auto.
Abort.

[FissoreD]

Another way to see it could be: if I'm solving a rule and the rule has a rigid solution, then I succeed immediately without looking at the premises