WIP: feat: allow limited type ascriptions in data/codata

[alexkeizer]

No description provided.

[alexkeizer]

Implements #15

[monsterkrampe]

I've put a bit of time here and there trying to understand what is going wrong here.
I think I at least managed to narrow the issue down a bit but admittedly I'm still mostly stepping in the dark.
In the commit I just added (which can be removed later), I tried to explicitly define instance foo : MvFunctor.{1,1} ($baseApplied) := $functor in Qpf/Macro/Data.lean. This produces a type error visible in Test/Arrow.lean that does not quite make sense to me yet:

type mismatch
  MvQPF.Comp.instMvFunctorComp
has type
  MvFunctor
    (MvQPF.Comp (TypeFun.ofCurried (MvQPF.Arrow α)) (Vec.append1 Vec.nil (MvQPF.Prj (Fin2.fs Fin2.fz)))) : Type 1
but is expected to have type
  MvFunctor
    (Vec.append1 (Vec.append1 (Vec.append1 Vec.nil (MvQPF.Prj (Fin2.fs Fin2.fz))) (MvQPF.Prj Fin2.fz))
      (MvQPF.Comp (TypeFun.ofCurried (MvQPF.Arrow α)) (Vec.append1 Vec.nil (MvQPF.Prj (Fin2.fs Fin2.fz))))
      Fin2.fz) : Type 2

This especially throws me off since it does not only expect a different universe but a completely different type.

Maybe you guys already made some more progress regarding this issue. Or maybe you have an idea why adding instance foo : MvFunctor.{1,1} ($baseApplied) := $functor in Qpf/Macro/Data.lean yields the above error.

[alexkeizer]

We've not really worked on this lately, so your help is appreciated!

The error is rather misleading, but a bit of a red herring.
There is a vector of three types, which is being indexed by the last Fin2 you see.
Using imaginary syntax, we could pretty print it as:

!![ Prj _, Prj _, Comp  (TypeFun.ofCurried (MvQPF.Arrow α) !![Prj 1]] 0

Remembering that typevectors are indexed right-to-left, this indeed reduces to:

Comp  (TypeFun.ofCurried (MvQPF.Arrow α) !![Prj 1]

which is in fact the expected type (modulo universes)!