Re: Functional dependencies, principal types, and decidable typechecking

Manuel M T Chakravarty wrote:

I accept that this is the process by which GHC computes these types, but

it does violate the principal types property, doesn't it? The relation

Int -> () <= forall c. Int -> c

does not hold.

I realise that principal types and principal typings are slightly different, but I was wondering if the fact that it has recently been shown that Hindley/Milner does not have principal typings has any meaning here? Keean.