<div>In the below &quot;head&quot; procedure,  [(Datum d) (Done &#39;EOS d)] does not type check.  I&#39;m not sure how I inform the type checker to just &quot;lift&quot; d to type (Option D).</div><div><br></div><div>#lang typed/racket/base</div>
<div><br></div><div>(require racket/match)</div><div><br></div><div>;; Input stream of datum D</div><div>(define-type (Stream D) (U (Datum D) &#39;Nothing &#39;EOS))</div><div><br></div><div>(struct: (D) Datum ([iota : D]))</div>
<div><br></div><div>;; Iteratee</div><div>(define-type (Iteratee D A) (U (Done D A) (Continuation D A)))</div><div><br></div><div>(struct: (D A) Done ([stream : (Stream D)] [accum : A]))</div><div><br></div><div>(struct: (D A) Continuation </div>
<div>  ([resume : ((Stream D) -&gt; (U (Done D A) (Continuation D A)))])) ;; ... -&gt; (Iteratee D A)</div><div><br></div><div>(: run (All (D A) (Iteratee D A) -&gt; A))</div><div>(define (run iter)</div><div>  (match iter</div>
<div>    [(Done _ accum)        accum]</div><div>    [(Continuation resume) (run (resume &#39;EOS))]))</div><div><br></div><div>(: iterator (All (D A) (Listof D) (Iteratee D A) -&gt; (Iteratee D A)))</div><div>(define (iterator lst iter)</div>
<div>  (match (cons lst iter)</div><div>    [(cons &#39;() i)           i]</div><div>    [(cons _ (Done _ _))    iter]</div><div>    [(cons (list-rest x xs) (Continuation k)) (iterator xs (k (Datum x)))]))</div><div><br></div>
<div>(: counter (All (D) (-&gt; (Iteratee D Integer))))</div><div>(define (counter)</div><div>  (: step (Integer -&gt; ((Stream D) -&gt; (Iteratee D Integer))))</div><div>  (define (step n)</div><div>    (ë: ((str : (Stream D)))</div>
<div>      (match str</div><div>        [(Datum _) (Continuation (step (add1 n)))]</div><div>        [&#39;Nothing  (Continuation (step n))]</div><div>        [&#39;EOS      (Done &#39;EOS n)])))</div><div>  (Continuation (step 0)))</div>
<div><br></div><div>;; e.g. (run (iterator &#39;(1 2 3) ((inst counter Integer))))</div><div><br></div><div>(: drop (All (D) Integer -&gt; (Iteratee D Void)))</div><div>(define (drop n)</div><div>  (: step (-&gt; ((Stream D) -&gt; (Iteratee D Void))))</div>
<div>  (define (step) </div><div>    (ë: ((str : (Stream D)))</div><div>      (match str</div><div>        [(Datum _) (drop (sub1 n))]</div><div>        [&#39;Nothing  (Continuation (step))]</div><div>        [&#39;EOS      (Done &#39;EOS (void))])))</div>
<div>  (if (zero? n)</div><div>      (Done &#39;Nothing (void))</div><div>      (Continuation (step))))</div><div><br></div><div>(: head (All (D) (-&gt; (Iteratee D (Option D)))))</div><div>(define (head)</div><div>  (: step (-&gt; ((Stream D) -&gt; (Iteratee D (Option D)))))</div>
<div>  (define (step)</div><div>    (ë: ((str : (Stream D)))</div><div>      (match str</div><div>        [(Datum d) (Done &#39;EOS d)]</div><div>        [&#39;Nothing  (Continuation (step))]</div><div>        [&#39;EOS      (Done &#39;EOS #f)])))</div>
<div>  (Continuation (step)))</div>