[GHC] #14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: #3485 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC rejects the following instance, complaining about the use of a type synonym family in the instance head: {{{#!hs type family Fam a class Multi a b | a -> b instance Multi (Maybe a) (Fam a) }}} However, this seems too strict to me, since the second parameter of `Multi` is determined by a functional dependency. If I tweak the instance slightly to lift the second parameter out of the instance head into an equality constraint, GHC accepts the instance: {{{#!hs instance (b ~ Fam a) => Multi (Maybe a) b }}} It seems to me that, due to the functional dependency, these two instances are completely equivalent. Therefore, GHC should accept the first instance. This is similar to an old ticket, #3485, but that did not involve fundeps, so GHC’s error was correct. I’m pretty sure the addition of functional dependencies changes things, making the two actually equivalent. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: Iceland_jack (removed) Comment: Consider {{{ (A) instance (b ~ [c]) => C Int b vs (B) instance C Int [c] }}} These behave quite differently. (B) waits until the constraint to be solved looks like `C Int [something]` and then uses the instance. But (A) waits only until the constraint looks like `C Int something` and then fires the instance, generating a constraint `something ~ [c0]` where `c0` is a fresh unification variable. So for example `C Int t0`, where `t0` is a unification variable` will be solved by (A) but not by (B). It's similar with type families. I think you should write it in the (A) form if you want that behaviour. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by lexi.lambda): Could you give me an example of a program with observably different behavior between the two instances? That is, given the thing being discussed, probably a program that typechecks under the presence of one instance but not the other. Without that, I’m not familiar enough with the precise details of how the constraint solver handles functional dependencies to understand the difference. Also, even if there ''is'' a meaningful difference, is it significant enough that it would make allowing the instance defined without the equality constraint meaningless or inconsistent? ---- The example I gave in the ticket is in something of a vacuum, so allow me to give an example of what actually caused this in the first place. Specifically, I was using the `lens` library’s TH function `makeFields` on a record type that had a type family application as the type of one of its fields. The code in question looked something like this: {{{#!hs type family Fam a data Rec a = Rec { _recValue :: Fam a } makeFields ''Rec }}} This effectively generates the following code: {{{#!hs class HasValue s a | s -> a where value :: Lens' s a instance HasValue (Rec a) (Fam a) where value = -- ... }}} …which raises the error. I opened [https://github.com/ekmett/lens/issues/754 ekmett/lens#754] to raise the issue with the `lens` folks directly, and I may very well attempt to solve the issue there myself by inserting the relevant Template Haskell checks and generating the equality constraint where necessary. I just figured it would make sense to ensure I wasn’t doing a lot of extra work to circumvent a possibly unnecessary restriction in GHC. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC):
GHC rejects the following instance, complaining about the use of a type synonym family in the instance head ...
? This isn't a bug. GHC has never allowed type family applications in the instance head. (With FlexibleInstances, it does allow type synonyms.) #3485 is an enhancement request (and closed, for good reasons IMO). So the FunctionalDependency is a red herring. I agree with your suggestion on lens#754 the Template Haskell for lenses should be smarter. If there's an opportunity for an enhancement, I think there's a more general suggestion. Borrow the irrefutable patterns idea like: {{{ instance HasValue (Rec a) ~(Fam a) where ... }}} And allow `~( ... )` to be any type or family application. Treat it as syntactic sugar for: {{{ instance (b0 ~ Fam a) => HasValue (Rec a) b0 where ... -- b0 is fresh }}} Also there's an opportunity for the compiler to see that instance (as compared with others): a. doesn't really overlap b. is consistent with FunDeps c. doesn't break the Coverage Condition -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by lexi.lambda): * type: bug => feature request Comment: You’re right in that this isn’t really a bug, so I’ve changed it to a feature request. In that framing, I’m still not completely sure why this wouldn’t be a reasonable change. The coverage condition itself is precedent for weakening of restrictions in the presence of fundeps (in that case, instance decidability), and this does not seem meaningfully different to me. I could be convinced by an example of the sort that SPJ alluded to, in which an instance of the form `Multi X (Y a)` behaves differently from `(b ~ Y a) => Multi X b`, but I’m not sure sure what such an example would look like or how it would differ from a user’s point of view. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Random thoughts, we can derive `MonadReader Bool` {{{#!hs newtype A a = A (Bool -> a) deriving newtype (Functor, Applicative, Monad, MonadReader Bool) }}} but given an instance like `instance (Representable f, Rep f ~ a) => MonadReader a (Co f)`.. if we ever want to (non-standalone) derive that we cannot specify the context.. and if we can [https://www.reddit.com/r/haskell/comments/6ksr76/rfc_part_1_deriving_instanc... derive via newtypes] the `~(Rep f)` notation makes sense to have: {{{#!hs newtype B f a = B (f a) deriving newtype (Functor, Applicative, Monad) deriving via Co (B r) (MonadReader ~(Rep r)) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC):
..., I’m still not completely sure why this wouldn’t be a reasonable change.
Try to figure out the rules: * The type family application cannot appear in a 'argument position' of a FunDep. * There might be multiple FunDeps/multi-directional. (An instance parameter might be in 'argument position' by one FunDep, but 'result position' from another.) * The variables in a type family application must be already bound by parameters appearing in 'argument position'. (Or possibly determined from those via constraints -- essentially the Liberal Coverage Conditions.) It's surely easier to have a blanket rule 'no type families'/achieve the effect with equality constraints.
The coverage condition itself is precedent for weakening of restrictions in the presence of fundeps (in that case, instance decidability), and this does not seem meaningfully different to me.
Even `UndecidableInstances` doesn't allow complete chaos. If that's what you want, there's a feature request somewhere dubbed 'dysfunctional functional dependencies'.
I could be convinced by an example of the sort that SPJ alluded to, ...
First consider type synonyms appearing in instance heads: {{{ {-# LANGUAGE FlexibleInstances #-} instance Multi String String where ... -- immediately expanded to instance Multi [Char] [Char] where ... -- not: instance (b0 ~ [Char]) => Multi [Char] b0 }}} OK Let's try to concoct an example per SPJ. Suppose {{{ type family Fam a where Fam a = Int instance Multi (Maybe a) (Fam a) where ... -- immediately expanded to instance Multi (Maybe a) Int where ... }}} At the use site, GHC will wait until `b` is resolved to `Int` before it will use the instance.
... in which an instance of the form Multi X (Y a) behaves differently from (b ~ Y a) => Multi X b, but I’m not sure sure what such an example would look like or how it would differ from a user’s point of view.
You mean `Y` is a type family? I'm not seeing that `instance Multi X (Y a)` would ever be a good idea: there's nothing to tell what `a` is. Even if the use site tells `Y a ~ Int`, that's no help (unless `Y` is injective -- but that's a different scenario). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I could be convinced by an example of the sort that SPJ alluded to, in which an instance of the form Multi X (Y a) behaves differently from (b ~ Y a) => Multi X b,
It affects type inference: {{{ instance (a ~ Int) => C a instance (a ~ Bool) => C a vs instance C Int instance C Bool }}} GHC's type inference engine does not support backtracking. If it did, it could try out the former two instances one at a time, and see which one "worked". With the latter two, only one matches. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #3485 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by lexi.lambda):
It affects type inference: [snip]
Yes, I’m aware of that, but my impression was that the functional dependency changes that. Multiple instances where the only thing that changes is variables constrained by a functional dependency are illegal, ''anyway''. Therefore, I’m trying to understand if there’s some difference between these two: {{{#!hs class C a b | a -> b instance C (Maybe a) [a] }}} vs {{{#!hs class C a b | a -> b instance (b ~ [a]) => C (Maybe a) b }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC