`check`ing of template expressions with an expected projected type results in an unmatched cases

[molenzwiebel]

I'd expect the following to typecheck (given that ... can produce any value), but it instead results in the classic "Missing a cases branch pattern errored."):

type Id<T> = T

a :: Id<Number> = 1   # fine
a :: Id<Number> = ... # error

Interestingly, this error also happens if you instantiate a non-forall type:

a :: Number<Number> = 1   # Number is not assignable to Number<Number>
a :: Number<Number> = ... # missing a cases branch

As an aside, is it intentional that forall type instantiation works even on non-forall types? I'd have expected Number<Number> to fail in the above snippet, not the assign check.

[jpolitz]

That just seems like a bug, plus a bad error message, in the type checker. Thanks for finding that!

I don't think the cases arity error has anything to do with the type instantiation, it's just a bug with …

Regarding Number<Number> I think we'd prefer if this program was not well-formed in the type-checker:

fun f(n :: Number<Number>) -> Number<Number>: n end

So I'm willing to call that a bug, too.

On Tue, Jun 01, 2021 at 11:43 AM, Thijs Molendijk @.***> wrote:

I'd expect the following to typecheck (given that ... can produce any value), but it instead results in the classic "Missing a cases branch pattern errored."):

type Id<T> = T

a :: Id<Number> = 1 # fine a :: Id<Number> = ... # error

Interestingly, this error also happens if you instantiate a non-forall type:

a :: Number<Number> = 1 # Number is not assignable to Number<Number> a :: Number<Number> = ... # missing a cases branch

As an aside, is it intentional that forall type instantiation works even on non-forall types? I'd have expected Number<Number> to fail in the above snippet, not the assign check.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/brownplt/pyret-lang/issues/1594, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAA5IU2BGLQGLQMTDKW4LRTTQUS4XANCNFSM455GNUSQ .