[GHC] #10719: Malformed data type quotation accepted

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- This is accepted: Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A where C :: C |])}}} "[DataD [] A_1627402878 [] [ForallC [] [] (NormalC C_1627402879 [])] []]" In contrast this is rejected: Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A p where C :: C |])}}} <interactive>:29:22: Malformed constructor result type: C However it would make sense to form an equality constraint (for later kind/type checking) in these cases, something along the lines of: {{{#!hs data A p where C :: (A p ~ C) => C }}} as there could be type synonym (or family) `C`. I have tested various versions >= 7.8.3 and all seem to behave the same. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by heisenbug): I should add that `:set -XDataKinds` and `:set -XTemplateHaskell` are on. I have played around a bit and these are actually accepted Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| type C = A; data A x where C :: 'C Int |])}}} "[TySynD C_1627404906 [] (ConT A_1627404904),DataD [] A_1627404904 [PlainTV x_1627404907] [ForallC [] [AppT (AppT EqualityT (VarT x_1627404907)) (ConT GHC.Types.Int)] (NormalC C_1627404905 [])] []]" Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A x where C :: 'C Int |])}}} "[DataD [] A_1627405048 [PlainTV x_1627405050] [ForallC [] [AppT (AppT EqualityT (VarT x_1627405050)) (ConT GHC.Types.Int)] (NormalC C_1627405049 [])] []]" with both `DataKinds` and `NoDataKinds`. All is very suspicipus, I think the result type's head is never checked. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * component: Compiler => Template Haskell -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by heisenbug): Here is the rest of the diagnosis: {{{ compiler/deSugar/DsMeta.hs:626: | Just (_, tys) <- hsTyGetAppHead_maybe res_ty }}} Name if the constructor (or whatever) is ignored here. We should know whether it is a constructor/variable and and check against the GADT name (when constructor) otherwise issue an extra equality constraint. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by jstolarek: Old description:
This is accepted:
Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A where C :: C |])}}}
"[DataD [] A_1627402878 [] [ForallC [] [] (NormalC C_1627402879 [])] []]"
In contrast this is rejected: Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A p where C :: C |])}}}
<interactive>:29:22: Malformed constructor result type: C
However it would make sense to form an equality constraint (for later kind/type checking) in these cases, something along the lines of: {{{#!hs data A p where C :: (A p ~ C) => C }}} as there could be type synonym (or family) `C`.
I have tested various versions >= 7.8.3 and all seem to behave the same.
New description: This is accepted: {{{ Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A where C :: C |])}}} "[DataD [] A_1627402878 [] [ForallC [] [] (NormalC C_1627402879 [])] []]" }}} In contrast this is rejected: {{{ Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A p where C :: C |])}}} <interactive>:29:22: Malformed constructor result type: C }}} However it would make sense to form an equality constraint (for later kind/type checking) in these cases, something along the lines of: {{{#!hs data A p where C :: (A p ~ C) => C }}} as there could be type synonym (or family) `C`. I have tested various versions >= 7.8.3 and all seem to behave the same. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by jstolarek: Old description:
This is accepted:
{{{ Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A where C :: C |])}}}
"[DataD [] A_1627402878 [] [ForallC [] [] (NormalC C_1627402879 [])] []]" }}}
In contrast this is rejected:
{{{ Prelude Language.Haskell.TH> {{{$(stringE . show =<< [d| data A p where C :: C |])}}}
<interactive>:29:22: Malformed constructor result type: C }}}
However it would make sense to form an equality constraint (for later kind/type checking) in these cases, something along the lines of: {{{#!hs data A p where C :: (A p ~ C) => C }}} as there could be type synonym (or family) `C`.
I have tested various versions >= 7.8.3 and all seem to behave the same.
New description: This is accepted: {{{ Prelude Language.Haskell.TH> $(stringE . show =<< [d| data A where C :: C |]) "[DataD [] A_1627402878 [] [ForallC [] [] (NormalC C_1627402879 [])] []]" }}} In contrast this is rejected: {{{ Prelude Language.Haskell.TH> $(stringE . show =<< [d| data A p where C :: C |]) <interactive>:29:22: Malformed constructor result type: C }}} However it would make sense to form an equality constraint (for later kind/type checking) in these cases, something along the lines of: {{{#!hs data A p where C :: (A p ~ C) => C }}} as there could be type synonym (or family) `C`. I have tested various versions >= 7.8.3 and all seem to behave the same. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11341 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #11341 Comment: Representation of GADTs has changed (#11341) since this was reported. Now we get: {{{ ghci> $(stringE . show =<< [d| data A where C :: C |]) "[DataD [] A_1627425412 [] Nothing [GadtC [C_1627425413] [] (PromotedT C_1627425413)] []]" ghci> $(stringE . show =<< [d| data A p where C :: C |]) "[DataD [] A_1627426432 [PlainTV p_1627426434] Nothing [GadtC [C_1627426433] [] (PromotedT C_1627426433)] []]" ghci> $(stringE . show =<< [d| type C = A; data A x where C :: 'C Int |]) "[ TySynD C_1627426587 [] (ConT A_1627426585) , DataD [] A_1627426585 [PlainTV x_1627426588] Nothing [GadtC [C_1627426586] [] (AppT (PromotedT C_1627426586) (ConT GHC.Types.Int))] []]" ghci> $(stringE . show =<< [d| data A x where C :: 'C Int |]) "[DataD [] A_1627426731 [PlainTV x_1627426733] Nothing [GadtC [C_1627426732] [] (AppT (PromotedT C_1627426732) (ConT GHC.Types.Int))] []]" }}} I believe that quoting works correctly here. Note also that all four definitions are invalid and they are correctly rejected by HEAD if you quote them and splice them in immediately. (Also, (3) and (4) are semantically equivalent since the type synonym is not used in any way.) This definition is also rejected by HEAD: {{{#!hs data A p where C :: (A p ~ C) => C }}} Unless I am missing something, I would close this report as invalid. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11341, #10828 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: #11341 => #11341, #10828 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10719: Malformed data type quotation accepted -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11341, #10828 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: Closing in concurrence with jstolarek. Reopen if you feel otherwise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10719#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC