You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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).
The text was updated successfully, but these errors were encountered:
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?)
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.
see for instance: https://github.com/johnynek/bosatsu/pull/1163/files#diff-25a462d709b48d25e8d8d95909ecad8339382ba129c10995a5e7a45e62b7f2b1R76
I had values like:
but then using them like:
wouldn't typecheck. Then I defined a function like:
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 toforall 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 callhide(x)
and we know the type ofx
, then we should be able to instantiatea := typeof(x)
.The text was updated successfully, but these errors were encountered: