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?

user_2840542 · Answer

@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.

Functional dependency does not unify when bound in GADT

1 Answers