(a) As others have said, Haskell's type system is certainly now powerful enough to express any constraint you throw at it. (b) Almost directly related to that,

(a) As others have said, Haskell's type system is certainly now powerful enough to express any constraint you throw at it. (b) Almost directly related to that, the less powerful your constraint language the more analyzable it is. I don't necessarily know that Q has these properties, but by constraining how complex the restrictions it encodes are it becomes more amenable to analysis. At first blush, it looks like you'd probably be able to throw a SMT solver at it quite easily.