[GHC] #11484: Type synonym using -XTypeInType can't be spliced with TH
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 8.0.1-rc1 Haskell | Keywords: TypeInType | 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: -------------------------------------+------------------------------------- The following code compiles: {{{#!hs {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_GHC -ddump-splices #-} module Foo where import Data.Kind type TySyn (k :: *) (a :: k) = () -- $([d| type TySyn2 (k :: *) (a :: k) = () |]) }}} But uncomment the last line, and it doesn't compile: {{{ $ /opt/ghc/head/bin/ghc Foo.hs [1 of 1] Compiling Foo ( Foo.hs, Foo.o ) Foo.hs:10:3-43: Splicing declarations [d| type TySyn2_aBH (k_aBI :: *) (a_aBJ :: k_aBI) = () |] ======> type TySyn2_a4BF (k_a4BG :: Type) (a_a4BH :: k_a4BG) = () Foo.hs:10:3: error: • Couldn't match expected kind ‘GHC.Prim.Any’ with actual kind ‘k1’ • In the type declaration for ‘TySyn2’ Foo.hs:10:3: error: • Kind variable ‘k_a4BG’ is implicitly bound in datatype ‘TySyn2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? Type variables with inferred kinds: k_a4BG (a_a4BH :: GHC.Prim.Any) • In the type declaration for ‘TySyn2’ }}} There are two issues here: 1. The error message claims that `TySyn2` is a datatype when it is actually a type synonym. This should be easy enough to fix; just change [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81... the code] that throws the error message to invoke [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81... tyConFlavour]. 2. For some reason, the type variable `a` in `TySyn2` fails to kind-check. Somehow, an `Any` got in there, but I'm not sure where it snuck in. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 RyanGlScott): (1) is fixed now. `Any` no longer appears in the error message, which is good, but now it fails with a different error message: {{{ $ /opt/ghc/8.0.1/bin/ghci GHCi, version 8.0.0.20160330: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> :set -XTemplateHaskell -XTypeInType -ddump-splices λ> import Data.Kind λ> data X; $([d| type TySyn2 (k :: *) (a :: k) = () |]) <interactive>:3:11-51: Splicing declarations [d| type TySyn2_a1aV (k_a1aW :: *) (a_a1aX :: k_a1aW) = () |] ======> type TySyn2_a5hC (k_a5hD :: Type) (a_a5hE :: k_a5hD) = () <interactive>:3:11: error: • Invalid declaration for ‘TySyn2’; you must explicitly declare which variables are dependent on which others. Inferred variable kinds: k_a5hD :: Type a_a5hE :: k • In the type synonym declaration for ‘TySyn2’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 RyanGlScott): I did some cursory debugging on this by pretty printing the `TyCon` and its `TyVar`s when [http://git.haskell.org/ghc.git/blob/7407a66d5bd29aa011f5a4228c6e2b2f7f8ad3f8... checkValidTyConVars] (the function which is producing that error message) is run. When you type in that type synonym directly, i.e., {{{ λ> type TySyn2 (k :: *) (a :: k) = () RGS TySyn2 [k_a5hY, a_a5hZ] }}} then the only type variables are `k` and `a`, as expected. But when it's spliced in from TH: {{{ λ> data X; $([d| type TySyn2 (k :: *) (a :: k) = () |]) ... <interactive>:3:11-51: Splicing declarations [d| type TySyn2_a1ba (k_a1bb :: *) (a_a1bc :: k_a1bb) = () |] ======> type TySyn2_a5hT (k_a5hU :: Type) (a_a5hV :: k_a5hU) = () RGS TySyn2 [k_a5hU[sk], k_a5hU, a_a5hV] }}} we can see how it went wrong, as GHC mistakenly believes that there are type variables. I suppose we just have to "un-skolemize" one of the occurrences of `k`... is there a function which does this? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 goldfire): My guess is that this problem is a consequence of the quite delicate design of `TcHsType.splitTelescopeTvs`. I imagine there's a way to apply a delicate patch to the delicate algorithm to fix this, but I propose a better solution that makes this all more robust: refactor `TcTyCon` to store more information about user-written telescopes (that is, lists of type variables that may have dependencies) so that `splitTelescopeTvs` becomes trivial. When I first wrote `splitTelescopeTvs` as part of the `TypeInType` work, I hadn't yet added `TcTyCon`, and I was very loathe to put surface-Haskell details about a user-written telescope into `TyCon`. But now that we have `TcTyCon`s that exist only in the first stages of type-checking, it's more reasonable to put in more surface-Haskell information. I think this refactoring would be fairly straightforward, but I'm afraid I haven't the time to do it myself. Happy to advise if you (for any value of "you") wish to take this on. Alternatively, if you want to figure out how to fix this particular problem without doing the larger refactor, I'm happy to look at that, too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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): Would you care to elaborate on what refactoring you have in mind? What source-level things were you thinking of recording, and how would it help? I confess that I have never understood `splitTelescopeTvs` despite the long, careful Note you wrote :-(. I would love to find a simpler path here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 goldfire): `getInitialKinds` produces the kind of a tycon from a `LHsQTyVars`. `kcTyClTyVars` and `tcTyClTyVars` then have to match up the bits in the `LHsQTyVars` with this produced kind, so that we know, for example, which kind variables are mentioned explicitly in the type and which aren't (affecting visibility). That is the point of `splitTelescopeTvs`, simply to find the correspondence between the `LHsQTyVars` and the kind of the tycon. With `TcTyCon`, we can just store this correspondence -- basically, storing in the `TcTyCon` exactly what `kcTyClTyVars` and `tcTyClTyVars` need to function. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 goldfire): I've done this change, pending validation, etc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2146 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => patch * differential: => Phab:D2146 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner:
Type: bug | Status: patch
Priority: normal | Milestone:
Component: Template Haskell | Version: 8.0.1-rc1
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D2146
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.2 Component: Template Haskell | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: th/T11484 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2146 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: patch => merge * testcase: => th/T11484 * milestone: => 8.0.2 Comment: The actual fix is in c5919f75afab9dd6f0a4a2670402024cece5da57, mentioned as comment:8:ticket:11821. Worth merging the test if you merge that patch. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11484: Type synonym using -XTypeInType can't be spliced with TH -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.2 Component: Template Haskell | Version: 8.0.1-rc1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: th/T11484 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2146 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged test to `ghc-8.0` as 999428588c2eb20f66b7dc1a1021aeee759e1df2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11484#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC