Why doesn't subtyping via existentials and constraints work?

Question

I've been trying to see how Haskell copes with subtyping so I came up with the following snippet:

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 _ = 5

f2 :: () -> (forall a. Integral a => a)
f2 = f1

The line f2 = f1 fails with an unexpected error message:

Couldn't match type ‘a’ with ‘Int’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      f2 :: forall a. Integral a => () -> a

It seems that the existential has been promoted to a universal, which of course is unintended.

My guess is that in implementation terms f2 needs to return a value and a corresponding dictionary, while f1 simply returns a value of type Int. However, from a logical perspective the contract of f2 is "a function from () to some unknown instance of Integral" and f1 satisfies it perfectly.

Should GHC do some implicit magic to make it work or am I missing something?

Answer 1

The a type you have in your f2 is universally quantified, not existentially quantified. GHC doesn't directly support kind of existential types that you're looking for.

You can, however, get something like this by wrapping it up in a new data type:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds           #-}

data Constrained c = forall a. c a => Constrained a

f1 :: () -> Int
f1 _ = 5

f2 :: () -> Constrained Integral
f2 unit = Constrained (f1 unit)

Now, this often isn't terribly useful because all that has been accomplished is that we've thrown out all (type) information about f2 () except that its type is an instance of Integral. You no longer know it's an Int. It's possible to keep track of this information as well, but that may or may not be useful depending on what you're doing.

More context for what you're doing and what you're looking to see would make it easier what sort of information about those kinds of things I should add.

As a side note: it isn't necessary to make those into functions that take an argument. You could just have f1 :: Int and f2 :: Constrained Integral.

Also, I would feel a bit remiss if I didn't mention that, despite downplaying the utility of these sorts of types in Haskell a bit earlier in this answer, I wrote an answer that describes some potentially practical uses for constrained existential types. While we're somewhat on the subject, it's probably also worth pointing out that ConstraintKinds is a powerful extension, whose use goes beyond just constrained existentials.

Answer 2

You're reading the type of f2 the wrong way around.

The type of f2 says "if you give me a (), I will give you a (forall a. Integral a => a). That is, f2 promises to give you a value that can be used as if it were in any type that is a member of Integral.

However the implementation of f2 says it will achieve this by simply calling f1. But f1 only returns Int! That is indeed a member of Integral, but it's not usable as any type that is a member of Integral.

In fact, the type f1 is actually a subtype of f2's type, rather than the other way around! This actually works:

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 = f2

f2 :: () -> (forall a. Integral a => a)
f2 _ = 5

It works because numeric literals are polymorphic, so a 5 can be any Num type (and Num is a super class of Integral, so if it can be any Num it can also be any Integral). f1 then calls f2 requesting that Int be the choice for a.

You noticed that GHC seems to be converting the type you wrote to f2 :: forall a. Integral a => () -> a, and you're right; it does actually normalise what you wrote to that type. The reason is those two types actually are the same thing with the way GHC's type system works. The caller instantiates any type variables quantified over the whole type of f2, and the caller would also be the one who receives the return value and so instantiates any type variables quantified over just the return value. Introducing a type variable with forall is the same if you scope if over the whole type or just over the return type of the function; it only makes a difference if it's scoped over the left side of the arrow (which is where higher-rank types come in).