Why can't GHC deduce type equality on a class type family in a Rank 2 type?

Question

As a very trimmed-down version of what I'm experiencing:

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
class ValueGen v where
  type Output v
  generate :: v -> Output v

instance ValueGen Integer where
  type Output (Integer) = Integer
  generate n = n + 1

newtype IntGenerator = Gen { generator :: forall v. ValueGen v => ((Output v) ~ Integer) => v }

myGen :: IntGenerator
myGen = Gen (3 :: Integer)

The error that GHC gives is

Could not deduce: v ~ Integer
from the context: (ValueGen v, Output v ~ Integer)
  bound by a type expected by the context:
            forall v. (ValueGen v, Output v ~ Integer) => v

This works fine if I just try to restrict v by type equality.

What is the issue that GHC is encountering? Why is it trying to deduce the restriction v ~ Integer if that's already informed by the typing of 3 :: Integer? Shouldn't the restriction check be that Output Integer, which resolves to Integer, is equal to Integer, and then pass?

Abstract

I hit this trying to write a rank 2 type which contained two Pipeline class instances which share some intermediate type. The essential idea was to get two pipelines like

a|---|b  b|---|c

and produce a new type Joined which is then an instance of Pipeline

a|------------|c
a|---|b  b|---|c

The issue is that the inner pipelines are stored with internal foralls using a restriction of type equality to a type parameter of Joined - but GHC seems to not recognise when the restriction is satisfied.

Answer 1

Definition you have written means that for IntGenorator you have:

If you give me an IntGenorator and think of some type v such that Output v ~ Integer then I will give you something of type v based on whatever is inside the IntGenorator

If for any type v such that Output v ~ Integer, you can give me something of type v then you can construct something of type IntGenorator

Because the type family is not injective there could be other types v than Integer such that Output v ~ Integer (note they could be in modules which ghc hasn’t compiled yet or which haven’t been written yet). Therefore ghc cant prove that the only type v with Output v ~ Integer is Integer (or rather some set of types which implement Num) and that therefore 3 :: Integer (or rather 3 :: Num a => a) is a valid value of the type forall v. (Output v ~ Integer) => v.

E.g. what if someone added an instance ValueGen Char with Output Char = Integer. Then 3 is certainly not of type Char (unless one implements Num Char) so you can’t put it inside an IntGenerator