Opened 10 months ago

Last modified 9 months ago

#15927 new bug

Weird interaction between fundeps and overlappable instances

Reported by: Darwin226 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: FunctionalDependencies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: 10675, 15632 Differential Rev(s):
Wiki Page:

Description

Consider this code

class MyState s m | m -> s where
    getMyState :: m s
instance {-# OVERLAPPABLE #-} (MyState s m, MonadTrans t, Monad m) => MyState s (t m) where
    getMyState = lift getMyState
instance Monad m => MyState s (StateT s m) where
    getMyState = get

f :: (MyState Int m, MyState Char m, MonadIO m) => m ()
f = do
    int <- getMyState
    str <- getMyState
    liftIO $ putStrLn (replicate int str)


works1 :: (MyState s m, Show s, MonadIO m) => m ()
works1 = do
    a <- getMyState
    liftIO (print a)

works2 = runStateT (runStateT f (5 :: Int)) 'a'

It defines a class similar to MonadState of mtl. There is a functional dependency in place, just like with MonadState and we can see that it works the same because works1 compiles where a would have an ambiguous type otherwise.

The f function "shouldn't" compile because it's using two different states at once subverting the functional dependency restriction. It does however compile because an explicit type signature is provided with an unsolvable constraint.

Now the really weird part is that works2 also compiles and produces the expected result even though it's using f.

Here's what I think is happening: instance resolution is looking for MyState Int (StateT Char m) and it finds the MyState s (StateT s m) instance. Instead of complaining that Int doesn't match Char (due to the fundep), it just rejects the instance and takes the overlappable one that does match. In the case where the state is unknown (i.e. both instances match), the fundep kicks in. That's why runStateT works1 True works.

Is this intended behavior? It seems pretty useful in some situations and I've tested this with 8.2 and 8.6 with the same results.

Change History (8)

comment:1 Changed 10 months ago by AntC

Keywords: FunctionalDependencies added

Yes you could always evade FunDep consistency like that -- see #10675 at "bogus"; or #15632 for a cut-down example.

Well done for getting that inconsistency into the same constraint!

There's nothing stopping you putting a bunch of constraints that are together unsatisfiable. That would usually mean you couldn't use f.

comment:2 Changed 10 months ago by Darwin226

I'm sorry if you addressed this in your comment and I'm just not getting it, but note that I'm not just declaring f with and unsatisfyable constraint. I'm also able to satisfy it! So writing

g :: StateT Int (StateT Char IO) ()
g = f

works.

So are you saying that this behavior can be relied on? Is my code likely to get broken in newer GHC versions?

comment:3 in reply to:  2 Changed 10 months ago by AntC

Replying to Darwin226:

I'm sorry if you addressed this in your comment and I'm just not getting it, but note that I'm not just declaring f with and unsatisfyable constraint. I'm also able to satisfy it!

Sorry if I was a bit oblique. I'm totally impressed that works. I would never have thought of trying it.

So are you saying that this behavior can be relied on? Is my code likely to get broken in newer GHC versions?

Good questions! I'll leave GHC HQ to answer definitively. Here's my take:

This behaviour has been around since at least 2004: it's exploited in the HList paper, but the authors felt very uncomfortable about it. If you read #10675, SPJ describes GHC's behaviour as "bogus" and not supported by any of the academic theory around FunDeps -- including the 2006 paper of which he is a co-author. So yes your code might break in future releases, except ...

There is a lot of code out there that exploits this loophole. (Usually with overlapping instances + FunDeps, but not exactly your ruse of putting contrary constraints on the same function.) So as my comments conclude on #10675, 'fixing' this will probably cause howls of outrage/break a fair amount of code. AFAICT nobody at GHC HQ is interested in anything around FunDeps/Overlaps, and hasn't been for a long time. So they will probably say:

a) No, that behaviour can't be relied on.

b) We're not going to 'fix' it, so you can get away with it for probably another decade.

c) Use Closed Type Families instead of the FunDep, and make MyState a single parameter typeclass.

I was going to try your code in my version of Haskell that (I think) takes a more principled approach. Just hang on a bit.

comment:4 Changed 10 months ago by AntC

