¿Qué significa poner una restricción en el tipo de un argumento en lugar del tipo de función?

Pongo una restricción en el tipo de argumento de una función en lugar de poner el tipo de la función.
Pensé que esto daría un error de sintaxis o agregaría más información al tipo de función.
Pero parece que la restricción se ignora por completo.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

test :: a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

main = print "Hello World"

Esto da el siguiente tipo de error:

Test3.hs:6:8: error:
    • No instance for (Num a) arising from a use of ‘n’
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            test :: forall a. a -> String
    • In the first argument of ‘(>)’, namely ‘n’
      In the expression: n > 10
      In the expression: if n > 10 then "Hello" else "World"
  |
6 |     if n > 10 then "Hello"
  |        ^

Test3.hs:6:8: error:
    • No instance for (Ord a) arising from a use of ‘>’
      Possible fix:
        add (Ord a) to the context of
          the type signature for:
            test :: forall a. a -> String
    • In the expression: n > 10
      In the expression: if n > 10 then "Hello" else "World"
      In an equation for ‘test’:
          test (n :: (Num a, Ord a) => a)
            = if n > 10 then "Hello" else "World"
  |
6 |     if n > 10 then "Hello"
  |  

¿Qué significa realmente poner una restricción en el tipo de argumento?

EDITAR:

¿Por qué esto necesita RankNTypesextensión?
No es necesario si elimino la (Num a, Ord a) =>restricción.

Esta es una instancia bastante exótica de subsunción polimórfica, como se describe aquí , que interactúa con la subsunción de restricción.

Si un tipo asubsume b, entonces exp :: aimplica exp :: ben el lenguaje superficial. Un ejemplo particular de subsunción es que f :: forall a. a -> aimplica f :: Int -> Int. Además, tenemos n :: Intimplica n :: c => Intpara cualquier crestricción.

Sin embargo, en el lenguaje central no hay subsunción en absoluto. Cada caso de subsunción en el lenguaje de superficie debe traducirse a lambdas y aplicaciones explícitas. Además, c => asimplemente se convierte c -> a, y el uso de funciones restringidas se traduce en la aplicación de funciones simples f :: c => apara algunos inst :: c. Por lo tanto, se f :: forall a. a -> avuelve f @Int :: Int -> Inty se n :: Intvuelve \_ -> n :: c -> Int.

Un caso raramente utilizado es la regla de subsunción contravariante para funciones. El siguiente es un código válido:

f :: (Int -> Int) -> Bool
f _ = True

g :: (forall a. a -> a) -> Bool
g = f

Esto se traduce a

f :: (Int -> Int) -> Bool
f = \_ -> True

g :: (forall a. a -> a) -> Bool
g = \x -> f (x @Int)

Funciona de manera similar con la subsunción de restricción:

f :: forall a. (Eq a => a) -> Bool
f _ = True

g :: forall a . a -> Bool
g = f

Que se traduce a

f :: forall a. (Eq a -> a) -> Bool
f = \_ -> True

g :: forall a . a -> Bool
g = \x -> f (\_ -> x)

Acercándonos a la pregunta original, si tenemos

f (x :: Eq a => a) = True

como definición superior, su tipo inferido es forall a. (Eq a => a) -> Bool. Sin embargo, podemos tener cualquier tipo de anotación para la fcual se incluye el tipo inferido. Entonces podemos tener:

f :: forall a. a -> Bool
f (x :: Eq a => a) = True

Y GHC sigue feliz. El código original

test :: a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

es equivalente a la siguiente versión ligeramente más clara:

test :: forall a. a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

El error de tipo, que se obtiene es simplemente porque nes realmente una función con dos argumentos, uno tiene el tipo Num ay el otro Ord a, y ambos de estos argumentos son los registros que contienen Numy Ordmétodos. Sin embargo, dado que no hay tales instancias en el alcance de la definición, no puede usarlas ncomo un número. La traducción se convertiría n > 10a (>) inst (n inst) (10 inst), donde inst :: Num a, pero no existe inst, por lo que no podemos traducir.

Por lo tanto, en el cuerpo del testcódigo todavía se verifica con n :: (Num a, Ord a) => a). Sin embargo, si solo devolvemos "Hola" sin usar n, de manera similar al fcaso anterior , obtenemos un tipo inferido que subsume el forall a. a -> Stringtipo de anotación. La subsunción se realiza luego en la salida de traducción reemplazando cada aparición de nen el cuerpo de testcon \_ -> n. Pero como nno ocurre en el cuerpo, la traducción no hace nada aquí.