Some types seem somewhat unusable

[johnynek]

see for instance: https://github.com/johnynek/bosatsu/pull/1163/files#diff-25a462d709b48d25e8d8d95909ecad8339382ba129c10995a5e7a45e62b7f2b1R76

I had values like:

refl_Int: Sub[forall a. a, Int] = refl_sub
refl_any: Sub[forall a. a, exists a. a] = refl_sub
refl_any1: Sub[exists a. a, exists a. a] = refl_sub

but then using them like:

ignore = (refl_Int, refl_any)

wouldn't typecheck. Then I defined a function like:

def hide(a) -> exists b. b: a

ignore = [hide(refl_Int), hide(refl_any)]

and that fails too.

I am starting to wonder if the extensions I've made to the type system basically mean some values are unusable. It could also just be some lurking bugs with existential types.

But a message like type ?211 does not subsume type forall a: *. a seems like we need to set a metavar to forall a. a but that's not possible because metavars must be rho types.

It seems like it should be trivial that if hide: forall a. (a -> exists. b. b) and we call hide(x) and we know the type of x, then we should be able to instantiate a := typeof(x).

[johnynek]

a related issue is that:

x = (a, b, c, ...)

should always typecheck, if everything before that type checks. I was surprised I couldn't even put these values in a tuple and have it typecheck. This is similar to:

struct Box(a)
x = Box(y)

should always compile and produce a good type. I imagine this is also failing for either existential or universal quantification or both (maybe when existentials are in covariant position or universals are in contravariant positions?)

[johnynek]

If we look at line 577 of rankn/Type.scala there is a todo about handling shadowing of ForAll types. It could be that if we handle this using the algorithm of #1126 then this issue would also be solved. My guess is based on the idea that types are often automatically assigned starting with a, b, c... so collisions are somewhat frequent in practice. So this may be blocking substitution from working just because we don't unshadow the types at that stage.

We could check this theory cheaply by throwing an exception in that branch and seeing how often it fails.