Functional Dependencies dilemma

functionaldeps.md

hi all, I'm trying to get my head around functional dependencies I've created a simplified version of MonadReader that has no functional dependencies

class MyMonadReader r m where
  ask :: m r

What works as expected

When creating instances like

instance Monad m => MyMonadReader Bool (ReaderT r m) where
  ask = pure True
instance Monad m => MyMonadReader String (ReaderT r m) where
  ask = pure "string"

I see it compiling (as expected) and if I change MyMonadReader definition to use functional dependencies

class MyMonadReader r m | m -> r where
  ask :: m r

The code (as expected) does not compile.

    Functional dependencies conflict between instance declarations:
      instance Monad m => MyMonadReader Bool (ReaderT r m)
        -- Defined at src/Machinery/FunDep.hs:29:10
      instance Monad m => MyMonadReader String (ReaderT r m)
        -- Defined at src/Machinery/FunDep.hs:31:10

What does not work as expected

If my instances look following

instance Monad m => MyMonadReader r (ReaderT r m) where    -- <---------- THIS ONE WAS ADDED
  ask = ReaderT.ask 
instance Monad m => MyMonadReader Bool (ReaderT r m) where
  ask = pure True

I would expect the code also to not to compile. But it does. And I'm truly puzzled. Can anyone help with that puzzle? Why it does not complain, with a definition like class MyMonadReader r m | m -> r where there should be only one instance for ReaderT r m , right?

Here's what I got from FP slack :) https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?#instance-resolution

i-am-tom:kcsongor: 1 hour ago
Hahah, thanks for the nudge! Totally forgot

i-am-tom:kcsongor: 1 hour ago
the tl;dr is that the functional dependency mechanism is triggered at the call site, not the definition site. Specifically, with a -> b, b will be inferred given an a that is concrete enough that it matches one instance

i-am-tom:kcsongor: 1 hour ago
if it isn't concrete enough to match one instance, you'll get an error (overlapping instances or ambiguous types, typically)

i-am-tom:kcsongor: 1 hour ago
The thing that makes this confusing is that GHC has some very basic checks that are run when you create instances with a fundep

i-am-tom:kcsongor: 1 hour ago
namely, if I have instance D a and instance D b, where a is a valid value for b (i.e. a is "more concrete"), GHC can tell you immediately that there's a problem

i-am-tom:kcsongor: 1 hour ago
If we have a case like yours:
instance Monad m => MonadReader Bool (ReaderT r m) where
ask = pure True
instance Monad m => MonadReader String (ReaderT r m) where
ask = pure "string"
It can also detect that, concretely, the same m maps to different (concrete!) r values

i-am-tom:kcsongor: 1 hour ago
So, why does your MonadReader r (ReaderT r m) not trigger this error?

i-am-tom:kcsongor: 1 hour ago
Well, we have two instance heads: MonadReader r (ReaderT r m) and MonadReader String (ReaderT r m)

i-am-tom:kcsongor: 1 hour ago
the first involves an equality between two variables in the instance head (both of which we've called r) and the second has a concrete value for this variable

i-am-tom:kcsongor: 1 hour ago
this makes this situation just a little bit too complicated for the basic checks

i-am-tom:kcsongor: 1 hour ago
for one, you may never instantiate r to anything but String - if so, is the instance overlapping, or duplicated?

i-am-tom:kcsongor: 1 hour ago
Another way that might help to look at it is to say MonadReader r (ReaderT s m) - the first instance adds the constraint that r ~ s, the second adds that r ~ String. It's not necessarily obvious that one is "more concrete" than the other, so we don't catch it in the basic check

i-am-tom:kcsongor: 1 hour ago
so yeah, the red herring is that you ever get an error when you define the class instances, because this isn't where the check occurs. It's just that GHC has some basic rules to catch common mistakes

i-am-tom:kcsongor: 1 hour ago
and is, in general, quite conservative with those rules. It doesn't error on instances unless it's sure they'd clash, just the same as it doesn't allow instances unless it's sure they're decidable (unless you turn the relevant extension on)

Encode Panda 1 hour ago
I was confused that it sometimes was able to report immediately but sometimes was waiting for the usage

Encode Panda 1 hour ago
thx for the answer

i-am-tom:kcsongor: 1 hour ago
Yeah, GHC tries its best, but its quick checks are nowhere near perfect. It's a pretty common misunderstanding with fundeps, I think - they don't impose restrictions on your instances, they impose restrictions on your usages. GHC's just often clever enough to do both

Encode Panda < 1 minute ago
👍