On Wed, Aug 24, 2016 at 11:49 AM, Morten Olsen Lysgaard
Lastly consider:
foo3 :: a -> Int foo3 x = x
The inferred type of `foo3` is, again, `foo3 :: t -> t`, when unified with the annotated type, `a -> Int`, we find that `t` must have the same type as `a`, and `t` must be of type `Int`, thus `t = a = Int`. Everything works out!?
I mentioned this when you were asking about this in IRC, but you may have missed it. All type variables are implicitly qualified at top level in standard Haskell (and in ghc if they are not explicitly qualified at some level). Thus the actual type signature is foo3 :: forall a. a -> Int and (forall a. a) does *not* unify with Int. This does not work in both directions, though; in your second example, the *inferred* type (t -> t) is permitted to unify with an explicitly specified type (Int -> Int). It is only explicitly specified types that do this (this is what "rigid" means: explicitly specified, therefore not permitted to unify with a more specific type). The reason for this is that the type signature specifies the contract with callers. (a -> a) which means (forall a. a -> a) promises the caller you will accept any (a) the *caller* chooses. This is why such explicit signatures are rigid: you promised the caller you will accept any (a), so you may not renege on that contract and always produce (Int). -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net