#nullable enable

using System;

// ---

interface Hk<W, A> { }

// ---

static class Nat
{
  public static Nat_Z Z() => new Nat_Z();

  public static Nat_S<N> S<N>(this N prev)
    where N : Nat<N>
    => new Nat_S<N>(prev);

  public static Nat<N> Narrow<N>(this Hk<Nat_Mu, N> hk)
      where N : Nat<N>
          => (Nat<N>)hk;

  public static TyEq<Nat_S<N>, Nat_S<M>> Succ<N, M>(this TyEq<N, M> ty)
      where N : Nat<N>
      where M : Nat<M>
      => new TyEq_Trust<Nat_S<N>, Nat_S<M>>();

  public static TyEq<N, M> Prev<N, M>(this TyEq<Nat_S<N>, Nat_S<M>> ty)
      where N : Nat<N>
      where M : Nat<M>
      => new TyEq_Trust<N, M>();
}

//

abstract record Nat<N>() : Hk<Nat_Mu, N>
    where N : Nat<N>
{
  public abstract R Accept<R>(Nat_Visitor<R, N> visitor);

  public abstract Fin<N>? ToFin(uint value);

  public abstract TyEq<N, M>? Equals<M>(Nat<M> other)
    where M : Nat<M>;

  public abstract uint ToUInt();
}

interface Nat_Mu { }

//

sealed record Nat_Z() : Nat<Nat_Z>
{
  public override R Accept<R>(Nat_Visitor<R, Nat_Z> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_Z>(), this);

  public override Fin<Nat_Z>? ToFin(uint value)
    => null;

  public override TyEq<Nat_Z, M>? Equals<M>(Nat<M> other)
    => other.Accept<TyEq<Nat_Z, M>?>(new Nat_Z_Equals_Visitor<M>());

  public override uint ToUInt() => 0;
}

sealed record Nat_Z_Equals_Visitor<M>() : Nat_Visitor<TyEq<Nat_Z, M>?, M>
    where M : Nat<M>
{
  TyEq<Nat_Z, M>? Nat_Visitor<TyEq<Nat_Z, M>?, M>.Visit(TyEq<M, Nat_Z> ty, Nat_Z value)
    => ty.Rot();

  TyEq<Nat_Z, M>? Nat_Visitor<TyEq<Nat_Z, M>?, M>.Visit<X>(TyEq<M, Nat_S<X>> ty, Nat_S<X> value)
    => null;
}

//

interface Nat_S_Mu { }

sealed record Nat_S<N>(N Prev) : Nat<Nat_S<N>>, Hk<Nat_S_Mu, N>
    where N : Nat<N>
{
  public override R Accept<R>(Nat_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);

  public override Fin<Nat_S<N>>? ToFin(uint value)
    => value == 0 ? Fin.Z<N>() : Prev.ToFin(value - 1)?.S();

  public override TyEq<Nat_S<N>, M>? Equals<M>(Nat<M> other)
    => other.Accept<TyEq<Nat_S<N>, M>?>(new Nat_S_Equals_Visitor<N, M>(Prev));

  public override uint ToUInt() => 1 + Prev.ToUInt();
}

sealed record Nat_S_Equals_Visitor<N, M>(N Prev) : Nat_Visitor<TyEq<Nat_S<N>, M>?, M>
    where N : Nat<N>
    where M : Nat<M>
{
  TyEq<Nat_S<N>, M>? Nat_Visitor<TyEq<Nat_S<N>, M>?, M>.Visit(TyEq<M, Nat_Z> ty, Nat_Z value)
    => null;

  TyEq<Nat_S<N>, M>? Nat_Visitor<TyEq<Nat_S<N>, M>?, M>.Visit<X>(TyEq<M, Nat_S<X>> ty, Nat_S<X> value)
    => Prev.Equals(value.Prev)?.Succ().Compose(ty.Rot());
}

//

interface Nat_Visitor<R, N>
    where N : Nat<N>
{
  R Visit(TyEq<N, Nat_Z> ty, Nat_Z value);

  R Visit<M>(TyEq<N, Nat_S<M>> ty, Nat_S<M> value)
      where M : Nat<M>;
}

// ---

static class Fin
{
  public static Fin<N> ToFin<N>(this uint value, N bound)
    where N : Nat<N>
    => bound.ToFin(value);

  public static Fin<Nat_S<N>> Z<N>()
      where N : Nat<N>
      => new Fin_Z<N>();

  public static Fin<Nat_S<N>> S<N>(this Fin<N> prev)
      where N : Nat<N>
      => new Fin_S<N>(prev);

  public static Fin<N> Narrow<N>(this Hk<Fin_Mu, N> hk)
      where N : Nat<N>
          => (Fin<N>)hk;
}

//

abstract record Fin<N>() : Hk<Fin_Mu, N>
    where N : Nat<N>
{
  public abstract R Accept<R>(Fin_Visitor<R, N> visitor);

  public A Impossible<A>(TyEq<N, Nat_Z> ty)
      => throw new Exception("impossible: Fin<Nat_Z>");
}

interface Fin_Mu { }

//

sealed record Fin_Z<N>() : Fin<Nat_S<N>>
    where N : Nat<N>
{
  public override R Accept<R>(Fin_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);
}

//

sealed record Fin_S<N>(Fin<N> Prev) : Fin<Nat_S<N>>
    where N : Nat<N>
{
  public override R Accept<R>(Fin_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);
}

//

interface Fin_Visitor<R, N>
    where N : Nat<N>
{
  R Visit<M>(TyEq<N, Nat_S<M>> ty, Fin_Z<M> value)
      where M : Nat<M>;

  R Visit<M>(TyEq<N, Nat_S<M>> ty, Fin_S<M> value)
      where M : Nat<M>;
}

