Defining a higher-rank class instance for `Nat.iterate`

Stream: new members

[Sebastian Graf]

I'm trying to define a Repr instance for mathlib's Nat.iterate. Here's what I got so far:

import Mathlib.Logic.Function.Iterate

import Mathlib.Logic.Function.Iterate

instance (f : Type → Type) (n : Nat) (α : Type) [∀β [Repr β], Repr (f β)] [Repr α] : Repr (f^[n] α) where
  reprPrec t p := match n with
  | 0   => reprPrec (cast (by simp : f^[0] α = α) t) p
  | n+1 => reprPrec (cast (Function.iterate_succ_apply' _ _ _ : f^[n+1] α = f (f^[n] α)) t) p

Unfortunately, it fails to resolve the type class instance for the inductive case:

failed to synthesize
  Repr (f (f^[n] α))
use `set_option diagnostics true` to get diagnostic information

What do I do? Note that it should be able to infer Repr (f^[n] α) and infer Repr (f (f^[n] α)) using the higher-rank constraint. I just don't know how to nudge the elaborator into it.

[Sebastian Graf]

Hmm, OK, the following works, but it's not pretty:

instance (f : Type → Type) (n : Nat) (α : Type) [instReprF : ∀β [Repr β], Repr (f β)] [instReprα : Repr α] : Repr (f^[n] α) where
  reprPrec t p := match n with
  | 0   => reprPrec (cast (by simp : f^[0] α = α) t) p
  | n+1 => let t := (cast (Function.iterate_succ_apply' _ _ _ : f^[n+1] α = f (f^[n] α)) t);
           @reprPrec _ (@instReprF _ (@instReprIterate_absDen _ _ _ instReprF _)) t p

Perhaps there is a simple trick I'm missing?

[Sebastian Graf]

Furthermore, the elaborator doesn't seem able to solve for the instance.

#synth Repr ((Prod Unit)^[100] Unit)

says

failed to synthesize
  Repr ((Prod Unit)^[100] Unit)
use `set_option diagnostics true` to get diagnostic information

(It works without ^[100], though.)