The pattern p is supposed to have type T, but instead…

This is a similar sort of error as The expression e must have both a blah type and also…, but concerns patterns instead of expressions. On the one hand, disco can figure out what type a pattern should be based on the type of the function. On the other hand, the pattern itself may correspond to a different type. For example,

Disco> :{
Disco| f : N -> N
Disco| f(x,y) = x + y
Disco| :}
Error: the pattern
  (x, y)
is supposed to have type
  ℕ,
but instead it has a product type.

In this example, we have declared the type of f to be N -> N, that is, a function which takes a natural number as input and yields another natural number as output. However, we have used the pattern (x,y) for the input of f, which looks like a value of a product type.