fix issue #169 #170

AlexKnauth · 2015-08-02T17:58:42Z

fixes #169

pnwamk · 2015-08-02T18:06:33Z

typed-racket-lib/typed-racket/types/subtype.rkt

@@ -266,7 +266,7 @@
         ;; [(_ (Univ:)) A0]
         ;; error is top and bot


So, does this mean this comment here is no longer true?

I think so. I think it means that it is only top now. I'm not sure why it would be bot in the first place, but changing this seems to break more tests, so I'm not sure how this should work.

samth · 2015-08-05T23:00:18Z

This is not the right change. Error is intended to be allowable anywhere, and only generated when there is a type error to prevent additional downstream type errors. If in #169 there's an Error generated, then we should figure out why there's no type error resulting from that.

AlexKnauth · 2015-08-05T23:44:57Z

Ok. I just hadn't expected the subtype check here (https://github.com/AlexKnauth/typed-racket/blob/fix/typed-racket-lib/typed-racket/infer/infer-unit.rkt#L483) to succeed, and that was what caused #169 .

I'll look for another way to solve this then.

AlexKnauth · 2015-08-05T23:50:42Z

@samth Is the parse-type here (

typed-racket/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt

Line 570 in 0c1d58a

(define rep-ty (parse-type (attribute form.rep-type)))

) the right way to do this?

Could that be what's causing Error to appear here for user-defined types? Is there a better way of doing this that avoids that?

AlexKnauth · 2015-08-06T02:02:04Z

Re: parse-type, maybe not. I put a printf in there, and parse-type is returning the right thing (Pos not Error). So I have no idea where the Error type is coming from.

AlexKnauth · 2015-08-12T16:07:41Z

Nope. I was wrong. parse-type is returning Error, but I got thrown off because it was printing as Pos, even though it matches the pattern (Error:). So, is there something else I should be using instead of parse-type?

samth · 2015-08-12T16:12:33Z

The printing issue is almost certainly because we end up with Pos aliased to Error.

Do you know why parse-type is failing?

AlexKnauth · 2015-08-12T16:13:24Z

No I don't.

samth · 2015-08-12T16:14:19Z

I think that's the first thing to investigate.

AlexKnauth · 2015-08-12T16:37:54Z

It seems like the Error type (still printed as Pos) is in the mapping table before I even call parse-type, and that's where it's coming from. But how did that get there?

AlexKnauth · 2015-08-12T16:54:02Z

Oh. It gets filled with all error types, and then replaced with the correct types later.

AlexKnauth · 2015-08-12T20:47:42Z

Ok I took a completely different approach and it's working now.

AlexKnauth · 2015-08-12T21:05:59Z

typed-racket-test/fail/issue-169-2.rkt

@@ -0,0 +1,10 @@
+#;
+(exn-pred #rx"expected: (Listof Nothing).*given: (Listof Pos*)")


Oh, except the parens and * probably aren't good in the regexp there.

AlexKnauth · 2015-08-12T21:54:21Z

How does this look now?

samth · 2015-08-14T13:34:11Z

typed-racket-lib/typed-racket/base-env/base-types-extra.rkt

@@ -17,7 +17,7 @@
 (define-other-types
  -> ->* case-> U Rec All Opaque Vector
  Parameterof List List* Class Object Values Instance Refinement
-  pred Struct Struct-Type Prefab Top Bot)
+  pred Struct Struct-Type Prefab Top Bot Distinction)


Why is this now exposed to users? What does it correspond to?

It's not; that's what this except-in is for: https://github.com/racket/typed-racket/pull/170/files#diff-be2db6e0db44e2e94aa8b096cd9b3850R21

Ok, now I think I understand. Why not create a new internal form, instead of a new type constructor that isn't exposed?

I couldn't think of any other way to allow both new-subtypes to refer to type aliases and for other forms to refer to new-subtypes properly.

But actually, this still is broken, in this example:

#lang typed/racket/base (define-new-subtype Lst (make-Lst (U Null (Pairof Elt Lst)))) (define-new-subtype Elt (make-Elt (U Symbol Lst))) (: cns : Elt Lst -> (Pairof Elt Lst)) (define cns (inst cons Elt Lst)) (: lst : Elt * -> Lst) (define (lst . args) (for/fold ([lst (make-Lst '())]) ([elt (in-list (reverse args))]) (make-Lst (cns elt lst))))

With this error highlighting the lst in the for/fold accumulator:

. Type Checker: type mismatch expected: Lst given: Lst in: lst

I guess I'm confused why the work done by this define-type-alias form can't be done manually in define-new-subtype/pass1.

Also, I am not sure that we even want to support recursive uses of new-subtype like this.

Oh it might be because I never allowed Distinction types to be subtypes of themselves.

Nope, still broken, even with that.

Probably @takikawa is the right person to help with recursive aliases.

Ok I just fixed it. There was a missing call to resolve in there, and that fixed it. I also added a version of that example as another test.

AlexKnauth · 2015-08-15T03:12:29Z

The travis build is passing now, thanks to #175

pnwamk reviewed Aug 2, 2015
View reviewed changes

AlexKnauth force-pushed the fix branch 2 times, most recently from a1190e1 to 50a7294 Compare August 12, 2015 20:26

AlexKnauth force-pushed the fix branch from 50a7294 to 5e8f316 Compare August 12, 2015 21:03

AlexKnauth reviewed Aug 12, 2015
View reviewed changes

AlexKnauth force-pushed the fix branch from 5e8f316 to 92e2e75 Compare August 12, 2015 21:11

samth reviewed Aug 14, 2015
View reviewed changes

AlexKnauth force-pushed the fix branch 2 times, most recently from 6104fe0 to 47266cf Compare August 14, 2015 18:06

AlexKnauth added 2 commits August 14, 2015 21:42

fix issue racket#169

f8cc9e8

Add error message specifications

af2c22f

AlexKnauth force-pushed the fix branch from 47266cf to af2c22f Compare August 15, 2015 02:42

AlexKnauth merged commit af2c22f into racket:master Aug 15, 2015

AlexKnauth deleted the fix branch August 15, 2015 04:02

		@@ -266,7 +266,7 @@
		;; [(_ (Univ:)) A0]
		;; error is top and bot

		@@ -0,0 +1,10 @@
		#;
		(exn-pred #rx"expected: (Listof Nothing).given: (Listof Pos)")

Uh oh!

fix issue #169 #170

fix issue #169 #170

Uh oh!

Conversation

AlexKnauth commented Aug 2, 2015

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

samth commented Aug 5, 2015

Uh oh!

AlexKnauth commented Aug 5, 2015

Uh oh!

AlexKnauth commented Aug 5, 2015

Uh oh!

AlexKnauth commented Aug 6, 2015

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

samth commented Aug 12, 2015

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

samth commented Aug 12, 2015

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AlexKnauth commented Aug 12, 2015

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AlexKnauth commented Aug 15, 2015

Uh oh!

Uh oh!