#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
#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 simonpj): Interesting. I have no idea what to do about (overlap + FDs). I would really welcome someone paying careful attention to FDs in GHC, reviewing tickets (including this one) and proposing what changes to make. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: | -------------------------------------+------------------------------------- Changes (by AntC): * related: 10675 => 10675, 9210, 8634 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Replying to [comment:2 AntC]: I've implemented the suggestion, in a version of Hugs. So throw at me your awkward cases/counter-examples. (Hugs latest release/Sep 2006 only allows `FunDeps + Overlap` if all the overlapping instances are per the strictly unify-to-equal rule. Hugs instance heads must overlap in a strict substitution order; none of GHC's allowing the potential for overlap.) Seems to be working; I have a type-level type equality test; it handles the tricky cases I'm aware of, including this ticket. #10675 is rejected. Even handles overlap of instances for TRex records. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
we can often produce much better code by directly solving for an available `Num Int` dictionary we might have at hand. This removes
#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, 15135 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by AntC): * related: 10675, 9210, 8634 => 10675, 9210, 8634, 15135 Comment: Adding related ticket, particularly ticket:15135#comment:3 and SPJ's reply at comment 6 "This is terribly unsatisfactory". Changing the optimisation level or the per-instance pragmas can change which instance is selected, and thereby the meaning of the program -- even within a single module. (The O.P. for that ticket is the familiar 'orphan instances'/separate modules -- which is at least a devil we know.) The linked manual for `-fsolve-constant-dicts` says potentially many layers of indirection and crucially allows other optimisations to fire ... This seems to be muddling up concerns: - selecting which instance satisfies a Wanted constraint (in case of Overlapping instances, this means 'best'/most closely satisfies); - vs: having resolved which instance, ''and'' determined it's the same instance as for a dictionary available at hand, ''then'' sharing the at-hand dictionary/removing layers of indirection, etc. I can see that under separate compilation, we can't be sure whether the 'best' instance in scope in the current module might get gazumped by an instance in another module. Then we can only go by the `OVERLAPPABLE` pragma. But we should always search all instances in scope in the current module, irrespective of pragmas or optimisation(?) OK that search is adding a performance hit for the compiler and it only makes a difference in case of overlap; but it shouldn't impact object code, presuming it does resolve to an at-hand dictionary. I didn't realise the pragmas had that dramatic of an effect on selecting instances. Then this applies from comment 1
I think it's arguable that an instance should only be overlappable if it says {-# OVERLAPPABLE #-}. But that's not our current spec.
Making that the rule (in some form) could detect/warn of problematic 'orphan instances'. Interpreting the rule for instances that are in no substitution order (the O.P. on this ticket #15632) still needs some head- scratching. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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, 15135, 15927 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by AntC): * related: 10675, 9210, 8634, 15135 => 10675, 9210, 8634, 15135, 15927 Comment: See #15927, where inconsistent constraints are put on the same function, and apparently do something useful(?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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, 15135, 15927, 9627, 16070 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by AntC): * related: 10675, 9210, 8634, 15135, 15927 => 10675, 9210, 8634, 15135, 15927, 9627, 16070 Comment: Adding a couple of related tickets. See also the paper linked from ticket:9627#comment:3 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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, 15135, 15927, 9627, 16070, | 16241 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by AntC): * related: 10675, 9210, 8634, 15135, 15927, 9627, 16070 => 10675, 9210, 8634, 15135, 15927, 9627, 16070, 16241 Comment: Linking #16241, which is a follow-on from #15135. Under separate compilation, `OVERLAPPABLE` gives better coherence than `OVERLAPPING`. But it's fragile. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15632#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC