Implement better type-checking

[jstolarek]

At the moment type checking is merged into one pass with desugaring and is a bit ad-hoc. It might be worth to implement a separate type-checking pass that would run before desugaring. The primary motivation for this is presence of exceptions, which can inhabit every type. At the moment this is implemented as a very inelegant special case: internally there is a separate type of exceptions ExnTy and the fact that it inhabits every type is achieved by overriding == and some helper functions, eg.:

instance Eq Type where
    ExnTy        == _              = True
    _            == ExnTy          = True
    -- standard equations follow (...)

-- | Is function type?
isFunTy :: Type -> Bool
isFunTy (FunTy _ _) = True
isFunTy ExnTy       = True
isFunTy _           = False

This does not scale in any way. A proper solution would be to have a type inference with unification. Then raise "foo" would have polymorphic type a and unification would find instantiation of type variables.

Another advantage of having type inference would be allowing exceptions to be raised inside a case scrutinee. At the moment this is not allowed because of the way we desugar let expressions, ie. assuming that we know the exact type of scrutinee and desugar branches based on that.