type checking fails with a correct type

[Daniel Fischer]

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