The case of the disappearing constraint: Oddities of a higher-rank type
haskell, higher-rank-types, type-constraints, types
Solution
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.
Problem
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?