[GHC] #15632: Undependable Dependencies

[GHC]

#15632: Undependable Dependencies
-------------------------------------+-------------------------------------
           Reporter:  AntC           |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:                 |  Operating System:  Unknown/Multiple
  FunctionalDependencies,            |
  OverlappingInstances               |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  10675
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider

 {{{#!hs
 {-# LANGUAGE  MultiParamTypeClasses, FunctionalDependencies,
               GADTs, FlexibleInstances, FlexibleContexts,
               UndecidableInstances   #-}


 data Hither = Hither  deriving (Eq, Show, Read)         -- just three
 data Thither = Thither  deriving (Eq, Show, Read)       -- distinct
 data Yon = Yon  deriving (Eq, Show, Read)               -- types

 class Whither a b  | a -> b  where
   whither :: a -> b -> b

 -- instance Whither Int Hither  where   -- rejected: FunDep conflict
 --   whither _ y = y                    -- with Thither instance, so

 instance {-# OVERLAPPING #-} (b ~ Hither) => Whither Int b  where
   whither _ y = y

 instance {-# OVERLAPS #-} Whither a Thither  where
   whither _ y = y
 instance {-# OVERLAPPABLE #-} (b ~ Yon) => Whither a b  where
   whither _ y = y

 f :: Whither Int b => Int -> b -> b
 f = whither

 g :: Whither Bool b => Bool -> b -> b
 g = whither
 }}}

 Should those three instances be accepted together? In particular, the
 published work on FDs (including the FDs through CHRs paper) says the
 `Thither` instance should behave as if:

 {{{#!hs
 instance (beta ~ Thither) => Whither a beta  where ...
 }}}
 (in which `beta` is a unification variable and the `~` constraint is type
 improvement under the FD.) But now the instance head is the same as the
 `Yon` instance, modulo alpha renaming; with the constraints being
 contrary.

 That's demonstrated by the inferred/improved type for `g`:

 {{{#!hs
 *Whither> :t g
 ===> g :: Bool -> Thither -> Thither             -- and yet

 *Whither> g True Yon
 ===> Yon
 }}}

 What do I expect here?
 * At least the `Thither` and `Yon` instances to be rejected as
 inconsistent under the FunDep.
 * (The `Hither` instance is also inconsistent, going by the strict
 interpretation in published work. But GHC's rule here is bogus, as
 documented in Trac #10675.)

 Exploiting Overlapping instances is essential to making this go wrong. The
 published work shies away from considering `FunDeps + Overlap`; and yet
 specifying the semantics as if the instances used bare unification
 variables is almost inevitably going give overlaps -- especially if there
 are multiple FDs.

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