type checking fails with a correct type
Daniel Fischer
daniel.is.fischer at web.de
Thu Apr 30 11:17:42 EDT 2009
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.
More information about the Glasgow-haskell-users
mailing list