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.