[racket] typed racket, filters, and polymorphism

What I’m trying to accomplish is something more like this:
#lang typed/racket

(require "dimensions.rkt")

(struct (d) unit ([name : Any] [scalar : Positive-Real] [dimension : d]) #:transparent
  #:guard (lambda (name scalar dimension _)
            (unless (dimension? dimension)
              (error 'unit "expected Dimension, given ~v" dimension))
            (values name scalar dimension)))

(define-type (Unitof d) (unit d))

(define-type Unit (Unitof Dimension))

(define Unit? (make-predicate Unit))

(define-type Unitish
  (U (Unitof Any)
     Dimension
     Positive-Real))

(: ->unit : (All (d) (case-> [(Unitof d) -> (Unitof d)]
                             [Unitish -> Unit])))
(define (->unit u)
  (cond [(unit? u)
         (unless (Unit? u) ; this should never happen anyway because of the guard
           (error '->unit "expected (Unitof Dimension), given ~v" u))
         u]
        [(dimension? u) (unit u 1 u)]
        [(positive-real? u) (unit u u dimensionless-dimension)]))


On Sep 25, 2014, at 6:19 PM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:

> No, I don't think you can do this. Can you say more about what you're
> trying to accomplish?
> 
> Sam
> 
> On Thu, Sep 25, 2014 at 6:15 PM, Alexander D. Knauth
> <alexander at knauth.org> wrote:
>> Do any of you have any advice for getting a function like this to
>> type-check?
>> #lang typed/racket
>> 
>> (: check-int : (All (a) (case-> [a -> a]
>>                                [Any -> Integer])))
>> (define (check-int int)
>>  (unless (exact-integer? int)
>>    (error 'check-int "expected Integer, given ~v" int))
>>  int)
>> 
>> ;. Type Checker: type mismatch
>> ;  expected: a
>> ;  given: Integer in: int
>> 
>> 
>> 
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
>> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140925/dc09b97f/attachment.html>