Generate all projectors/method via the tactic

[mtzguido]

unfold
let maybe_ghost (b:bool) (post : unit -> prop) =
  if b
  then unit -> squash (post ())
  else unit -> squash (post ())

noeq
type r (p:Type) = {
   ghost : bool;
   pred : p -> prop;
   ( ! ) : y:p -> maybe_ghost ghost (fun _ -> pred y);
}

Error:

* Error 19 at LimitationOfProjectors.fst(13,5-13,6):
  - Subtyping check failed; expected type y: p
      -> maybe_ghost (Mkr?.ghost (Mkr ghost pred op_Bang))
          (fun _ -> Mkr?.pred (Mkr ghost pred op_Bang) y); got type y: p -> maybe_ghost ghost (fun _ -> pred y)
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also LimitationOfProjectors.fst(13,18-13,53)

Query (from .smt2):

; Encoding query formula : forall (p: Type)
;   (projectee: LimitationOfProjectors.r p)
;   (b: Prims.bool)
;   (b: (_: p -> Prims.prop))
;   (b:
;   (y: p
;       -> ((match b with
;             | true -> _: Prims.unit -> Prims.squash (b y)
;             | _ -> _: Prims.unit -> Prims.squash (b y))
;           <:
;           Type)))
;   (_: _: Prims.unit{projectee == LimitationOfProjectors.Mkr b b b})
;   (y: p).
;   (*Subtyping check failed; expected type y: p
;   -> maybe_ghost (Mkr?.ghost (Mkr ghost pred op_Bang))
;       (fun _ -> Mkr?.pred (Mkr ghost pred op_Bang) y); got type y: p -> maybe_ghost ghost (fun _ -> pred y)*)
;   (match b with
;     | true -> _: Prims.unit -> Prims.squash (b y)
;     | _ -> _: Prims.unit -> Prims.squash (b y)) ==
;   (match Mkr?.ghost (LimitationOfProjectors.Mkr b b b) with
;     | true -> _: Prims.unit -> Prims.squash (Mkr?.pred (LimitationOfProjectors.Mkr b b b) y)
;     | _ -> _: Prims.unit -> Prims.squash (Mkr?.pred (LimitationOfProjectors.Mkr b b b) y))

I think this fails due to a combination of the dependency and use of pred under a binder in (!)'s type, so #1948 applies. It actually works if we just unfold the projectors for ghost and pred before checking (!).

While that unfolding may work, with @nikswamy we're thinking using the tactic from #1355 (comment) would be better overall. Trying...

[mtzguido]

Fails in the exact same way : )

The problem is that the unfolding of the projectors is blocked because we are under a match. Adding zeta_full to the tactic also makes it work, but is probably dangerous in general.

[mtzguido]

Tactic now in master and can be used instead of the builtin projector generation by attaching the meta_projectors attribute to the typeclass in question.