Type equality constraints and polymorphism

Question

What are the exact semantics of equality constraints? Are these two types exactly equivalent?

f :: Int -> IO [T]
g :: (a ~ T) => Int -> IO [a]

Is g a monomorphic or a polymorphic function that happens to only work for T? It trivially seems monomorphic but will the compiler handle it like f? The GHC user guide section on equality constraints does not discuss implementation details.

I seem to recall polymorphic functions may require INLINEABLE or SPECIALIZE pragmas to enable all optimizations and there can be a runtime cost to making things needlessly polymorphic. Could that be the case for g here as well or will GHC know better and simplify this right away? Or maybe, it depends?

Answer 1

Well, the types certainly aren't exactly equivalent.

The type-checker considers them different types. If you compile with -ddump-types, you'll see:

TYPE SIGNATURES
  f :: Int -> IO [Double]
  g :: forall a. (a ~ Double) => Int -> IO [a]

The two types also behave differently at compile time. For example, with the TypeApplications extension, g @Double 10 is a valid expression while f @Double 10 isn't.

In core, the equality constraint is implemented -- like all constraints -- as an extra dictionary argument, and you'll see this difference in the types reflected in the generated core. In particular, if you compile the following program:

{-# LANGUAGE GADTs #-}

module EqualityConstraints where

import Control.Monad

f :: Int -> IO [Double]
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
g n = replicateM n readLn

with:

ghc -ddump-types -ddump-simpl -dsuppress-all -dsuppress-uniques \
    -fforce-recomp EqualityConstraints.hs

you'll see core like the following:

-- RHS size: {terms: 12, types: 22, coercions: 3, joins: 0/0}
g = \ @ a $d~ eta ->
      case eq_sel $d~ of co { __DEFAULT ->
      replicateM
        $fApplicativeIO eta (readLn ($fReadDouble `cast` <Co:3>))
      }

-- RHS size: {terms: 6, types: 4, coercions: 0, joins: 0/0}
f = \ n -> replicateM $fApplicativeIO n (readLn $fReadDouble)

and this difference will persist in the core even with -O2.

Indeed, if you prevent inlining, the resulting final core (and even the final STG) will involve some unnecessary dictionary passing, as you can see by playing with:

{-# LANGUAGE GADTs #-}

import Control.Monad

f :: Int -> IO [Double]
{-# NOINLINE f #-}
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
{-# NOINLINE g #-}
g n = replicateM n readLn

main = do
  f 2
  g 2

and compiling with -ddump-simpl and -ddump-stg.

As far as I can see, this difference is still visible even in the optimized assembly with -O2.

So, I think it's safe to say that g is treated sufficiently polymorphically that the caveats about runtime costs of needless polymorphism do indeed apply.

Answer 2

One big difference is when you use such constraints in a type class.

class F a where f :: Int -> IO [a]
instance F Int where f n = pure [1,2,3]
instance (a ~ Int) => F a where f n = pure [1,2,3]

If you use the second instance declaration you won't be able to create any other instances because, despite the constraint, all types will unify with a.