Some Types are not fully expanded

wilbowma commented 4 years ago

It looks like some types, namely universes (surprise surprise) are not fully expanded when they are matched against their pattern expanders. I'm guessing this happens because universes store their types unexpanded since they need to be expanded lazily. Unfortunately, the pattern expanded for universes doesn't first expand the type.

This causes a problem if anyone tries to extend universes, creating a type that expands to a universe, as I just did.

(define-typed-syntax Type
  [(_ s:layer n:nat) Γë½
   #:with n+1 (+ (syntax-e #'n) 1)
   ---------------------
   [Γë╗ #,(syntax-property
         (syntax-property (cur-expand #'(Type- n)) 'layer (syntax->datum #'s))
         ':
         #'(Type s n+1))]])

I have a fix, but I think the root cause is that we need better Turnstile abstractions for universes.

@stchang

stchang commented 4 years ago

Yes this is a known problem.

If you look at current-typecheck-relation it has to check for both unexpanded and unexpanded Type too. So your hack is reasonable. Not sure how to handle it with the current Racket macro system.

stchang commented 4 years ago

solving https://github.com/wilbowma/cur/issues/90 (or https://github.com/wilbowma/cur/issues/37) would also help with this?

wilbowma / cur

Some Types are not fully expanded #133