[GHC] #15632: Undependable Dependencies
GHC
ghc-devs at haskell.org
Thu Sep 13 07:53:34 UTC 2018
#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
More information about the ghc-tickets
mailing list