call/cc + letrec + occurrence typing can be unsound
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 25/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers
Research direction
Start by running the supplied Typed Racket example and tracing how occurrence typing handles letrec-bound variables and inner defines. Determine how the call/cc mutation reaches bar, then add a regression case covering the example. Done means the unsound program is rejected or its occurrence typing is prevented as described.
Written by the indexing model from the issue text.
Description
In the following example, the mutation exposed via the combination of call/cc and letrec can lead to unsoundness via occurrence typing; bar has the type (-> False False) but actually is called with #t. The obvious solution is to disable occurrence typing on letreced variables (including inner defines that are not converted to let).
#lang typed/racket
(define (bar [v : False]) : False
(error "yo" v))
(define-type klk (-> (U klk (List klk Boolean)) (List klk Boolean)))
(define (foo)
(letrec ((x (call/cc (lambda ([k : klk]) : (List klk Boolean) (list k #f)))))
(when (list? x)
(if (false? (second x))
(begin
(call/cc
(lambda ([k : klk])
((first x) (list k #t))))
(bar (second x)))
((first x) x)))))
(foo)
- Dominant language
- Racket
- Stars
- 575
- Forks
- 106
- Avg merge
- 2h 1m
- Merged PRs (30d)
- 2
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from racket/typed-racket
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
racket/typed-racket#1512 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
racket/typed-racket#1505 · 13 comments ·
-
Difficulty 3/5 1-2 days Newbie friendliness 58/100
racket/typed-racket#1516 ·
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
racket/typed-racket#1506 ·
-
Difficulty 4/5 3-5 days Newbie friendliness 30/100
racket/typed-racket#1493 · 1 comment ·
All issues in racket/typed-racket
Similar issues
-
mlir
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
llvm/llvm-project#224908 · 1 comment ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
area-CodeGen-coreclr untriaged
Difficulty 1/5 Under an hour Newbie friendliness 92/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
secondlife/sl-vscode-plugin#147 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
objectionary/phie#149 ·