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