<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>