What is the formal name for GHC automatically adapting less-constrained functions to more-constrained rank-2 arguments? [closed]

Yes, GHC creates a wrapper. You can catch it in the act if you add a {-# NOINLINE applyToMany #-} pragma and compile with:

ghc -O0 -ddump-simpl -fforce-recomp -dsuppress-all -dsuppress-uniques Adapting.hs 

The function applyToMany is compiled to:

applyToMany = \ f -> (f $fShowInt $fEqInt $fOrdInt (I# 42#), f $fShowBool $fEqBool $fOrdBool True) 

so it expects to receive a function that can be called with three dictionary arguments, for each of Show, Eq, and Ord. On the other hand, justEq only takes one dictionary argument (for Eq):

justEq = \ @a $dEq x -> case == $dEq x x of { __DEFAULT -> x } 

So, when result is compiled to core, GHC inserts an adapter:

result = applyToMany (\ @a _ $dEq _ eta -> justEq $dEq eta) 

By the way, if you try this out for yourself, you might be interested in recompiling with the Eq a constraint removed from applyToMany's signature, since Eq is a superclass of Ord. The resulting code is different in interesting ways.

This is a form of "subtyping" or "subsumption". The paper Practical type inference for arbitrary-rank types on Haskell's higher-rank type system talks about subsumption generally, but without talking about type classes specifically.

Basically, we say S is a subtype of T or that T subsumes S (both written S <: T) if every value of S can be "treated" as a value T. In OO languages, for example, classes are subtypes of their superclasses, since a Dog value can always be "treated" as an Animal value.

To use the examples in the paper, in Haskell98, forall a b. a -> b -> b is a subtype of Int -> Int -> Int. That may look backwards, but it's because any function of the polymorphic type can be treated as a function of the monomorphic type by instantiating it with a=Int and b=Int. That's why given:

k :: forall a b. a -> b -> b f1 :: (Int -> Int -> Int) -> Int 

the expression f1 k is well typed. k's type is a subtype of the type of f1s first argument, so it can be treated as a value of the expected type, so the expression is well typed.

Similarly, with RankNTypes, given:

f2 :: (forall x. x -> x -> x) -> Int 

the expression f2 k is also well typed. k's type is a subtype of forall x. x -> x -> x, so it is an acceptable first argument to f2.

In your original example, Eq a => a -> a is a subtype of (Show a, Eq a, Ord a) => a -> a. (Again, not backwards -- for polymorphism, more polymorphic types are less "constrained" and so more likely to be subtypes; for constraints, types with fewer constraints are less "constrained" and so more likely to be subtypes.) Because of this, it is okay to pass a value of the former type like justEq to a function expecting a value of the latter type, like applyToMany.

The way in which the OO language "translates" a Dog so it can be passed to a function expecting an Animal, or the way GHC figures out what's needed to pass k to f1 or f2, or to pass justEq to applyToMany --- well, those are all implementation details, and you probably won't find too much impressive theory or formal nomenclature about those details.