[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             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Here's my starter for 10, analysis and rationale below.

 A) Apply the FunDep consistency check as per the published work.
    That is, per Definition 6 of the FDs through CHRs paper.
    If the FunDep's argument positions of the instance head unify, their
 results must be strictly ''equal''.

 Except:

 B) Relax to follow GHC's [ticket:10675#comment:15 'bogus consistency
 check'] providing all of
    i)   The FunDep is full;

    ii)  One of the instances is strictly more specific; and

    iii) That instance's argument positions taken together are strictly
 more specific.
         (i.e. the result positions are not less specific.)

    (The bogus consistency check is that the result positions be unifiable
 rather than equal under the substitution induced by unifying the
 arguments.)

 So the example on this ticket gets rejected: although the `Thither`
 instance is strictly more specific than the `Yon`, its argument position
 is not. Furthermore the `Thither` instance is in no substitution ordering
 wrt to the `Hither` instance. The `Hither` and `Yon` instances are happy
 together, and in a substitution ordering.

 Note these rules allow nearly all of the dubious instances discussed in
 the various tickets (including 'dysfunctional dependencies'), ''but''
 insist you write them in a convoluted way that would be a big hint you're
 probably doing something silly.

 > reviewing tickets (including this one)

 I've added some more ticket links to this one; #10675 is the authority.

 > someone paying careful attention to FDs in GHC.

 That's what [https://github.com/ghc-proposals/ghc-proposals/pull/56 this
 proposal] was about. Search for the ticket numbers in the discussion.

 I'll also add a comment to #10675 explaining how to apply the rules for
 it; and giving the inferred types (much more sensible).

 '''Rationale'''

 > proposing what changes to make

 What we ''don't'' want is to go delving into constraints or some global
 search amongst instances in scope. IOW we do want rules that can be
 applied pairwise between instances and per-FunDep. That also makes it
 easier to explain to puzzled users why their instances are being rejected.

 In general there might be multiple FunDeps; a parameter position might be
 an argument for one FunDep but a result for another. For non-full FunDeps
 (which is #10675) I don't think there's anything we could do other than
 apply the strict rule. But you can evade that rule (deliberately so) with
 a strictly more general/overlappable instance.

 And I think that relaxation is justified because putting unification
 variables in result positions is a) what the published work gives as the
 semantics; and b) gives you overlapping instances in effect anyway.

 Specifically, the above rules authorise what we've been doing for over a
 dozen years to get a type-level type equality predicate

 {{{#!hs
 class TypeEq a b (r :: Bool)  | a b -> r
 instance TypeEq a a True
 instance {-# OVERLAPPABLE #-} (f ~ False) => TypeEq a b f
 }}}

 The equal instance is equivalent to, and could happily be written as

 {{{#!hs
 instance {-# OVERLAPPING #-} (t ~ True) => TypeEq a a t
 }}}

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