[GHC] #12159: Record-like GADTs with repeated fields (of same type) rejected
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I came across a curious bug with record-like GADTs and repeated fields. Consider following code: {{{#!hs {-# LANGUAGE GADTs #-} data Foo p where Bar :: { quux' :: Bool } -> Foo Char Baz :: { quux'' :: Bool } -> Foo Int quux :: Foo p -> Bool quux (Bar q) = q quux (Baz q) = q quuxSetter :: Foo p -> Bool -> Foo p quuxSetter old@Bar{} q = old{quux' = q} quuxSetter old@Baz{} q = old{quux'' = q} }}} This compiles and all is fine. *But* GHC is supposed to create the nice `quux` and `quuxSetter` accessors for me, right? So, let's try: {{{#!hs data Foo p where Bar :: { quux :: Bool } -> Foo Char Baz :: { quux :: Bool } -> Foo Int }}} It does not compile! Instead I get: {{{ T12159.hs:3:1: error: Constructors Bar and Baz have a common field quux , but have different result types In the data type declaration for Foo Failed, modules loaded: none. }}} This is not very polite :-) It should simply create the accessors like I did above. It obviously can be done! Testcase is attached. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by heisenbug): * Attachment "T12159.hs" added. Test case -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: mpickering (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) * type: bug => feature request Comment: It probably wouldn't be difficult to generate selector functions in cases like this, but record updates are likely to be tricky, because of cases like this: {{{#!hs data Foo p where Bar :: { quux :: a } -> Foo a Baz :: { quux :: a } -> Foo [a] }}} Record updates are already quite tricky to type-check. We'd need a clear specification of what should be accepted (see also #2595). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is a dup of #8673 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Gragghlel. Look at `TcTyDecls`: {{{ Note [GADT record selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ For GADTs, we require that all constructors with a common field 'f' have the same result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon] E.g. data T where T1 { f :: Maybe a } :: T [a] T2 { f :: Maybe a, y :: b } :: T [a] T3 :: T Int and now the selector takes that result type as its argument: f :: forall a. T [a] -> Maybe a Details: the "real" types of T1,T2 are: T1 :: forall r a. (r~[a]) => Maybe a -> T r T2 :: forall r a b. (r~[a]) => Maybe a -> b -> T r So the selector looks like this: f :: forall a. T [a] -> Maybe a f (a:*) (t:T [a]) = case t of T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g)) T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g)) T3 -> error "T3 does not have field f" }}} An alternative design choice would be this: * A field is "naughty" if its type, in any constructor, mentions any existential type variables * Generate selectors only for non-naughty fields * Allow updates only of non-naughty fields In the example above, `f` is naughty because `T1`'s real type is {{{ T1 :: forall r a. (r~[a]) => a -> T r }}} And `f :: Maybe a` mentions the existential variable `a`. In contrast, in the example from the description {{{ data Foo p where Bar :: { quux :: Bool } -> Foo Char Baz :: { quux :: Bool } -> Foo Int }}} `quux :: Bool` mentions no existentials, so we can generate a perfectly fine selector. Under this scheme some fields that currently get record selectors would not get them, and vice versa. ------ I think this would be a good change * It'd mean that we used the same rule for record selectors as for record updates. Currently they are different; compare * `Note [Naughty record selectors]` in `TcTyDecls` * `Note [Criteria for update]` in `TcExpr` * We have at least two Trac tickets wanting behaviour (this one and #8673). * I dont' know anyone who needs the existing behaviour. (E.g. in data type `T` above, `f` would no longer get a record selector, although you could write one by hand.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): A few of us discussed this and believe that both cases above can be covered with a single generalisation: for all the constructors that mention the field, require that the field types are the same, then take the anti-unifier of all the result types and check that this includes all the variables mentioned by the common field type. For example: {{{#!hs data S x where S1 :: { f :: Maybe a } -> S ([a], Int) S2 :: { f :: Maybe a } -> S ([a], Bool) f :: S ([a], b) -> Maybe a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Iavor adds a couple more tricky examples: {{{ data S :: * -> * where S1 :: { s :: Bool } -> S (Int,Char) S2 :: { s :: Bool } -> S (Int,Int) }}} In this case, the anti-unifier would compute: {{{ s :: S (Int, a) -> Bool }}} However, the `Int` part is accidental, and we can use the more general: {{{ s :: S a -> Bool }}} Another example: {{{ data T :: * -> * where T1 :: { t :: Bool } -> T Bool }}} In this case we have the usual GADT problems of not knowing how much to abstract: {{{ t :: T a -> a t :: T a -> Bool }}} Neither of these is more general than the other, so it is not clear what to do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): Yes, it's not quite anti-unification, but something like "find the most general type that binds all the type variables used in the field type, and can be instantiated to all the result types". I think we can reasonably require all the fields to have syntactically the same type, and use that as the result type of the selector. So we would pick `T a -> Bool` over `T a -> a`. Moreover, this wouldn't allow the following: {{{#!hs data S :: * -> * where S1 :: { s :: a } -> S a S2 :: { s :: Bool } -> S Bool S2 :: { s :: Int } -> S Int }}} even though in principle it could have a selector of type `S a -> a`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): Just ran into this (in the “simple” case where a field would appear in all constructors with the same field type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): It just needs someone to nail down the details, write a spec (preferably a GHC proposal), and the execute -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12159: Record-like GADTs with repeated fields (of same type) rejected -------------------------------------+------------------------------------- Reporter: heisenbug | 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by vagarenko): * cc: vagarenko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC