[GHC] #15927: Weird interaction between fundeps and overlappable instances

[GHC]

#15927: Weird interaction between fundeps and overlappable instances
-------------------------------------+-------------------------------------
        Reporter:  Darwin226         |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
                                     |  FunctionalDependencies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  10675, 15632      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

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

 * The two instances for `MyState`are 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:

 {{{#!hs
 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:

 {{{#!hs
 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:

 {{{#!hs
     * 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?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15927#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler