Am Donnerstag 30 April 2009 18:25:43 schrieb Jan Jakubuv:

Hello Daniel,

On Thu, Apr 30, 2009 at 05:17:42PM +0200, Daniel Fischer wrote:

...

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.

thanks for the explanation. Maybe I'm starting to understand what is going on. Now I understand it thus the call of `nonsense` inside the case construct can potentially result in a different `SUBST`-type `s1` than the top-level `nonsense`. That is why it has to be explicitly typed.

But I am still not following why the type inference works fine without the signature. Isn't it still ambiguous?

Ah, that's a tricky one :) Without the type signature, the type of nonsense has to be inferred from scratch. We start with nonsense t = rhs so nonsense is a function, taking an argument of type argT, giving a result of type resT: nonsense :: argT -> resT Now we infer the type of the rhs, resT. case nonsense t of Nothing -> Just empty or, rewritten, let r = nonsense t in case r of Nothing -> Just empty now r is the result of applying nonsense to t, hence r :: resT. So Nothing has type resT. Since Nothing :: forall a. Maybe a, we can now deduce resT === Maybe b for some b we don't know anything about yet. In case r matches Nothing, the result is (Just empty), so b is the type of empty. empty has type (SUBST s => s), giving resT === SUBST s => Maybe s and nonsense :: SUBST s => argT -> Maybe s *Now* the free type variables are quantified, giving nonsense :: forall argT s. SUBST s => argT -> Maybe s Since in Haskell, type variables are implicitly universally quantified, the "forall argT s." part isn't necessary and not displayed. Here comes the snag: If you give the (implicitly universally quantified) type signature, you explicitly say that nonsense can return a value of type Maybe s, whatever s is, as long as it's a member of SUBST. But then the type-checker cannot assume that r and Just empty have the same type, thus it sees let r = nonsense t , from which it finds r :: forall s1. SUBST s1 => Maybe s1 on the other hand, it finds Just empty :: forall s2. SUBST s2 => Maybe s2, giving nonsense the ambiguous type nonsense :: forall t s1 s2. (SUBST s1, SUBST s2) => t -> Maybe s2 You can ask GHC by compiling the module without the type signature and with the flag -ddump-simpl , the relevant part of the core is: ================================================================== Nonsense.nonsense :: forall t_agD s_agJ. (Nonsense.SUBST s_agJ) => t_agD -> Data.Maybe.Maybe s_agJ [GlobalId] [Arity 2] Nonsense.nonsense = \ (@ t_agD) -- type of argument (@ s_agJ) -- type of result is (Maybe s_agJ) ($dSUBST_agL :: Nonsense.SUBST s_agJ) -- SUBST dictionary for s_agJ (eta_shh :: t_agD) -> letrec { nonsense1_agA :: t_agD -> Data.Maybe.Maybe s_agJ -- inner nonsense, the type is fixed as that at which the outer nonsense is called, -- there is *no* forall here! [Arity 1] nonsense1_agA = \ (t_afx :: t_agD) -> case nonsense1_agA t_afx of wild_Xk { Data.Maybe.Nothing -> Data.Maybe.Just @ s_agJ ($dSUBST_agL `cast` ((Nonsense.:Co:TSUBST) s_agJ :: (Nonsense.:TSUBST) s_agJ ~ s_agJ)); Data.Maybe.Just ipv_shd -> Control.Exception.Base.patError @ (Data.Maybe.Maybe s_agJ) "Nonsense.hs:(16,13)-(17,36)|case" }; } in nonsense1_agA eta_shh ==================================================================

...

{-# LANGUAGE ScopedTypeVariables #-}

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

Great, ScopedTypeVariables is exactly what I was looking for. It solves all my problems.

Great :D

Thank you, Jan.

Cheers, Daniel