Lifting should not duplicate types containing (co)matches

[timsueberkrueb]

Consider the following example:

codata Fun(a b: Type) {
    Fun(a, b).ap(a b: Type, x: a): b
}

codata Forall(p: Type -> Type) {
    Forall(p).forall_ap(p: Type -> Type, x: Type): p.ap(Type, Type, x)
}

let id: Forall(\a. a -> a) {
    comatch { .forall_ap(_, _) => \x.x }
}

When lifting all comatches using cargo run -- lift Forall the_example_above.pol, it generates the following program:

codata Fun(a b: Type) {
    Fun(a, b).ap(a b: Type, x: a): b
}

codata Forall(p: Type -> Type) {
    Forall(p).forall_ap(p: Type -> Type, x: Type): p.ap(Type, Type, x)
}

let id: Forall(\a. a -> a) {MkForall1}

codef MkForall1: Forall(\a. Fun(a, a)) { .forall_ap(x, x0) => \x3. x3 }

In this program, the typechecker compares the type of id with the type of MkForall1. However, since \a. a -> a resp. \a. Fun(a, a) occur in different source code locations, unification is not allowed.

[BinderDavid]

This program should work, but it doesn't:

codata Fun(a b: Type) {
    Fun(a, b).ap(a b: Type, x: a): b
}

codata Forall(p: Type -> Type) {
    Forall(p).forall_ap(p: Type -> Type, x: Type): p.ap(Type, Type, x)
}

#[transparent]
let generated : Fun(Type, Type)  {
    \a. a -> a
}

let id: Forall(generated) {MkForall1}

codef MkForall1: Forall(generated) { .forall_ap(x, x0) => \x3. x3 }

[BinderDavid]

Also:

use "../std/data/eq.pol"
use "../std/data/bool.pol"
use "../std/codata/fun.pol"


#[transparent]
let foo : Fun(Bool, Bool)  {
    \x. x
}

let proof: Eq(Fun(Bool, Bool), foo, foo) {
    Refl(Fun(Bool,Bool), foo)
}