newly defined subtype doesn't play well as part of union

[philnguyen]

What version of Racket are you using?

v6.6.0.2

What program did you run?

#lang typed/racket/base
(define-new-subtype New-Int (integer->new-int Integer))
(define-type T (U String New-Int))
(ann (integer->new-int 42) T)

What should have happened?

The above program's last line does not type check.

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

; Type Checker: type mismatch
;   expected: T
;   given: New-Int
;   in: (integer->new-int 42)

[AlexKnauth]

One thing might be causing this. The way the sub-typing code is written, when it sees a define-new-subtype type like New-Int, it checks the type it was based on, in this case Integer. If it does that before checking for unions, that could cause problems like this one. On the other hand if it checks for unions first, it could miss cases where a define-new-subtype is based on a union type.

So I'm not sure what exactly it should do.

Anyone else, is there a way to make it check for both of those cases?

[pnwamk]

This issue is something intersections sort of have to worry about already (they distribute themselves over Unions and then are checked first in subtyping, which together solves the issue).

I think the best solution would be to re-implement Distinctions as Opaque types that have no predicate -- then the function which produces values of the distinction type simply produces an intersection of the original type and the new Opaque type.

For example, for New-Int:

lang typed/racket/base

(define-new-subtype New-Int (integer->new-int Integer))

'New-Int' would be a new Opaque type, and the function this creates (integer->new-int) would be a function of type (All (A) (∩ A Integer) -> (∩ A New-Int)) (or similar).

I'll see if I can't throw something together that does this tonight or tomorrow morning and report.

-Andrew

On Sun, Jul 17, 2016 at 6:33 PM Alex Knauth notifications@github.com wrote:

One thing might be causing this. The way the sub-typing code is written, when it sees a define-new-subtype type like New-Int, it checks the type it was based on, in this case Integer. If it does that before checking for unions, that could cause problems like this one. On the other hand if it checks for unions first, it could miss cases where a define-new-subtype is based on a union type.

So I'm not sure what exactly it should do.

Anyone else, is there a way to make it check for both of those cases?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/typed-racket/issues/408#issuecomment-233208159, or mute the thread https://github.com/notifications/unsubscribe-auth/ADfg6vvv61U9bOONTb5iUJZZ03X9XcOdks5qWq2ygaJpZM4JOVAH .

[AlexKnauth]

Do you mean that a Distinction type based on Integer could be replaced by (∩ Integer Opaque-New-Int)?

[pnwamk]

Yes.

On Mon, Jul 18, 2016 at 5:35 PM Alex Knauth notifications@github.com wrote:

Do you mean that a Distinction type based on Integer could be replaced by (∩ Integer Opaque-New-Int)?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/racket/typed-racket/issues/408#issuecomment-233466250, or mute the thread https://github.com/notifications/unsubscribe-auth/ADfg6v-A2KsrofQHS3WjGF4ahL-TJo2hks5qW_GBgaJpZM4JOVAH .