Some examples of potential outputs.

examples/identity.agda

@@ -0,0 +1,2 @@
+identity : ∀ { A : Set } → A → A
+identity x = x

examples/identity.rs

@@ -0,0 +1,5 @@
+pub fn identity<A>(param0: A) -> A {
+    match (param0, ) {
+        (x, ) => x,
+    }
+}

examples/nat.agda

@@ -0,0 +1,31 @@
+data Nat : Set where
+  Zero : Nat
+  Succ : Nat → Nat
+
+add : Nat → Nat → Nat
+add n Zero = n
+add n (Succ m) = Succ (add n m)
+
+data Eq {A : Set} (a : A) : A → Set where
+  Refl : Eq a a
+
+cong : {A B : Set} → {a b : A} → (f : A → B) → Eq a b → Eq (f a) (f b)
+cong f Refl = Refl
+
+sym : {A : Set} → {a b : A} → Eq a b → Eq b a
+sym Refl = Refl
+
+trans : {A : Set} → {a b c : A} → Eq a b → Eq b c → Eq a c
+trans Refl Refl = Refl
+
+add-left-id : (a : Nat) → Eq (add Zero a) a
+add-left-id Zero = Refl
+add-left-id (Succ a) = cong Succ (add-left-id a)
+
+succ-left-add : (a b : Nat) → Eq (add (Succ a) b) (Succ (add a b))
+succ-left-add a Zero = Refl
+succ-left-add a (Succ b) = cong Succ (succ-left-add a b)
+
+add-comm : ∀ (a b : Nat) → Eq (add a b) (add b a)
+add-comm a Zero = sym (add-left-id a)
+add-comm a (Succ b) = trans (cong Succ (add-comm a b)) (sym (succ-left-add b a))

examples/nat.rs

@@ -0,0 +1,90 @@
+use std::rc::Rc;
+use std::marker::PhantomData;
+
+pub enum __Impossible {}
+
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub enum Nat {
+    Zero,
+    Succ(Rc<Nat>),
+}
+
+use Nat::{Zero, Succ};
+
+pub fn add(n: Rc<Nat>, m: Rc<Nat>) -> Rc<Nat> {
+    match (&*n, &*m) {
+        (_, Zero) => n.clone(),
+        (_, Succ(m)) => Rc::new(Succ(add(n.clone(), m.clone()))),
+    }
+}
+
+// Erased everything except the A: Set type parameter, which *does* have a useful equivalent
+pub enum Eq<A> {
+    Refl,
+    // Rust doesn't like unused type parameters :(
+    __Impossible(__Impossible, PhantomData<A>),
+}
+
+use Eq::Refl;
+
+// Set arguments lifted to type parameters, implicit arguments are made explicit
+pub fn cong<A, B>(a: Rc<A>, b: Rc<A>, f: Rc<dyn Fn(Rc<A>) -> Rc<B>>, eq: Rc<Eq<A>>) -> Rc<Eq<B>> {
+    match (&*a, &*b, &*f, &*eq) {
+        (_, _, _, Refl) => Rc::new(Refl),
+        _ => unreachable!(),
+    }
+}
+
+pub fn sym<A>(a: Rc<A>, b: Rc<A>, eq: Rc<Eq<A>>) -> Rc<Eq<A>> {
+    match (&*a, &*b, &*eq) {
+        (_, _, Refl) => Rc::new(Refl),
+        _ => unreachable!(),
+    }
+}
+
+pub fn trans<A>(a: Rc<A>, b: Rc<A>, c: Rc<A>, eq1: Rc<Eq<A>>, eq2: Rc<Eq<A>>) -> Rc<Eq<A>> {
+    match (&*a, &*b, &*c, &*eq1, &*eq2) {
+        (_, _, _, Refl, Refl) => Rc::new(Refl),
+        _ => unreachable!(),
+    }
+}
+
+pub fn add_left_id(a: Rc<Nat>) -> Rc<Eq<Nat>> {
+    match (&*a, ) {
+        (Zero, ) => Rc::new(Refl),
+        (Succ(a), ) => cong(add(Rc::new(Zero), a.clone()), a.clone(), Rc::new(|n| Rc::new(Succ(n))), add_left_id(a.clone())),
+    }
+}
+
+pub fn succ_left_add(a: Rc<Nat>, b: Rc<Nat>) -> Rc<Eq<Nat>> {
+    match (&*a, &*b) {
+        (_, Zero) => Rc::new(Refl),
+        (_, Succ(b)) => cong(add(Rc::new(Succ(a.clone())), b.clone()), Rc::new(Succ(add(a.clone(), b.clone()))), Rc::new(|n| Rc::new(Succ(n))), succ_left_add(a.clone(), b.clone())),
+    }
+}
+
+pub fn add_comm(a: Rc<Nat>, b: Rc<Nat>) -> Rc<Eq<Nat>> {
+    match (&*a, &*b) {
+        (_, Zero) => sym(add(b.clone(), a.clone()), add(a.clone(), b.clone()), add_left_id(a.clone())),
+        (_, Succ(b)) => trans(
+            Rc::new(Succ(add(a.clone(), b.clone()))),
+            Rc::new(Succ(add(b.clone(), a.clone()))),
+            add(Rc::new(Succ(b.clone())), a.clone()),
+            // Eq (Succ (add a b))) (Succ (add b a))
+            cong(
+                add(a.clone(), b.clone()),
+                add(b.clone(), a.clone()),
+                Rc::new(|n| Rc::new(Succ(n))),
+                // Eq (add a b) (add b a)
+                add_comm(a.clone(), b.clone())),
+            // Eq (Succ (add b a)) (add (Succ b) a)
+            sym(
+                add(Rc::new(Succ(b.clone())), a.clone()),
+                Rc::new(Succ(add(b.clone(), a.clone()))),
+                // Eq (add (Succ b) a) (Succ (add b a))
+                succ_left_add(b.clone(), a.clone()))),
+    }
+}
+
+// To get the compiler to shut up
+fn main() {}

