[Haskell-cafe] Rigid type variables and their role in type checking

[Brandon Allbery]

On Wed, Aug 24, 2016 at 11:49 AM, Morten Olsen Lysgaard <morten at lysgaard.no>
wrote:

> 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 at gmail.com                                  ballbery at sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160824/1cee9da2/attachment.html>