inferred type of function in Haskell

The type func :: (Ord a, Num a) => a -> a means that returned type should match with one you passed in. But since you are returning a constant and it doesn't depend on input, its type can be any type of class Num. Thus, compiler infers func :: (Ord a, Num a, Num t) => a -> t.

The inferred type is correct. Let's see how it gets inferred. We will only look at the returned value first:

func x | … = 4 | … = error "…" 

The latter term, error "…" :: a, is unconstrained. However, 4 has the type Num a => a, therefore your function will have type

func :: (Num result) => ????? -> result 

Now let's have a look at x:

func x | x > 0 = … | … 

Due to the use of (>) :: Ord a => a -> a- > Bool and 0 :: Num a, x's has to be an instance of both Num and Ord. So from that point of perspective, we have

func :: (Num a, Ord a) => a -> ???? 

The important part is that 4 and x don't interact. Therefore func has

func :: (Num a, Ord a, Num result) => a -> result 

Of course, result and a could be the same type. By the way, as soon as you connect x and 4, the type will get more specific:

func x | x > 0 = 4 + x - x | … 

will have type (Num a, Ord a) => a -> a.

As you may or may not be aware, Haskell’s numeric literals are polymorphic. That means that a number literal, like 0 or 4, has the type Num a => a. You seem to already understand this, since the type signature you expect includes a Num constraint.

And indeed, the type signature you have provided is a valid one. If you included it, it would be accepted by the compiler, and if it’s the type you actually want, by all means include it. However, the reason it is different from the inferred type is that Haskell will attempt to infer the most general type possible, and the inferred type is more general than the one you’ve written.

The question is, why is the inferred type permitted? Well, consider this similar but distinct function:

func' x | x > 0 = "ok" | otherwise = error "Non positive number" 

This function’s type is (Ord a, Num a) => a -> String. Notably, the input of the function has absolutely no bearing on the output, aside from whether or not the result is ⊥. For this reason, the result can be absolutely anything, including a string.

However, consider yet another function, again similar but distinct:

func'' x | x > 0 = x - 1 | otherwise = error "Non positive number" 

This function must have the type you described, since it uses x to produce a new value.

However, look again at the original func definition. Note how the literal on the right hand side, the 4, does not have anything to do with x. That definition is actually quite a bit closer to func' than func'', so the numeric literal has the type Num t => t, and it never needs to be specialized. Therefore, the inferred type allows the two numeric types to be separate, and you have the more general type written in your question.