On Apr 30, 2009, at 09:52 , Jan Jakubuv wrote:

*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'

http://www.haskell.org/pipermail/haskell-cafe/2008-April/041397.html http://hackage.haskell.org/trac/ghc/ticket/1897 The type really is ambiguous according to GHC's rules, because you're missing some relationships. As I understand it (which may well be wrong), f you leave off the explicit typing it will successfully infer everything including the missing relationship; but if you explicitly type it you prevent inference of the missing relationship. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

Am Donnerstag 30 April 2009 15:52:12 schrieb 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?

In nonsense t = case nonsense t of Nothing -> Just empty , which type has the Nothing? It can have the type Maybe s1 for all s1 belonging to SUBST, that is the ambiguous type variable.

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

Here, Nothing must have the same type as x. Since x may be returned, x must have type Maybe s, for the type variable s of the signature, so the types are completely determined.

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)

Probably something like the above. To fix the error, you could use asTypeOf: nonsense :: SUBST s => t -> Maybe s nonsense t = res where res = case nonsense t `asTypeOf` res of Nothing -> Just empty or {-# LANGUAGE ScopedTypeVariables #-} nonsense :: forall s. SUBST s => t -> Maybe s nonsense t = case nonsense t :: Maybe s of Nothing -> Just empty

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.

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

Sincerely, Jan.