What does putting a constraint in an argument's type instead of function's type do?

user_1770031 0
Viewed 231

I put a constraint in the type of a function's argument instead of putting in the function's type.
I thought this would either give a syntax error or add more information to the type of the function.
But it looks like the constraint is completely ignored.

{-# 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"

This gives the following type 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"
  |

What does putting a constraint in the the argument's type actually do?

EDIT:

Why does this need RankNTypes extension?
It is not needed if I remove (Num a, Ord a) => constraint.

haskell
1 Answers

This is a rather exotic instance of polymorphic subsumption, as described here, interacting with constraint subsumption.

If a type a subsumes b, then exp :: a implies exp :: b in the surface language. A particular example of subsumption is that f :: forall a. a -> a implies f :: Int -> Int. Also, we have n :: Int implies n :: c => Int for any c constraint.

However, in the core language there is no subsumption at all. Every case of subsumption in the surface language must be translated to explicit lambdas and applications. Also, c => a simply becomes c -> a, and usage of constrained functions is translated to simple function application of f :: c => a to some inst :: c. Hence, f :: forall a. a -> a becomes f @Int :: Int -> Int, and n :: Int becomes \_ -> n :: c -> Int.

A rarely used case is the contravariant subsumption rule for functions. The following is valid code:

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

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

This is translated to 

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

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

It works similarly with constraint subsumption:

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

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

Which is translated to

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

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

Getting closer to the original question, if we have

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

as a top definition, its inferred type is forall a. (Eq a => a) -> Bool. However, we can have any type annotation for f which is subsumed by the inferred type! So we may have:

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

And GHC is still happy. The original code

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

is equivalent to the slightly clearer following version:

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

The type error which you get is simply because n is really a function with two arguments, one has type Num a and the other Ord a, and both of these arguments are records containing Num and Ord methods. However, since there are no such instances in scope in the definition, you cannot use n as a number. The translation would convert n > 10 to (>) inst (n inst) (10 inst), where inst :: Num a, but there is no such inst, so we cannot translate.

Hence, in the body of test the code is still checked with n :: (Num a, Ord a) => a). However, if we just return "Hello" without using n, then similarly to the previous f case, we get an inferred type which subsumes the forall a. a -> String annotation type. The subsumption is then realized in the translation output by replacing every occurrence of n in the body of test with \_ -> n. But since n does not occur in the body, the translation does not do anything here.

user_10682320
Related