typed-racket icon indicating copy to clipboard operation
typed-racket copied to clipboard

Internal Typechecker Error: Base type L+ not in predefined-type-table

Open SuzanneSoy opened this issue 9 years ago • 1 comments

What version of Racket are you using?

6.6.0.4

What program did you run?

#lang typed/racket

(define-type (L+ T REST) (Pairof T (∩ (L+ T Any) REST)))

What should have happened?

A better error message. I was fiddling around with types, trying to see if I could describe the type for a pair of same-length lists (I don't think it's possible), so the code above isn't supposed to work anyway.

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

.../share/racket/pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt:270:0: Internal Typechecker Error: Base type L+ not in predefined-type-table
while typechecking:
here
originally:
here

The problematic definition is not highlighted in red (so in a larger file, it would be harder to find), and the "while typechecking: here originally: here" is not particularly helpful :) .

SuzanneSoy avatar Sep 09 '16 11:09 SuzanneSoy

This now compiles with v6.9.0.1. However, running (:type L+) produces the following type, which seems a bit odd:

(All (T REST) (Pairof T (∩ REST (Opaque L+))))

The following simpler example also produces this occurrence of Opaque, is this expected behaviour?

> (define-type (L1 HD TL) (Pairof HD (L1 HD TL)))
> (:type L1)
(All (HD TL) (Pairof HD (L1 HD TL)))
> (define-type (L2 HD TL) (Pairof HD (∩ (L2 HD TL) TL)))
> (:type L2)
(All (HD TL) (Pairof HD (∩ TL (Opaque L2))))

On the last line, I would have expected (All (HD TL) (Pairof HD (∩ TL (L1 HD TL)))). Furthermore, as it stands, this type featuring Opaque seems unusable:

> (define-type (L3 HD TL) (Pairof HD (∩ (U (L3 HD TL) Null) TL)))
> (ann (ann '(1 2 3)
            (Pairof Integer
                    (∩ (Pairof Integer
                               (∩ (Pairof Integer
                                          (∩ Null Any))
                                  Any))
                       Any)))
       (L3 Integer Any))
  Type Checker: type mismatch
  expected: (L3 Integer Any)
  given: (List Integer Integer Integer) in: (quote (1 2 3))
> (make-predicate (L3 Integer Any))
  type-check: type name used out of context
  type: L3
 in: L3 in: L3

Should I close this and open separate issues?

SuzanneSoy avatar Apr 19 '17 22:04 SuzanneSoy