RankNTypes with type aliases confusion [duplicate]

Question

I'm trying to understand how type constraints work with type aliases. First, let's assume I have next type alias:

type NumList a = Num a => [a]

And I have next function:

addFirst :: a -> NumList a -> NumList
addFirst x (y:_) = x + y

This function fails with next error:

Type.hs:9:13: error:
    • No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            addFirst :: a -> NumList a -> a
    • In the pattern: y : _
      In an equation for ‘addFirst’: ad

Which is obvious. This problem already described here:

Understanding a rank 2 type alias with a class constraint

And I understand why we need {-# LANGUAGE RankNTypes #-} for such type aliases to work and why previous example doesn't work. But what I don't understand is why next example compiles fine (on ghc 8):

prepend :: a -> NumList a -> NumList a
prepend = (:)

Of course it fails in ghci if I try to pass wrong value:

λ: prepend 1 []
[1]
λ: prepend "xx" []

<interactive>:3:1: error:
    • No instance for (Num [Char]) arising from a use of ‘prepend’
    • When instantiating ‘it’, initially inferred to have
      this overly-general type:
        NumList [Char]
      NB: This instantiation can be caused by the monomorphism restriction.

Seems like type type checking delayed at runtime :(

Moreover, some simple and seems to be the same piece of code doesn't compile:

first :: NumList a -> a
first = head

And produces next error:

Type.hs:12:9: error:
    • No instance for (Num a)
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            first :: NumList a -> a
    • In the expression: head
      In an equation for ‘first’: first = head

Can somebody explain what is going on here? I expect some consistency in whether function type checks or not.

Answer 1

Seems like type type checking delayed at runtime :(

Not really. Here it's may be a bit surprising because you get the type error in ghci after having loaded the file. However it can be explained: the file itself is perfectly fine but that does not mean that all the expressions you can build up using the functions defined in it will be well-typed.

Higher-rank polymorphism has nothing to do with it. (+) for instance is defined in the prelude but if you try to evaluate 2 + "argh" in ghci, you'll get a type-error too:

No instance for (Num [Char]) arising from a use of ‘+’
In the expression: 2 + "argh"
In an equation for ‘it’: it = 2 + "argh"

Now, let's see what the problem is with first: it claims that given a NumList a, it can produce an a, no questions asked. But we know how to build NumList a out of thin air! Indeed the Num a constraints means that 0 is an a and makes [0] a perfectly valid NumList a. Which means that if first were accepted then all the types would be inhabited:

first :: NumList a -> a
first = head

elt :: a
elt = first [0]

In particular Void would be too:

argh :: Void
argh = elt

Argh indeed!