| HasCallStack is an operational annotation that has no place in declarative | type signatures I'm not sure I really agree with that. There is a rich literature on effect systems, which decorate types with information about what effects the function has: exceptions, divergence, IO, and the like. So type like head :: Partial => [a] -> a where 'Partial =>' expresses the fact that calling this function might lead to a call of 'error' doesn't seem inherently something that doesn't belong in a type system. Indeed if `error :: Partial => String -> a`, then we can guarantee that any function that calls error will need a Partial constraint... it propagates upward as it should. TL;DR none of this seems (to me) inappropriate for a declarative type system. Simon