Missing error message for trying to define generic unions

[HalflingHelper]

union TwoList<K, V> {
  nil
  vnode(V, TwoList)
  knode(K, TwoList)
}


postulate tl_induction : all T: type, E : type.
  all P : fn TwoList<T, E> -> bool.
  if P(nil) and (all k : T, tl : TwoList<T, E>. if P(tl)  then P(knode(k, tl)))
  then all x : TwoList<T, E>. P(x)

I ran into this while working on induction stuff, ignore the weird theorem, the error is

Exception: /home/calvin/Documents/Programming/343/deduce/blah.pf:38.75-38.77: expected a term of type TwoList
but got term tl of type TwoList<T,E>

        in context of call knode(k, tl)
        function type: (fn <K,V> K, TwoList -> TwoList<K,V>)
        inferred type arguments: K := T, V := E

The solution of course is to change the TwoList in the union declaration to TwoList<K, V>. Maybe it is important to have the ability to not instantiate types, but I would hazard a guess that this shouldn't be allowed. If so we should probably catch this error at the union declaration instead of when typechecking theorems.

It's also possible to do stuff where we swap the order of type parameters, making it impossible(?) to create a recursive function on the union.

union TwoList<K, V> {
  nil
  vnode(V, TwoList<V, K>)
  knode(K, TwoList<K, V>)
}

Again I'm not sure if we should do something about this.

[jsiek]

I agree that it shouldn't be allowed.

[HalflingHelper]

@jsiek While I'm at it, should something like this also error?

union broken {
    b(broken)
}

It's possible to define a non-terminating function, but impossible to call it concretely.

[HalflingHelper]

Also upon further reflection, the last example is probably ok? Like can maybe make sense

union No<K, V> {
    nil
    th(No<K, V>)
    sh(No<V, K>)
}


recursive f<T, E>(No<T, E>) -> No<T, E> {
    f(nil) = nil
    f(th(n)) = f(n)
    f(sh(n)) = sh(n)
}

I think that for now I'll just make sure that recursive parameters have the right number of type params, since something like this DEFINITELY shouldn't work

union No<K, V> {
    nil
    th(No<K>)
}

[jsiek]

Yes to checking for the right number of type params.

I wouldn't worry about the unusable unions and non-terminating functions that can't be called.

[HalflingHelper]

union A<E> {
    a(E)
}

union No<K, V> {
    f(fn (A) -> bool)
}

At first glance, something like this should error too