Got it. Thanks. :) The gotcha for me is that I was thinking as "a generic type 'a' that I may " and not in terms "if something is typed a generic 'a', then it must fit in ANY type". I think this is a common mistake, as I did read about it more than once.
I.e., undefined :: a means a value that can fit in any type. (Num a => a) means a value that can fit int any type that has an instance for Num. My O.O. mind reacted to that as: Num a => a is a numeric type, it may or may not be a Int. Like type hierarchy in Java. A variable declared as "Object" does not mean that it fits in any type. It just means that you have no information about it's real type. Thiago. 2012/1/4 Antoine Latter <aslat...@gmail.com>: > On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri <evoh...@gmail.com> wrote: >> Do not compile: >> >> f :: a -> a >> f x = x :: a >> >> Couldn't match type `a' with `a1' >> `a' is a rigid type variable bound by >> the type signature for f :: a -> a at C:\teste.hs:4:1 >> `a1' is a rigid type variable bound by >> an expression type signature: a1 at C:\teste.hs:4:7 >> In the expression: x :: a >> In an equation for `f': f x = x :: a >> >> >> Any of these compiles: >> >> f :: a -> a >> f x = undefined :: a > > Re-written: > > f :: forall a . a -> a > f x = undefined :: forall a . a > > Renaming variables to avoid shadowing: > > f :: forall a . a -> a > f x = undefined :: forall b . b > > Which is allowed. > > The rest of your examples are similar - a new value is introduced with > a new type that can unify with the required type. > > This is different from the failing case: > > g :: a -> a > g x = x :: a > > Let's go through the same process. > > Insert foralls: > > g :: forall a . a -> a > g x = x :: forall a . a > > Rename shadowed variables: > > g :: forall a . a -> a > g x = x :: forall b . b > > In the function body we have declared that the value 'x' may take on > any value. But that's not true! The value 'x' comes from the input to > the function, which is a fixed 'a' decided by the caller. > > So it does not type-check. > > Antoine > >> >> f :: Num a => a -> a >> f x = undefined :: a >> >> f :: Int -> Int >> f x = undefined :: a >> >> f :: Int -> Int >> f x = 3 :: (Num a => a) >> >> >> Can someone explain case by case? >> >> Thanks, >> Thiago. >> >> 2012/1/4 Yves Parès <limestr...@gmail.com>: >>>> I don't see the point in universally quantifying over types which are >>> already present in the environment >>> >>> I think it reduces the indeterminacy you come across when you read your >>> program ("where does this type variable come from, btw?") >>> >>> >>>> So is there anyway to "force" the scoping of variables, so that >>>> f :: a -> a >>>> f x = x :: a >>>> becomes valid? >>> >>> You mean either than compiling with ScopedTypeVariables and adding the >>> explicit forall a. on f? I don't think. >>> >>> 2012/1/4 Brandon Allbery <allber...@gmail.com> >>> >>> On Wed, Jan 4, 2012 at 08:41, Yves Parès <limestr...@gmail.com> wrote: >>>> >>>> Would you try: >>>> >>>> f :: a -> a >>>> >>>> f x = undefined :: a >>>> >>>> And tell me if it works? IMO it doesn't. >>> >>>> It won't >>> >>> Apparently, Yucheng says it does. >>> >>> _______________________________________________ >>> Haskell-Cafe mailing list >>> Haskell-Cafe@haskell.org >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe