Type not inferred by GADT match and functional depenency-CodePudding

I have a misunderstanding of the Haskell type system that I think may be common, but I cannot find an explanation for the specific type-checking failure shown by this simple example:

{-#LANGUAGE GADTs, FunctionalDependencies #-}

module GaF where

class XDeterminesY x y | x -> y
instance XDeterminesY Int Double

data Wrapper x where
    WrappedInt :: Wrapper Int

func :: XDeterminesY x y => Wrapper x -> y -> Double
func WrappedInt a = a

GHC complains that it cannot deduce y ~ Double from the context x ~ Int. I imagined that to perform such a deduction was the whole point of declaring the functional dependency.

CodePudding user response：

I imagined that to perform such a deduction was the whole point of declaring the functional dependency.

Unfortunately, this is not the case. FunDeps never refine rigid type variables as it happens during pattern matching on a GADT. Intuitively, they should do that in some cases, but they do not. I guess this is because they appeared in Haskell long before GADTs were a thing, so there was no precedent.

It is pretty annoying, I concur. That's why I believe that type families are in general a much better idea. FunDeps, in my opinion, should be replaced by type families when it is possible to do so (note that in class C a b c | a->c, b->c we indeed can not).

Note in passing that a similar failure can be observed in the injective type families extension: one would expect GHC to infer a ~ b from F a ~ F b, but it does not.

Anyway, I think you are now wondering "if this was not the point of FunDeps, what is their point?". Well, consider:

class C a b | a -> b where
   foo :: a -> b -> String
   bar :: a -> String

instance C Bool Int where ...

Without FunDeps, a call like bar True would be ambiguous: C Bool Int in one instance we could use to resolve the constraint, but there could be another one. Here, the issue is that the type bar :: a -> String does not involve b, so there is no way to know if we can safely commit to the instance. The type is deemed to be ambiguous.

With FunDeps, instead, we promise there will be no other instance, so a type involving only a is no longer ambiguous, and instance resolution can work just fine with that.

(By the way, nowadays such ambiguities can be manually resolved at the call site with type applications, but this was not the case in the past.)