default   Racket Bugs
Main PageQuick QueryStandard QueryAdvanced QueryHelp
Log in

View Problem Report: 12945

send email to interested parties or send email followup to audit-trail
Reporter's email: ray dot racine at gmail dot com
Number: 12945
Category: typed-scheme
Synopsis: Specific Example Of A Combinator Of Two Poly Functions Failing To Type Check
Class: sw-bug
Responsible: samth
Notify-List:
Severity: non-critical
Priority: medium
State: closed
Confidential: no
Arrival-Date: Fri Jul 27 15:36:02 -0400 2012
Closed-Date: Wed Feb 27 11:17:08 -0500 2013
Last-Modified: Wed Feb 27 11:20:01 -0500 2013
Originator: Ray Racine
Organization: plt
Submitter-Id: unknown
Release: 5.3.0.16--2012-07-23(3bce0729/d/list)
Environment: unix "Linux rpr 3.2.0-27-generic #43-Ubuntu SMP Fri Jul 6 14:25:57 UTC 2012 x86_64 x86_64 x86_64 GNU/Linux" (x86_64-linux/3m) (get-display-depth) = 32
Human Language: english
(current-memory-use) 947689608
Links: (links) = (); (links #:user? #f) = (); (links #:root? #t) = (#<path:/code/racketlib/>); (links #:user? #f #:root? #t) = ()


Collections:
("/home/ray/.racket/5.3.0.16/collects"
(non-existent-path))
("/usr/local/racket/collects"
("string-constants" "mred" "mrlib" "macro-debugger" "mzcom" "raco" "defaults" "plai" "slatex" "setup" "scribble" "srfi" "lang" "config" "mysterx" "future-visualizer" ".gitignore" "json" "icons" "readline" "preprocessor" "typed-racket" "web-server" "picturing-programs" "stepper" "texpict" "xrepl" "compiler" "framework" "wxme" "mzscheme" "plot" "honu" "algol60" "scheme" "trace" "handin-server" "scriblib" "slideshow" "swindle" "games" "typed" "2htdp" "graphics" "sgl" "hierlist" "reader" "deinprogramm" "drscheme" "profile" "at-exp" "xml" "data" "sirmail" "errortrace" "info-domain" "redex" "handin-client" "typed-scheme" "dynext" "html" "planet" "gui-debugger" "version" "rackunit" "r6rs" "eopl" "htdp" "racket" "browser" "frtime" "unstable" "help" "net" "test-engine" "lazy" "r5rs" "syntax" "mzlib" "meta" "drracket" "syntax-color" "s-exp" "racklog" "repo-time-stamp" "make" "scribblings" "parser-tools" "embedded-gui" "tests" "launcher" "teachpack" "db" "rnrs" "schemeunit" "images" "!
file" "ffi" "openssl" "datalog"))

Computer Language: (("Determine language from source") (#(#t print mixed-fraction-e #f #t debug) (default) #() "#lang racket\n" #t #t ((main) (test))))
Description: The following overally long example (sorry for that) fails to type check.

See the following gist.

https://gist.github.com/3156946
File Attachments:
How-To-Repeat: Paste gist code from https://gist.github.com/3156946 in DrRacket.
Uncomment drop1keep1Poly procedure and type checking fails.
Fix:
Release-Note:
Unformatted:

send email to interested parties or send email followup to audit-trail

Audit Trail:

State changed from "open" to "closed" by endobson at Wed, 27 Feb 2013 11:17:08 -0500
Reason>>> Not a bug.

From: Eric Dobson <eric.n.dobson at gmail.com>
To: samth at racket-lang.org, ray.racine at gmail.com, stamourv at racket-lang.org,
        bugs at racket-lang.org
Cc: 
Subject: Re: typed-scheme/12945: Specific Example Of A Combinator Of Two Poly
 Functions Failing To Type Check
Date: Wed, 27 Feb 2013 08:16:37 -0800

 The reason that this fails to typecheck is that it shouldn't, you need
 to rewrite
 
 
 ;;(: drop1keep1Poly (All (D A B) (-> (Iteratee D B))))
 ;;(define (drop1keep1Poly)
 ;;  (seq (drop 1) (λ: ((accum : A)) (head))))
 
 (: drop1keep1Poly (All (D) (-> (Iteratee D (Option D)))))
 (define (drop1keep1Poly)
  (seq ((inst drop D) 1) (λ (x) ((inst head D)))))
 
 The reason is that head returns (Iteratee X (Option X)) which doesn't
 match (Iteratee D B), and you need the lambda to accept the Void
 argument from seq, and annotating it as A, prevents that. Also the
 instantiations are needed because TR's inference is bad at polymorphic
 functions applied to polymorphic functions.