Encoding thunked sequences in Dafny

[kiranandcode]

How can I encode thunked sequences in Dafny? I've come up with the following definition:

datatype Node<T> = Nil | Cons(x:T,tail: () -> Node<T>) 
type Seq<T> = () -> Node<T> 

but I don't think this is exactly what I want because as soon as I try to write functions over the definition, I run into problems:

function contents<T>(s: Seq<T>) : seq<T> {
  match s() {
    case Nil => []
    case Cons(hd,tail) => [hd] + contents(tail)
  }
}

(above Dafny complains that it can not prove that the recursive call is terminating)

I'd like to retain the definition I've given before--- is there some way of adding ghost-state to the datatype definition such that Dafny can reason about it being finite for example?

Apologies for the beginner question, I'm somewhat new to Dafny.

[kiranandcode]

Okay, after some experimentation, I've ended up with the following representation, which seems to capture what I want:

datatype Node<T> = Nil | Cons(x:T,rest: () -> Node<T>) 
type Seq<T> = () -> Node<T> 

predicate modelled_by<T>(s: Seq<T>, model: seq<T>)  {
  match s() {
    case Nil => model == []
    case Cons(hd,rest) => |model| > 0 && model[0] == hd && modelled_by(rest, model[1..])
  }
}

method length<T>(s: Seq<T>, ghost model: seq<T>) returns (res: int)
  requires modelled_by(s, model)
  ensures res == |model| {
  match s() {
    case Nil => res := 0;
    case Cons(hd, rest) =>
      res := length(rest, model[1..]);
      res := res + 1;
  }
}