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.