[Haskell-cafe] Solved but strange error in type inference

[AUGER Cédric]

Le Tue, 3 Jan 2012 20:46:15 +0100,
Yves Parès <limestrael at gmail.com> a écrit :

> > Actually, my question is why the different type can't be unified
> > with the
> inferred type?
> 
> Because without ScopedTypeVariable, both types got expanded to :
> 
> legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String
> ([t], s)
> 
> subsome :: *forall nt* t s. [RRule nt t s] ->  Either String ([t], s)
> 
> So you see subsome declare new variables, which *do not *match the
> *rigid *ones declared by legSome signature, hence the incompatibility.
> 

How ugly! I thought that Haskell didn't allow to mask type variables.

Does that mean that I can do:

foo :: (a -> a) -> (b -> b) -> a -> a
foo bar dummy =
  let strange :: a -> a
      strange = dummy
  in
  foo

(ok, that's dead code, but how misleading it would be!)

Is there some way to enforce a typing error here?
(I am pretty sure there is some flag to have explicit 'forall's,
but I am not sure that it forces you to use 'forall' explicitely.)

I come from Coq community (where forall must be explicit) and Ocaml
community (where most people strongly rely on type inference and do not
put types very often). I didn't try this example on Ocaml.

> As we said before, you have three ways to work it out:
> 1) Use scoped type variables with explicit forall nt on legSome and
> *no forall *on subsome, so that nt in subsome matches nt declared in
> legSome. 2) Don't give a type signature for subsome and let GHC find
> out which is its correct type.
> 3) Extract subsome so that it becomes a top-level function with a
> polymorphic type (Recommended).

In fact I first wanted to write directly the method without using
auxiliary functions (I changed my mind since, as I redisigned my code
and it wasn't possible [or at least natural for me] to put the code
directly inlined).

In fact I often do nested functions when there are free variables in
the function. I particulary hate to have code like that:

foo :: bar -> foobar -> barfoo
foo b fb = if f b fb
           then foo b (g b fb)
           else h b fb

as b is in fact invariant in the calls of 'foo'; so I always rewrite
this as:

foo :: bar -> foobar -> barfoo
foo b = let fooAux :: foobar -> barfoo
            fooAux fb = if f b fb
                        then fooAux (g b fb)
                        else h b fb
        in fooAux

that is more verbose, but I well see what are the recursive parameters,
and I have the (probably wrong) feeling that it is better since
function calls have less arguments.

Here subsome was depending on the free variable "sg", so I had to
generalize it to do so even if I won't have benefits in having the
ability to use it elsewhere (as it was the only place I wanted to use
it).

I always prefer to minimize the number of specialized functions, since
I hate jumping from parts of code to other parts of code to understand
what a function really does.

> 
> 
> Now, concerning the error I asked you to deliberately provoke, that's
> the quickest way I found to know what is the output of the type
> inferer, and maybe the only simple one.
> So this error is:
> > Couldn't match expected type `Int'
> >               with actual type `[([Symbols nt t], [s] -> t0)]
> >                                 -> Either [Char] ([t], t0)'
> >   In the expression: subsome :: Int
> GHC tells you the type it infers for subsome: [([Symbols nt t], [s]
> -> t0)] -> Either [Char] ([t], t0)
> The nt you see is the one from legSome, those messages show scoped
> variables. (You'd get something like 'nt1' or 'nt0' if it was another
> variable, meant to be instanciated to a different type).
> This accords with your previous error message, which happens to give
> you more details about where the rigid type variable nt comes from:
> >      `nt' is a rigid type variable bound by
> >           the type signature for
> >             legSome :: LegGram nt t s -> nt -> Either String ([t],
> > s)
> 
> HTH.
> 
> 2012/1/3 Yucheng Zhang <yczhang89 at gmail.com>
> 
> > On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson
> > <spam at scientician.net> wrote:
> > > 'subsome' to a different type than the one you intended -- and
> > > indeed one which can't be unified with the inferred type. (Unless
> > > you use ScopedTypeVariables.)
> >
> > Thanks for the reply.
> >
> > Actually, my question is why the different type can't be unified
> > with the inferred type? Could you point me some related resources?
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >