\nonstopmode
\documentclass{article}
\usepackage{pifont}
\usepackage[utf8x]{inputenc}

\usepackage{latex/agda}
\DeclareUnicodeCharacter{738}{$^\mathsf{s}$}
\DeclareUnicodeCharacter{8759}{::}

\setlength{\mathindent}{0pt}

\begin{document}
\begin{code}

{-# OPTIONS --copatterns --sized-types #-}

postulate
  Size   : Set
  Size<_ : Size → Set
  ↑_     : Size → Size
  ∞      : Size

{-# BUILTIN SIZE    Size   #-}
{-# BUILTIN SIZELT  Size<_ #-}
{-# BUILTIN SIZESUC ↑_     #-}
{-# BUILTIN SIZEINF ∞      #-}

data List (A : Set) : Set where
  [] : List A
  _∷_ : (x : A) (xs : List A) -> List A

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

-- Sized streams via head/tail.

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head  : A
    tail  : ∀ {j : Size< i} → Stream {j} A
open Stream public

-- Streams and lists.

-- Prepending a list to a stream.

_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[]        ++ˢ s = s
(a ∷ as)  ++ˢ s = a ∷ (as ++ˢ s)

-- Unfold which produces several outputs at one step

record List1 (A : Set) : Set where
  constructor _∷_
  field
    first  : A
    rest   : List A
open List1 public

unfold⁺ : ∀ {S : Size → Set} {A : Set}

  (step : ∀ {i} → S i → List1 A × (∀ {j : Size< i} → S j)) →

  ∀ {i} → (s : S i) → Stream {i} A

head  (unfold⁺ step s) =  first (fst (step s))
tail  (unfold⁺ step s) =  let  ((_ ∷ l) , s′) = step s
                          in   l ++ˢ unfold⁺ step s′
\end{code}
Problem: The ∷ in the last let statement is not colored with constructor color.
\end{document}