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?
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 forall
s using a restriction of type equality to a type parameter of Joined
- but GHC seems to not recognise when the restriction is satisfied.
Definition you have written means that for IntGenorator
you have:
If you give me an
IntGenorator
and think of some typev
such thatOutput v ~ Integer
then I will give you something of typev
based on whatever is inside theIntGenorator
If for any type
v
such thatOutput v ~ Integer
, you can give me something of typev
then you can construct something of typeIntGenorator
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