[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
      Resolution:                    |             Keywords:
                                     |  FunctionalDependencies,
                                     |  OverlappingInstances
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  10675, 9210,      |  Differential Rev(s):
  8634                               |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 There is a structure of instances for which the suggested rules at
 comment:2 are over-restrictive: you can code round it under the rules, but
 awkwardly. I'd appreciate feedback on how common this is: a diamond
 overlap pattern. Consider

 {{{#!hs
 class Whuther a b  | a -> b  where ...

 instance Whuther (Int, a2, Bool) Hither  where ...

 instance (b ~ Thither) => Whuther (Int, a2, a3) b  where ...

 instance (b ~ Thither) => Whuther (a1, a2, Bool) b  where ...

 instance (b ~ Yon) Whuther (a1, a2, a3) b  where ...

 }}}

 The `Hither`instance is strictly more specific than any of the other
 three; the `Yon` instance is strictly more general. The two `Thither`
 instances overlap, but are in no substitution order, so don't meet
 conditions B ii), B iii) above. (For the example, it's not necessary the
 two instances produce the same result type for `b`, it just makes the
 example more poignant. Also it's not necessary for there to be a more
 general instance; in practice there usually is a 'catch-all'.)

 Currently GHC accepts this example, and does the 'right thing'. (Saying
 GHC accepts it is not much of a claim: GHC will accept nearly any rubbishy
 set of instances; whether it does the 'right thing' in all cases needs a
 lot of testing.)

 The example can be coded within the rules, via an auxiliary class:

 {{{#!hs
 class Whuther a b  | a -> b  where ...

 instance Whuther (Int, a2, Bool) Hither  where ...

 instance (b ~ Thither) => Whuther (Int, a2, a3) b  where ...

 instance (Whuther2 (a1, a2, a3) b) => Whuther (a1, a2, a3) b  where ...

 class Whuther2 a b  | a -> b  where ...

 instance (b ~ Thither) => Whuther2 (a1, a2, Bool) b  where ...

 instance (b ~ Yon) Whuther2 (a1, a2, a3) b  where ...

 }}}
 This has taken a symmetric set of instances to asymmetric, arbitrarily
 moving one of the instances into the auxiliary class.

 A very similar set of instances that GHC also accepts, but for which it's
 not clear what would be the 'right thing':

 {{{#!hs
 class Whuther a b  | a -> b  where ...

 instance Whuther (Int, Char, Bool) Hither  where ...

 instance (b ~ Thither) => Whuther (Int, a2, a3) b  where ...

 instance (b ~ Thither) => Whuther (a1, a2, Bool) b  where ...

 instance (b ~ Yon) Whuther (a1, a2, a3) b  where ...

 }}}

 These are accepted because of GHC's delayed/relaxed overlap check. then
 consider a wanted `Whuther (Int, a2, Bool) b` in which `a2` is known to be
 apart from `Char`. This gives irresolvable overlap, because there's no
 reason to prefer either of the `Thither` instances.

 I could amend the rules, still keeping within the idea of pairwise
 validation of instance heads. If A), B) fail:

 C) Relax to follow GHC's bogus consistency check providing all of

     i) The FunDep is full;

     ii) The instances overlap but neither is strictly more specific;
         there is a third instance strictly more specific than either; and

     iii) that third instance's argument positions taken together are
 exactly at the unification of the two partially-overlapping instances'
 argument positions.

         (i.e. the third instance's result positions are not less specific
 than the unification.)

 C ii), iii) together need search amongst instances. Note there could be at
 most one instance that would meet the criteria:

 * `Whuther (Int, a2, Bool) Hither` meets C ii), its `(Int, a2, Bool)`
 exactly meets C iii).

 * `Whuther (Int, Char, Bool) Hither` meets C ii), but its `(Int Char,
 Bool)` is too specific for C iii).

 * Note that both of those instances could legitimately be in scope under
 the rules: they're in a strict substitution order; and their FunDep result
 position is the same (meets condition A)'s strict consistency condition).

 To make the search a bit more deterministic, we could revise C ii) to
 require

 C)    ii') Neither of the instances is strictly more specific; and
         there is a third instance at exactly the unification of the two
 instances.

 Then C iii) is not needed. Under C ii'), the example at the top of this
 comment would be rejected, but the `Hither` instance could be amended to:

 {{{#!hs

 instance (b ~ Hither) => Whuther (Int, a2, Bool) b  where ...
 }}}

 And that would still allow another `instance Whuther (Int, Char, Bool)
 Hither`, which is strictly more specific yet.

 I've tried coding either version of rule C). It needs **either** entirely
 restructuring the consistency check to delay until all the instances are
 visible (rather than validating instances one-by-one in order of textual
 appearance); **or** requiring the programmer write the overlapping
 instances in textual order most-specific first. Usual practice is to write
 most-specific first. Never the less this makes the validation rules
 brittle: programmers won't appreciate error messages suggesting re-
 ordering their instances ''might'' help (no guarantee).

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