Functional dependency does not unify when bound in GADT

Question

In the following code:

class FD a b | a -> b

data Foo a where
  Foo :: FD a b => b -> Foo a

unFoo :: FD a b => Foo a -> b
unFoo (Foo x) = x

By common sense this should work, since a is the same in constraints in both GADT and function, and it determines b, however this doesn't compile with following error:

    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        a pattern with constructor:
          Foo :: forall a b. FD a b => b -> Foo a,
        in an equation for ‘unFoo’
        at src/Lib.hs:13:8-12
      ‘b’ is a rigid type variable bound by
        the type signature for:
          unFoo :: forall a b. FD a b => Foo a -> b
        at src/Lib.hs:12:1-29
    • In the expression: x
      In an equation for ‘unFoo’: unFoo (Foo x) = x
    • Relevant bindings include
        x :: b1 (bound at src/Lib.hs:13:12)
        unFoo :: Foo a -> b (bound at src/Lib.hs:13:1)
   |
13 | unFoo (Foo x) = x
   |                 ^

is there any good reason why it doesn't work?

Hallowmas

The interactions between fundeps and GADTs, and those between injective type families and GADTs seem pretty bad at the moment. One would expect those to provide T ~ U constraints in many cases, but they apparently do not. – Cerebrovascular

Seems certainly a valid (safe!) use case for unsafeCoerce. – Jonquil

@Jonquil I think I'd prefer to rewrite it to use associated types before I reached for that footgun. – Bekha

@leftaroundabout, you might think so, but you can satisfy the fundep checker in bogus ways. instance MonadReader a U1 => MonadReader a U1 where ask = U1. The type family and GADT machinery is much more careful. – Omnibus

@Omnibus EEEK! How is that working... in particular, how is it not just sending the typechecker in a loop until we get a stack overflow? – Jonquil

@leftaroundabout, you need to enable UndecidableInstances, at which point it's perfectly happy to tie a knot and assume you know what you're doing. – Omnibus

@Omnibus sure, but I'd thought that when I then write ask :: U1 Int it should try to unify a ~ Int, leading it to unifying Int with the a in MonadReader a U1, leading it to MonadReader a U1, ... – but never typecheck. Actually though, it looks like it never bothers with any such thing. – Jonquil

Answer 1

@chi The interactions between fundeps and GADTs, ... seem pretty bad at the moment.

I think it's more fundamental than that (and not just "at the moment", and not just for FunDeps).

Whatever the compiler infers about the type of x in

unFoo (Foo x) = ...

is only valid on the RHS, within the match on (Foo x). Trying to return bare x would let any assumptions escape.

To compare a much older equivalent: before we had GADTs there were existentially-quantified data constructors, so

data Foo' a = forall b. FD a b => Foo' b

unFoo' :: FD a b => Foo' a -> b
unFoo' (Foo' x) = x

Fails to compile for the same reason.

Or trying to write an instance for FD gives the same rigid type variable trouble:

class FD a b | a -> b  where
  unFoom :: Foo a -> b
instance FD Int Bool  where
  unFoom (Foo x) = x    -- Couldn't match expected type `Bool' with actual type `b'

You might find Hugs' error message more revealing (for the existential datatype)

*** Because        : cannot instantiate Skolem constant

And I'm not convinced it's much to do with FunDeps. Compare

data FooN a where           
  FooN :: Num b => b -> FooN a

unFooN :: Num b => FooN a -> b
-- unFooN (FooN x) = x + 1                 -- rejected
unFooN (FooN x) = const undefined (x + 1)  -- accepted (but useless)

z = 1 + unFooN (FooN 7)                    -- accepted (for useless unFooN)

Rejected for the same reason: the assumption x :: Num b => b is valid only inside the match.

Addit: (in response to comments)

To expand on the "is only valid on the RHS, within the match on (Foo x)":

• In general, a GADT has many constructors, potentially each with different constraints.
• (Or indeed we might have a value with no constructor as in (undefined :: Foo t).)
• So the match has to see the constructor before applying what's 'only valid on the RHS'.

A FunDep is treated as any other constraint for those purposes, so the OP's problem is like the FooN case. (The existential b remains scoped only on RHS.)

@dfeuer's reworking using type families doesn't rely on scoping of tyvar b; the type family applies to a, which has scope throughout unFoo. That means F a has same scope. Because of the magic ~ superclass constraint, unFoo's signature is equivalent to:

unfoo: Foo a -> F a

But here be dragons: F a is not necessarily well-formed everywhere [Section 3 'Totality Trap'], because code doesn't need evidence there's an applicable instance.

So I'm going to diametrically disagree with dfeuer: the FunDep does carry evidence, just like the Num b example, and that evidence can't escape the pattern match; type family F a doesn't carry evidence (of an instance match -- the ~ constraint is taken to hold without evidence), so F a is available throughout the scope of a -- "available" doesn't mean valid.

Midlands

It's not about the presence of fundeps, but it's about what they (don't) mean. They're for inference only, not evidence. A version using type families and equality constraints compiles just fine. – Omnibus

@Omnibus so please explain the FooN example: no FunDeps; and yet apparently not (enough) evidence for Num b. – Midlands

Your example seems ... pretty much unrelated. I understand that evidence is only opened under pattern matches, but that has nothing to do with the OP's problem. The OP's problem is that fundeps don't carry evidence. – Omnibus

"The OP's problem" is that the code doesn't compile/gives a rigid type variable message. The problem with the FooN example is that the code doesn't compile/gives a rigid type variable message. I've put the same constraint on the GADT and on unFooN. Num b => does carry evidence. If the examples are "unrelated ... [because] fundeps don't carry evidence.", why isn't the constraint on FooN carrying evidence? – Midlands

"rigid type variable" is pretty generic. The OP's assumption was that the functional dependency on their FD class would behave like the equality constraint on the version I linked to. It does not. – Omnibus

I understand that in GADT, an evidence is valid only under pattern match and it cannot escape, however in case of unFoo it seems to be possible to determine that GADT's evidence and external evidence are the same, which doesn't seem to happen. In case of unFooN this is not the case and a in FooN a is phantom – Hallowmas

Fundeps definitely don't carry evidence. GHC doesn't use them for type checking at all—it only uses them for type inference. – Omnibus