It seems to me that that type annotation and type application play similar role in several context. But there are situation where type application is just not possible and the only way to reproduce its behavior type annotation

λ> :set -XTypeApplications

λ> :t fromInteger(42::Integer)
fromInteger(42::Integer) :: Num a => a
λ> :t 42
42 :: Num p => p

λ> fromInteger @Float (42::Integer)  
42.0
λ> 42 :: Float
42.0

For technical reasons we can't write 42 @Float.

My question would then be

If Type Annotation and Type Application are indeed the same as in result in the same effect, what is actually happening when we write

λ> 42 :: Fractional a => a
42.0  -- type defaulting is understood and not the issue of the question
λ> :t it
it :: Fractional a => a

Does that make sense to say that it is equivalent to

42 @Fractional a => a

I find that strange as type application, if my understanding is correct is for concrete type only. Also it seems to me that in fact we are instead adding more constraint to a rather than applying a full new type.

Hence the question: What is actually happening under the hood here ?

Because indeed when i add the constraint manually the following occur (due indeed to the hierarchy)

λ> 42 :: (Num a, Fractional a) => a
42.0
λ> :t it
it :: Fractional a => a

λ> :t 42 :: (Num a, Fractional a) => a
42 :: (Num a, Fractional a) => a :: Fractional a => a

The point being, that this behavior feels more like what is actually happening when we write 42 :: Fractional a => a rather than thinking of it as 42 @Fractional a => a

EDIT1

Following @leftaroundabout excellent answer i would like to add more context to my question to help narrow down what i am after.

In short, why is it that the following works:

λ> (2 :: (Num p => p)) :: (Fractional p => p)
2.0

But the inverse does not

λ> (2 :: (Fractional p => p)) :: (Num p => p)

<interactive>:5:2: error:
    • Could not deduce (Fractional p1)
        arising from an expression type signature
      from the context: Num p
        bound by the inferred type of it :: Num p => p
        at <interactive>:5:1-42
      or from: Num p1
        bound by an expression type signature:
                   forall p1. Num p1 => p1
        at <interactive>:5:31-42
      Possible fix:
        add (Fractional p1) to the context of
          an expression type signature:
            forall p1. Num p1 => p1
    • In the expression: (2 :: (Fractional p => p)) :: (Num p => p)
      In an equation for ‘it’:
          it = (2 :: (Fractional p => p)) :: (Num p => p)

I suspect that there must be more to

λ> 42 :: Fractional a => a

being equivalent

it :: ∀ a . Fractional a => a
it = 42

The point being that 42 has the polymorphic type derived from fromInteger(42::Integer) = Num a => a and somehow restricting that further to be Fractional a => a is ok. The other way around would not work.

How do that mechanic work, how is it called and what rules does it follow ?

My original understanding was that type application was happening, but clearly based on @@leftaroundabout answer, I understand now that's not what is happening.

Reading around i'm suspecting that it is more related to Type Unification ??

CodePudding user response：

All polymorphic functions/values have implicit extra arguments, specifying what concrete types the type variables in the signature are instantiated to. All a type application does is explicitly pass a type-value into that implicit argument, which otherwise the type checker would try to infer from the context.

What this never does is quantifying over new type variables or applying (non-equational) constraints to them.

It is sensible enough to write 42 @Double. It happens to be not allowed by Haskell, but it could well be, because the polymorphic literal expects an implicit type argument, and Double is a suitable instantiation. (Though of course, why not just write 42 :: Double instead!) In particular, Double has kind Type, and it has a Num instance.

42 @Fractional however doesn't make sense, because Fractional is a type class, i.e. it has kind Type -> Constraint, and a number literal doesn't accept anything like that. When you write 42 :: Fractional a => a, what you're doing instead is to (anonymously) define a new polymorphic value. Your GHCi request is shorthand for making a definition

it :: ∀ a . Fractional a => a
it = 42

You could then afterwards write it @Double or it @Rational (but not it @Int).