haskellghctype-variablestype-kindstype-constructor

What GHC/Haskell specification says that free type constructors match rightmost types?


I was caught off guard recently when I tried to pass a constructor for a type of kind * -> * -> *, with one bound type var, to a function expecting a constructor for * -> *. Concretely, it was along the lines of passing (\x -> (x, 42)) :: (forall a. a -> (a, Int)) to a function of type forall c. (forall a. a -> c a) -> .... This is ambiguous but not an error in GHC: (,) cast to * -> * could be interpreted as a constructor for either the left or righthand argument, and GHC appears to just default to the righthand argument. For higher-kinded matches, it'll take the rightmost arguments. To see this, just test the inferred type:

foo :: c a b -> a -> b -> ()
foo _ _ _ = ()

bar = foo ((), 42, 'a') 42 'a' -- typechecks

I wrongly believed instead that it would match the free variables in order, but this higher-rank case is the only time where that would obviously be preferred, and other times it's a wash. Is there official documentation describing this rule? I'm slightly annoyed but also understanding of the fact that this is not an error, because I can foresee that saves wrapping a lot of things in newtypes.


Solution

  • Unless I misunderstand the question, this simply follows from type application being left-associative, just like function application.

    (a, b) is (,) a b is ((,) a) b. So (Int, a) is ((,) Int) a, but (a, Int) isn't <something> a.