Equivalence in class laws

[Wolfgang Jeltsch]

Hello,
instances of classes are required to fulfill certain laws. These laws
are usually given in the form t = t' where t and t' are terms. My
question is what the exact meaning of the = is.
Does it mean that evaluation of the terms must lead to equal results
regarding (==)? But if this is the case, what about terms of types which
aren't instances of Eq? Furthermore, wouldn't equivalence be undefined
if at least one of the two terms is _|_.
Or does the = mean that the results of both terms must have exactly the
same structure. But if this is true, what would it mean that two
functions have the same structure?
Does the = even include that all free variables occuring in t and/or t'
must be evaluated the same way?
In the following example, for instance, f x and g x wouldn't be
equivalent according to the last definition although they would yield
the same result for every x:
    f :: () -> ()
    f _ = undefined

    g :: () -> ()
    g () = undefined
When evaluating f x, nothing of x would be evaluated which wouldn't be
the case when evaluating g x. So x is not evaluated the same way in f x
and g x but both terms always yield the same result (always _|_).
Consider replacing each of the two occurences of undefined above by ().
The difference in the evaluation of x would now result in different
results of f x and g x if x = undefined. f x would be () and g x would
be _|_. Where difference in free variable evaluation causes difference
in term results there requirement of result equivalence of course
includes requirement of "free variable evaluation equivalence". In these
cases the second and the third definition approach from the beginning of
this mail would be equivalent.
Now let's consider the Monad/MonadPlus law
    m >>= \x -> mzero = mzero
and the monadic instances of []. Here we have the case that evaluation
behaviour of m is not the same for both terms. (The second term doesn't
even contain m and therefore does no evaluation of m at all which is of
course not true for the first term.) And here the different evaluation
behaviour of m results in both terms not having the same result for
every m. For example
    undefined >>= \x -> mzero
is not mzero but _|_. You may also take a term like
    [1 ..] >>= \x -> mzero
which maybe looks harmless but also has _|_ as result. Does this mean
that [] doesn't satisfy the Monad/MonadPlus laws?
I'm interested in your answers regarding all these questions.

Wolfgang