The case of the disappearing constraint: Oddities of a higher-rank type

Question

All the experiments described below were done with GHC 8.0.1.

This question is a follow-up to RankNTypes with type aliases confusion. The issue there boiled down to the types of functions like this one...

{-# LANGUAGE RankNTypes #-}

sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y

... which are rejected by the type checker...

ThinAir.hs:4:13: error:
    * No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            sleight1 :: a -> (Num a => [a]) -> a
    * In the pattern: y : _
      In an equation for `sleight1': sleight1 x (y : _) = x + y

... because the higher-rank constraint Num a cannot be moved outside of the type of the second argument (as would be possible if we had a -> a -> (Num a => [a]) instead). That being so, we end up trying to add a higher-rank constraint to a variable already quantified over the whole thing, that is:

sleight1 :: forall a. a -> (Num a => [a]) -> a

With this recapitulation done, we might try to simplify the example a bit. Let's replace (+) with something that doesn't require Num, and uncouple the type of the problematic argument from that of the result:

sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y

This doesn't work just like before (save for a slight change in the error message):

ThinAir.hs:7:24: error:
    * No instance for (Num b) arising from a use of `y'
      Possible fix:
        add (Num b) to the context of
          the type signature for:
            sleight2 :: a -> (Num b => b) -> a
    * In the second argument of `const', namely `y'
      In the expression: const x y
      In an equation for `sleight2': sleight2 x y = const x y
Failed, modules loaded: none.

Using const here, however, is perhaps unnecessary, so we might try writing the implementation ourselves:

sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x

Surprisingly, this actually works!

Prelude> :r
[1 of 1] Compiling Main             ( ThinAir.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t sleight3
sleight3 :: a -> (Num b => b) -> a
*Main> sleight3 1 2
1

Even more bizarrely, there seems to be no actual Num constraint on the second argument:

*Main> sleight3 1 "wat"
1

I'm not quite sure about how to make that intelligible. Perhaps we might say that, just like we can juggle undefined as long as we never evaluate it, an unsatisfiable constraint can stick around in a type just fine as long as it is not used for unification anywhere in the right-hand side. That, however, feels like a pretty weak analogy, specially given that non-strictness as we usually understand it is a notion involving values, and not types. Furthermore, that leaves us no closer from grasping how in the world String unifies with Num b => b -- assuming that such a thing actually happens, something which I'm not at all sure of. What, then, is an accurate description of what is going on when a constraint seemingly vanishes in this manner?

Stanger

I find that somewhat natural, since e.g. x in the type f :: A -> (x -> B) -> C in in a positive (or covariant) position. Roughly, f is promising to provide x instead of requiring it from outside. This is extended to y :: C a => a. Also, every type you use that y, GHC has to provide a dictionary so to obtain a value of type a -- so it will complain if there's no such dictionary around. – Ethnogeny

That seems very strange, I agree. Probably, only GHC-makers know what kind of magic happens behind forall :) – Monogenetic

@Ethnogeny Putting the issue in terms of positive and negative positions is quite clarifying indeed. It is interesting how things only makes sense here if you sublate the intuitive view of constraints as some sort of restricted quantification (e.g. "Num a => a stands for some type a in Num") and begin seeing them as, in essence, functions from dictionaries. – Stanger

Answer 1

Oh, it gets even weirder:

Prelude> sleight3 1 ("wat"+"man")
1
Prelude Data.Void> sleight3 1 (37 :: Void)
1

See, there is an actual Num constraint on that argument. Only, because (as chi already commented) the b is in a covariant position, this is not a constraint you have to provide when calling sleight3. Rather, you can just pick any type b, then whatever it is, sleight3 will provide a Num instance for it!

Well, clearly that's bogus. sleight3 can't provide such a num instance for strings, and most definitely not for Void. But it also doesn't actually need to because, quite like you said, the argument for which that constraint would apply is never evaluated. Recall that a constrained-polymorphic value is essentially just a function of a dictionary argument. sleight3 simply promises to provide such a dictionary before it actually gets to use y, but then it doesn't use y in any way, so it's fine.

It's basically the same as with a function like this:

defiant :: (Void -> Int) -> String
defiant f = "Haha"

Again, the argument function clearly can not possibly yield an Int because there doesn't exist a Void value to evaluate it with. But this isn't needed either, because f is simply ignored!

By contrast, sleight2 x y = const x y does kinda sorta use y: the second argument to const is just a rank-0 type, so the compiler needs to resolve any needed dictionaries at that point. Even if const ultimately also throws y away, it still “forces” enough of this value to make it evident that it's not well-typed.

Woundwort

How amusing. I wonder whether the following interpretation is sensible: If constraints are essentially functions from dictionaries, Num in Num b is essentially a type function that produces a type with one inhabitant (if there is an instance, and you aren't fooling around with IncoherentInstances and the like) or zero inhabitants (if there is no instance), and so Num String => String is much like Void -> String, except that in the former case the compiler can't even cheat by passing undefined in lieu of the argument. – Stanger