[TC] Check for existence of typeclass instance on instantiation of a constrained type variable or abstract type

[fdupress]

No description provided.

[fdupress]

The following snippet shows two questionable successes. Both rely on the clone lifting an assumption about an abstract type to the concrete type it is instantiated with, instead of having that assumption checked.

It also shows a non-questionable success. Non-questionable in the sense that there is no world in which it should be a success. (It also means that the scope of the missing constraint check is well beyond clones and I need to rename this issue.)

op p : 'a -> bool.

type class tc = {
  axiom pP : forall (x : tc), p x
}.

theory VeryBad.
theory T.

type t <: tc.

lemma urk : p witness<:t>.
proof. exact: pP. qed.

end T.

type t2.

clone import T as T' with type t <- t2.

lemma urker : p witness<:t2>.
proof. apply: urk. qed.
end VeryBad.

theory AlsoBad.
theory T.

type t <: tc.
end T.

lemma urk ['a <: tc] : p witness<:'a>.
proof. exact: pP. qed.

type t2.
clone T as T' with type t <- t2.

lemma urker : p witness<:t2>.
proof. by apply: urk<:t2>. qed.
end AlsoBad.

theory VeryVeryBad.
type t.

lemma urkest: p witness<:t>.
proof. by apply (pP<:t> witness). qed.
end VeryVeryBad.