// ---

static class Vect
{
  public static Vect<A, Nat_Z> Nil<A>()
      => new Vect_Nil<A>();

  public static Vect<A, Nat_S<N>> Cons<A, N>(this Vect<A, N> tail, A head)
      where N : Nat<N>
      => new Vect_Cons<A, N>(head, tail);

  public static A IndexOf<A, N>(this Fin<N> ix, Vect<A, N> vect)
    where N : Nat<N>
    => vect[ix];
}

//

abstract record Vect<A, N>()
    where N : Nat<N>
{
  public abstract A this[Fin<N> ix] { get; }

  public abstract N Length { get; }
}

//

sealed record Vect_Nil<A>() : Vect<A, Nat_Z>
{
  public override A this[Fin<Nat_Z> ix]
    => ix.Impossible<A>(new TyEq_Refl<Nat_Z>());

  public override Nat_Z Length => Nat.Z();
}

//

sealed record Vect_Cons<A, N>(A Head, Vect<A, N> Tail) : Vect<A, Nat_S<N>>
    where N : Nat<N>
{
  public override A this[Fin<Nat_S<N>> ix]
    => ix.Accept(new Vect_Cons_Index_Visitor<A, N>(this));

  public override Nat_S<N> Length => Tail.Length.S();
}

sealed record Vect_Cons_Index_Visitor<A, N>(Vect_Cons<A, N> Cons) : Fin_Visitor<A, Nat_S<N>>
    where N : Nat<N>
{
  public A Visit<M>(TyEq<Nat_S<N>, Nat_S<M>> ty, Fin_Z<M> value) where M : Nat<M>
      => Cons.Head;

  public A Visit<M>(TyEq<Nat_S<N>, Nat_S<M>> ty, Fin_S<M> value) where M : Nat<M>
  {
    var ix = ty.Prev().LiftL<Fin_Mu>().Rot().Cast(value.Prev).Narrow();
    return Cons.Tail[ix];
  }
}

// ---

abstract record TyEq<A, B>()
{
  public abstract B Cast(A a);

  public abstract TyEq<A, C> Compose<C>(TyEq<B, C> ty);

  public abstract TyEq<B, A> Rot();

  public abstract TyEq<Hk<W, A>, Hk<W, B>> LiftL<W>();
}

sealed record TyEq_Refl<A>() : TyEq<A, A>
{
  public override A Cast(A a)
    => a;

  public override TyEq<A, C> Compose<C>(TyEq<A, C> ty)
    => ty;

  public override TyEq<A, A> Rot()
    => this;

  public override TyEq<Hk<W, A>, Hk<W, A>> LiftL<W>()
    => new TyEq_Refl<Hk<W, A>>();
}

sealed record TyEq_Trust<A, B>() : TyEq<A, B>
{
  public override B Cast(A a)
    => (B)(object)a;

  public override TyEq<A, C> Compose<C>(TyEq<B, C> ty)
    => new TyEq_Trust<A, C>();

  public override TyEq<Hk<W, A>, Hk<W, B>> LiftL<W>()
    => new TyEq_Trust<Hk<W, A>, Hk<W, B>>();

  public override TyEq<B, A> Rot()
    => new TyEq_Trust<B, A>();
}

// ---

interface SomeNat_Visitor<R>
{
  R Visit<N>(N nat) where N : Nat<N>;
}

interface SomeNat
{
  R Accept<R>(SomeNat_Visitor<R> visitor);

  public static SomeNat Z() => Nat.Z().Erase();
}

//

static class SomeNat_Helpers
{
  public static SomeNat ToSomeNat(this uint value)
  {
    SomeNat nat = SomeNat.Z();

    for (uint i = 0; i < value; i++)
    {
      nat = nat.S();
    }

    return nat;
  }

  public static SomeNat Erase<N>(this N nat)
    where N : Nat<N>
    => new SomeNat_Wrap<N>(nat);

  public static SomeNat S(this SomeNat nat)
    => nat.Accept(new SomeNat_S_Visitor());
}

sealed record SomeNat_S_Visitor() : SomeNat_Visitor<SomeNat>
{
  SomeNat SomeNat_Visitor<SomeNat>.Visit<N>(N nat) => nat.S().Erase();
}

//

sealed record SomeNat_Wrap<N>(N Nat) : SomeNat
  where N : Nat<N>
{
  public R Accept<R>(SomeNat_Visitor<R> visitor)
    => visitor.Visit<N>(Nat);
}

// ---

public static class Program
{
  public static void Main()
  {
    var xs = Vect.Nil<int>().Cons(2).Cons(1);

    Console.WriteLine(xs[Fin.Z<Nat_S<Nat_Z>>()]);
    Console.WriteLine(xs[Fin.Z<Nat_Z>().S()]);

    Console.WriteLine(0u.ToFin(bound: xs.Length)?.IndexOf(xs));
    Console.WriteLine(1u.ToFin(bound: xs.Length)?.IndexOf(xs));
    Console.WriteLine(2u.ToFin(bound: xs.Length)?.IndexOf(xs).ToString() ?? "null");

    Console.WriteLine(42u.ToSomeNat().Accept(new Example_SomeNat_Visitor()));

    Console.WriteLine(Nat.Z().S().S().S().Erase().Accept(new Example_SomeNat_Visitor()));
  }
}

sealed record Example_SomeNat_Visitor() : SomeNat_Visitor<uint>
{
  uint SomeNat_Visitor<uint>.Visit<N>(N nat) => nat.ToUInt();
}