#8953: Reifying poly-kinded type families misses kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Old description:

Consider the following two modules:

{{{ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

module A where

type family Poly (a :: k) :: * type instance Poly (x :: Bool) = Int type instance Poly (x :: Maybe k) = Double }}}

{{{ {-# LANGUAGE TemplateHaskell #-}

module B where

import Language.Haskell.TH import A

$( do info <- reify ''Poly runIO $ putStrLn $ pprint info return [] ) }}}

Compiling with HEAD yields this output:

{{{ type family A.Poly (a_0 :: k_1) :: * type instance A.Poly x_2 = GHC.Types.Double type instance A.Poly x_3 = GHC.Types.Int }}}

The problem is that the type patterns in the reified instances are just plain variables, without their kind annotations. This omission makes the instance declarations unfaithful to the original meaning.

New description: Consider the following: {{{ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TemplateHaskell #-} import Language.Haskell.TH type family Poly (a :: k) :: * type instance Poly (x :: Bool) = Int type instance Poly (x :: Maybe k) = Double $( do info <- reify ''Poly runIO $ putStrLn $ pprint info return [] ) }}} Compiling with HEAD yields this output: {{{ type family Main.Poly (a_0 :: k_1) :: * type instance Main.Poly x_2 = GHC.Types.Double type instance Main.Poly x_3 = GHC.Types.Int }}} The problem is that the type patterns in the reified instances are just plain variables, without their kind annotations. This omission makes the instance declarations unfaithful to the original meaning. -- Comment (by goldfire): Only one module is required. Previous bug description had two. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Still getting worse! Now, look at this: {{{ a :: Proxy (Proxy :: * -> *) a = undefined b :: Proxy (Proxy :: (* -> *) -> *) b = undefined $( do info_a <- reify 'a info_b <- reify 'b runIO $ mapM putStrLn $ map pprint [info_a, info_b] return [] ) }}} produces {{{ Main.a :: Data.Proxy.Proxy Data.Proxy.Proxy Main.b :: Data.Proxy.Proxy Data.Proxy.Proxy }}} Yet, the types of `a` and `b` are ''not'' the same, and assigning one to the other rightly results in a type error. Furthermore, we really need to give the kind of ''every'' type variable binder. Consider {{{ type StarProxy (a :: *) = Proxy a }}} Reifying tyvar binders omits any kinds that are `*`, yet the kind annotation here is very relevant (if `-XPolyKinds` is on). Oh, and the original problem (not reifying kind annotation on type variable patterns) can affect ''class'' instances, too, not just ''type'' instances. So, new plan: 1. Never reify a tyvar binder into a `PlainTV`. Always use `KindedTV`. 2. Include a kind annotation (`SigT`) wrapping every use of a poly-kinded tycon. This wrapping will wrap around any arguments the tycon is applied to. 3. If a class or family tyvar is polykinded, include a kind annotation on any pattern used to specialize this tyvar in instance declarations. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: Phab:D387 | -------------------------------------+------------------------------------- Changes (by goldfire): * differential: => Phab:D387 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: Phab:D387 | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"b174288b15300093a4356c853ce2ea0abb4876f5/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="b174288b15300093a4356c853ce2ea0abb4876f5" Test #8953 in th/T8953 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: Phab:D387 | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"c3ecf06018ee3d97a6536de57519af865976ce04/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="c3ecf06018ee3d97a6536de57519af865976ce04" Annotate poly-kinded type patterns in instance reification. This should fix #8953. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 7.9 Haskell | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: Phab:D387 | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"18a4a5dad3cbee3c8bb4005ec09edf401ebe294c/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="18a4a5dad3cbee3c8bb4005ec09edf401ebe294c" Update release notes for #9262 #8953 #9084. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Template Haskell | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: th/T8953 Related Tickets: | Blocking: | Differential Revisions: Phab:D387 -------------------------------------+------------------------------------- Changes (by goldfire): * owner: goldfire => * status: closed => new * version: 7.9 => 7.10.1 * resolution: fixed => * milestone: => 7.12.1 Comment: Embarrassingly, this patch misses closed type families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: th/T8953 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D387 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.1 => Comment: This won't be happening for 8.2. If you would like to see this happen please do pick it up! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8953: Reification drops necessary kind annotations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch Priority: normal | Milestone: 8.2.1 Component: Template Haskell | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: th/T8953 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D387, Wiki Page: | Phab:D2795 -------------------------------------+------------------------------------- Comment (by Ryan Scott ): In [changeset:"f65ff2c4c9b60e370a722ac7572186816e23e573/ghc" f65ff2c4/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="f65ff2c4c9b60e370a722ac7572186816e23e573" Disambiguate reified closed type family kinds in TH Summary: A continuation of #8953. This fixes an oversight in which the left-hand sides of closed type families, when reified in Template Haskell, would not be given kind annotations, even when they are necessary for disambiguation purposes in the presence of `PolyKinds`. Fixes #8953 and #12646. Test Plan: ./validate Reviewers: hvr, bgamari, austin, goldfire Reviewed By: goldfire Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2795 GHC Trac Issues: #8953, #12646 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8953#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler