It's not at all easy in general. Suppose we have
f :: [!a] -> [a] f xs = xs
Does f run down the list, behind the scenes, evaluating each element?
No, because what [!a] means is List !a = ([] | !a : List !a). It does not mean ([] | !(!a : List !a)). Since the Cons thunks are not forced to HNF, the argument type [!a] should mean a lazy list with strict elements. So you would pay the extra expense in a function like length :: [!a] -> Int length [] = 0 length (_:xs) = succ (length xs)
That could be expensive. Would it make any difference if we wrote f :: [!a] -> [a], or f :: [a] -> [!a]? Or does the type mean that f *requires* a list with *already-evaluated* elements?
I don't see it as expensive: the function would do exactly what it's supposed to do, given its declaration. If the declared and inferred types don't match on strictness, the compiler should emit a warning that the declared function type is too strict. As for f :: [a] -> [!a] I'm not sure if this kind of declaration should be treated as a guarantee or an obligation. That is, I'm not sure if the compiler should report an error if the function definition does not actually return a list of elements in HNF, or if it should insert code to force each element to HNF. But I'm mostly concerned about data declarations. See, what bugs me is that it's allowed to declare data Maybe' a = Nothing' | Just' !a data List' a = Nil | Cons' !a (List' a) and then use those to declare data MaybeList1 a = [Maybe' a] data MaybeList2 a = List' (Maybe' a) But now the containers are incompatible mutually and incompatible with [Maybe a]. If strictness annotations were allowed not only at the top level, then [Maybe a], [Maybe !a], [!(Maybe a)], and [!(Maybe !a)] would all be compatible types. And the libraries wouldn't need to provide different version of functions for lazy and strict containers of the same kind.