examples/records.agda

@@ -0,0 +1,14 @@
+record Pair (A B : Set) : Set where
+  field
+    fst : A
+    snd : B
+
+record Foo (A : Set) : Set where
+  field
+    foo : Pair A A
+
+mk-foo : {A : Set} → A → Foo A
+mk-foo x = record
+  { foo = record
+    { fst = x
+    ; snd = x } }

examples/records.rs

@@ -0,0 +1,25 @@
+pub struct Pair<A, B> {
+    pub fst: ::std::rc::Rc<A>,
+    pub snd: ::std::rc::Rc<B>,
+    // Can be ommitted, as both `A` and `B` appeared in a field
+    pub _phantom: ::std::marker::PhantomData<(A, B)>,
+}
+
+pub struct Foo<A> {
+    pub foo: ::std::rc::Rc<Pair<A, A>>,
+    // Can be ommitted, as `A` appeared in a field
+    pub _phantom: ::std::marker::PhantomData<A>,
+}
+
+pub fn mk_foo<A>(param0: ::std::rc::Rc<A>) -> ::std::rc::Rc<Foo<A>> {
+    match (param0, ) {
+        (x, ) => ::std::rc::Rc::new(Foo::<A> {
+            foo: ::std::rc::Rc::new(Pair::<A, A> {
+                fst: x.clone(),
+                snd: x.clone(),
+                _phantom: ::std::marker::PhantomData,
+            }),
+            _phantom: ::std::marker::PhantomData,
+        }),
+    }
+}

examples/sum.agda

@@ -0,0 +1,6 @@
+data Sum (A B : Set) : Set where
+  Inj1 : A → Sum A B
+  Inj2 : B → Sum A B
+
+data UnusedExample (A B : Set) : Set where
+  OnlyLeft : A → UnusedExample A B

examples/sum.rs

@@ -0,0 +1,20 @@
+struct __InternalEmpty;
+pub struct __InternalEmptyCase<T>(::std::marker::PhantomData<T>, __InternalEmpty);
+
+pub enum Sum<A, B> {
+    Inj1(A),
+    Inj2(B),
+    // Can be ommitted, as `A` appeared in a variant
+    Empty(__InternalEmptyCase<(A, B)>),
+}
+
+pub use Sum::{Inj1, Inj2};
+
+pub enum UnusedExample<A, B> {
+    OnlyLeft(A),
+    // Can not be omitted, as `B` did *not* appear in a variant
+    // Could be simplified to __InternalEmptyCase<B>
+    Empty(__InternalEmptyCase<(A, B)>),
+}
+
+pub use UnusedExample::{OnlyLeft};