A more-principled FunDep consistency (see #15632) says:

  • The two instances for MyStateare fine (but see below):
    • the FunDep is full;
    • the instance heads are in a strict substitution order;
    • on the more specific instance, its argument side (StateT s m) is strictly more specific -- i.e. than (t m).

However the signature for f gets rejected:

  • "Constraints are not consistent with Functional Dependencies"

d'uh. If I comment out the signature, that type gets inferred anyway, and rejected for the same reason.

Whereas in GHC, works2 does indeed work and produce the expected output. (I needed to give it a signature to say it's in IO.)

And using your g works, as you say, without a signature:

works3 = runStateT (runStateT g (7 :: Int)) 'b'

Instead of complaining that Int doesn't match Char (due to the fundep), it just rejects the instance and takes the overlappable one that does match.

Yes your analysis is correct. And that's a folk-art way to subvert the FunDep. To prove your analysis, change the more-specific instance:

instance (Monad m, s ~ s') => MyState s' (StateT s m) where
    getMyState = get

By avoiding the repeated s in your original instance this says:

  • If the wanted m is of the form (StateT s m),
  • then match anything for the s' (because it's a distinct bare variable),
  • and improve the s' to s from the StateT.

We still get the definition of f accepted, but we can't use it:

    * Couldn't match type `Int' with `Char' arising from a use of `f'
    * In the first argument of `runStateT', namely `f'
      In the first argument of `runStateT', namely
        `(runStateT f (5 :: Int))'
      In the expression: runStateT (runStateT f (5 :: Int)) 'a'

What that revised instance is doing, with the ~ constraint, is making explicit the 'official' semantics for improvement under a FunDep, as per the FunDeps through CHRs paper.

That's also the semantics followed for a Closed Type Family.

behavior ... seems pretty useful in some situations

Yeah. Add the example to the "dysfunctional Functional Dependencies" #8634.

Wise counsel would be not to rely on it/can you refactor your code?

comment:5 in reply to:  4 Changed 10 months ago by AntC

You've clearly unearthed an(other) example of GHC's bogusness with FunDeps+Overlaps. Without wanting to take anything away from that ...

Replying to AntC:

behavior ... seems pretty useful in some situations

... can you refactor your code?

The code as currently is fragile and non-scalable. It relies on the payload content of the StateTs having distinct types. You can do this

f :: (MyState Int m, MyState Char m, MyState String m, MonadIO m) => m ()
                                    -- believe 3 impossible things before breakfast
f = do
    int <- getMyState
    char <- getMyState
    str <- getMyState
    liftIO $ putStrLn ((replicate int char) ++ str)
  • But it doesn't work if f wants two values of the same type. (getMyState will always get the first-bound.) ... liftIO $ putStrLn (str1 ++ str2)

I suggest you want either

  • depth-based access: getMyState has an extra parameter for the depth. Or it very cleverly takes the content from this layer and unwraps one layer of State for the next call. Now you need a PolyMonad; or
  • type-indexed access: wrap each layer's content in a newtype. Make sure they're distinct types.

Type-indexed access is in effect what you have: you can remove the FunDep from MyState, and f is happy, its multiple MyState constraints make sense, works2 still works. works1 stops working, because it needs the FunDep.

Last edited 10 months ago by AntC (previous) (diff)

comment:6 Changed 10 months ago by Darwin226

Well, since the mtl default is to not only disallow multiple states of the same type, but multiple states of ANY type, I wouldn't really call this non-scaleable. It's strictly more flexible than mtl.

Last edited 10 months ago by Darwin226 (previous) (diff)

comment:7 in reply to:  6 Changed 10 months ago by AntC

Replying to Darwin226:

Well, since the mtl default is to not only disallow multiple states of the same type, but multiple states of ANY type, I wouldn't really call this non-scaleable. It's strictly more flexible than mtl.

I'm not following: the approach you're using 'allows' multiple states of same type in the sense you can stack a String on top of a String. But it's useless: getMyState as written will only access one of them. Then being "flexible" in this way, is only going to lead to confusion.

Monad Transformers used to do this stacking. (I'm talking over 10 years ago.) The l in mtl stands for library: in general many modules might import mtl and declare instances of MonadTrans. If mtl were still relying on overlapping instances, it would be impossible/difficult to co-ordinate the instances to each use a unique type; and any code in modules using the stack would risk the well-known issues of 'orphan instances'.

Perhaps your intended usage has a different pattern, and you're prepared to do the co-ordination manually. But at least for a sanity check, validate when you add a type to the stack that it's unique.

comment:8 Changed 9 months ago by bgamari

Milestone: 8.6.3

Ticket retargeted after milestone closed

Note: See TracTickets for help on using tickets.