Some Types are not fully expanded

[wilbowma]

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]

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]

solving #90 (or #37) would also help with this?