I am ascribing the type of a variable with type Num a => a -> a to Int, which throws an error, as expected. However, the error isn't exactly as I expected.
GHCi
λ> let x = typeInference 1
λ> :t x
x :: Num a => a -> a
λ> x :: Int
<interactive>:141:1: error:
• Couldn't match expected type 'Int'
with actual type 'Integer -> Integer'
• Probable cause: 'x' is applied to too few arguments
In the expression: x :: Int
In an equation for 'it': it = x :: Int
λ>
typeInferance definition
typeInference :: Num a => a -> a -> a
typeInference x y = x + y + 1
I expected the error message to say with actual type 'Num a => a -> a', which is the polymorphic type, why doesn't it? Does this have to do with GHCi's type defaulting?
This is indeed because of GHCi's type defaulting.
The rules for this are described in section 4.3.4 of the Haskell 2010 Report and this part is especially relevant:
Each defaultable variable is replaced by the first type in the default list that is an instance of all the ambiguous variable’s classes. It is a static error if no such type is found.
Every variable that is defaultable is replaced by what it defaults to, which is the operation that occurs before the error message is produced.
Type defaulting must occur before type checking, when there is an ambiguous type. In particular, if the type class constraint were kept around instead of defaulted, the expression x :: Int would have an ambiguous type in it as defined in
We say that an expression e has an ambiguous type if, in its type ∀ u'. cx ⇒ t, there is a type variable u in u' that occurs in cx but not in t. Such types are invalid.
(Taken from the Haskell 2010 Report, replacing u with an overbar with u').
Since, if the type were valid, the overall expression would have a type variable (the one constrained by Num) that does not appear in the resulting type (Int) (and the type variable cannot be unified away), the defaulting must occur here before the type checking.
This can be made a bit more explicit by realizing that we are type checking
(x :: forall a. Num a => a -> a) :: Int
It looks like, during unification, if the outermost type constructor does not match ((->) on the left-hand side and Int on the right-hand side), it must default because it cannot automatically go deeper into the unification (as it could if the outermost type constructor here on the right-hand side were also (->)).
Here are a few more examples I've tested which follow this behavior:
ghci> :set -XExplicitForAll
ghci> (x :: forall a. Num a => a -> a) :: Char -> Char -- Outermost constructor matches, so 'a' can get unified with Char and the 'a' type variable disappears
<interactive>:5:2: error:
• No instance for (Num Char)
arising from an expression type signature
• In the expression:
(x :: forall a. Num a => a -> a) :: Char -> Char
In an equation for ‘it’:
it = (x :: forall a. Num a => a -> a) :: Char -> Char
ghci> (x :: forall a. Num a => a -> a) :: Maybe Char
<interactive>:8:2: error:
• Couldn't match expected type ‘Maybe Char’
with actual type ‘Integer -> Integer’
• In the expression: (x :: forall a. Num a => a -> a) :: Maybe Char
In an equation for ‘it’:
it = (x :: forall a. Num a => a -> a) :: Maybe Char
ghci> (x :: forall a. Num a => a -> a) :: Either Char Bool
<interactive>:10:2: error:
• Couldn't match expected type ‘Either Char Bool’
with actual type ‘Integer -> Integer’
• In the expression:
(x :: forall a. Num a => a -> a) :: Either Char Bool
In an equation for ‘it’:
it = (x :: forall a. Num a => a -> a) :: Either Char Bool
ghci> (x :: forall a. Num a => (,) a a) :: Either Char Bool
<interactive>:11:2: error:
• Couldn't match expected type ‘Either Char Bool’
with actual type ‘(Integer, Integer)’
• In the expression:
(x :: forall a. Num a => (,) a a) :: Either Char Bool
In an equation for ‘it’:
it = (x :: forall a. Num a => (,) a a) :: Either Char Bool
ghci> (x :: forall a. Num a => (,) a a) :: Char
<interactive>:12:2: error:
• Couldn't match expected type ‘Char’
with actual type ‘(Integer, Integer)’
• In the expression: (x :: forall a. Num a => (,) a a) :: Char
In an equation for ‘it’:
it = (x :: forall a. Num a => (,) a a) :: Char