type checking fails with a correct type

[Jan Jakubuv]

Hi,

I have the following problem. Below is the smallest program I have found
that shows the problem. That is why the program makes no sense (I have also
meaningful but more complicated program). When I run this program in ghci:

    class SUBST s where 
        empty :: s

    --nonsense :: SUBST s => t -> Maybe s
    nonsense t = case nonsense t of
        Nothing -> Just empty

then everything is fine and I can see the type signature of `nonsense`
inferred by ghci:

    *Main> :t nonsense 
    nonsense :: (SUBST s) => t -> Maybe s

But, when I put this signature into the code (that is, when the commented
line above is uncommented) then type checking fails with the following
error:

    Ambiguous type variable `s' in the constraint:
      `SUBST s'
        arising from a use of `nonsense' at problem-type.hs:6:18-27
    Probable fix: add a type signature that fixes these type variable(s)

Now, what is the problem here? Why does type checking fail with the
signature that the type inference itself inferred?

I am developing kind of generic interface and I don't want to fix the type
`s`. I want `nonsense` to work possibly for any instance of SUBST and the
concrete instance to be determined by the context where `nonsense` is used.

In my original, meaningful but more complicated example I had the following
error:

    Couldn't match expected type `STerm s'
           against inferred type `STerm s1'
    When generalising the type(s) for `refute'

(this message does not provide any information where `s1` comes from)

The original example shares with the above one the property that the type
`s` is not mentioned in types of arguments, just in the type of a result
(although, in the original example, some relation between types `t` and `s`
is expressed in the type context via equality constrains on associated
types (STerm from the error message) ).

I tested this with ghc-6.6.1, ghc-6.10.1, ghc-6.10.2 obtaining the same
result.

BTW, I don't understand why but everything works fine with the following
addition:

    nonsense' :: SUBST s => t -> Maybe s
    nonsense' t = case nonsense' t of
        Nothing -> Just empty
        x       -> x

I'll be grateful for any explanation of this issue.

Sincerely,
  Jan.



-- 
Heriot-Watt University is a Scottish charity
registered under charity number SC000278.