Strange behaviors of match's or pattern

[NoahStoryM]

What version of Racket are you using?

v7.8

What program did you run?

Program 1:

#lang typed/racket
(define-type Type (U Number Symbol))
(ann (lambda (arg)
       (match arg
         [(or (? number? x)
              (? symbol? x))
          x]))
     [-> Type Type])

Program 2:

#lang typed/racket
(define-type Variable (Refine [var : Symbol] (! var 'λ)))
(define-predicate variable? Variable)
(define-type Type (U Number Variable))
(ann (lambda (arg)
       (match arg
         [(or (? number? x)
              (? variable? x))
          x]))
     [-> Type Type])

Program 3:

#lang typed/racket
(define-type Variable (Refine [var : Symbol] (! var 'λ)))
(define-predicate variable? Variable)
(define-type Type (U Number Variable (Listof Type)))
(ann (lambda (arg)
       (match arg
         [(or (? number? x)
              (? variable? x))
          x]))
     [-> Type Type])

What should have happened?

Print a procedure.

If I change or pattern to 2 different patterns in match, the above codes will work properly.

(match arg
  [(? number? x) x]
  [(? variable? x) x])

If you got an error message, please include it here.

Program 1: Why could x be False type?

Type Checker: type mismatch
  expected: Type
  given: (U False Type)
  in: x

Program 2: Why could x be Symbol type instead of Variable type?

Type Checker: type mismatch
  expected: Type
  given: (U Complex False Symbol)
  in: x

Program 3: The program stucks in an endless loop.

[capfredf]

Match is not well supported in Typed Racket, because it is too complicated. I would use cond or if to do this kind of reasoning.

(match arg
  [(? number? x) x]
  [(? variable? x) x])

(match arg
         [(or (? number? x)
               (? variable? x))
          x])

Though the behaviors of two expressions are the same, their fully expanded code is different. The first roughly amounts to

(let-values ([(flag res) (cond 
                          [(number? arg)
                           (values #t arg)]
                          [(string? arg) (values #t arg)])])
 (if flag res
   (error 'hello)))

The second:

(let-values ([(flag res) (cond
                          [(number? arg)
                           (values #t arg)]
                          [(string? arg) (values #t arg)]
                          [else (values #f #f)])])
  (if flag res
        (error 'hello)))

[samth]

I would just say that it's or patterns that aren't well supported, but yes this is an issue of the pattern match expands to not being comprehensible to TR.

[NoahStoryM]

Subtype may affect or pattern's behavior:

Following codes work:

#lang typed/racket

(struct A ())
(struct B ([val : A]))

(match (A)
  [(or (B val)) (ann val A)]
  [_ 'done])

print:

'done

#lang typed/racket

(struct A ())
(struct B A ([val : A]))

(match (B (A))
  [(or (B val)) (ann val A)]
  [_ 'done])

print:

#<A>

But following codes fail:

#lang typed/racket

(struct A ())
(struct B A ([val : A]))

(match (A)
  [(or (B val)) (ann val A)]
  [_ 'done])

error messages:

Type Checker: type mismatch
  expected: A
  given: (U A False)
  in: val