Idea for codata syntax in Haskell

Coinduction.hs

-- Inspired by http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf

[codata|
  codata Stream a where
    head :: Stream a -> a
    tail :: Stream a -> Stream a
|]

fib :: Stream Nat
[copattern|
  head fib        = Z
  head (tail fib) = S Z
  tail (tail fib) = zipWith plus fib (tail fib)
|]


-- should translate roughly into:

data StreamOut t where
  Head :: StreamOut (Stream a -> a)
  Tail :: StreamOut (Stream a -> Stream a)

-- `Coinductive ds` denotes a set of evaluation rules for a data type
-- defined by its destructors `ds`.
newtype Coinductive ds a =
    Coinduction { run :: forall r. ds (Coinductive ds a -> r) -> r }
type Stream = Coinductive StreamOut

head xs = run xs Head
tail xs = run xs Tail

fib :: Stream Nat
fib = Coinduction $ \case
  Head -> Z
  Tail -> Coinduction $ \case
    Head -> S Z
    Tail -> zipWith plus fib (tail fib)