Mutual recursion does not work with differing type arguments

[antalsz]

Consider the following painfully contrived Haskell code:

module BadMut where

data Nat = Z | S Nat

sink :: Nat -> a -> a
sink Z     x = x
sink (S n) x = sank n x

sank :: Nat -> b -> b
sank Z     x = x
sank (S n) x = sink n x

This is some well-founded mutual recursion (that doesn't do anything). However, thanks to sink taking the type parameter a and sank taking the type parameter b, the translated Coq code doesn't type check:

Inductive Nat : Type := Z : Nat |  S : Nat -> Nat.

Definition sank : forall {b}, Nat -> b -> b :=
  fix sank {b} arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | Z, x => x
           | S n, x => sink n x
           end with sink {a} arg_0__ arg_1__
                      := match arg_0__, arg_1__ with
                         | Z, x => x
                         | S n, x => sank n x
                         end for sank.

Definition sink : forall {a}, Nat -> a -> a :=
  fix sank {b} arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | Z, x => x
           | S n, x => sink n x
           end with sink {a} arg_0__ arg_1__
                      := match arg_0__, arg_1__ with
                         | Z, x => x
                         | S n, x => sank n x
                         end for sink.

In, for example Definition sink : ... := fix sank {b} arg_0__ arg_1__ := ..., we see that b is never referred to, so it is completely ambiguous!

This problem also crops up when the two (or more) functions have different numbers of type arguments.

We can fix this example by simply changing sank :: Nat -> b -> b to sank :: Nat -> a -> a, but it might be possible to get hs-to-coq to get this right. That would probably entail annotating the types of every function argument, something which we've avoided so far. But maybe it'd be good!

[sweirich]

What about moving the type generalization to the toplevel:

Definition sank {b} : Nat -> b -> b :=
  fix sank arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | Z, x => x
           | S n, x => sink n x
           end with sink arg_0__ arg_1__
                      := match arg_0__, arg_1__ with
                         | Z, x => x
                         | S n, x => sank n x
                         end for sank.

[antalsz]

@sweirich Right now, we do that when we can. The issue here is that the two function take different implicit arguments ({a} vs. {b}), so we can't common them up. We currently only put the longest common prefix at the top level.

[sweirich]

Got it. deAnnotate' in CoreSyn.hs is an example that suffers from this limitation.