#11484 closed bug (fixed)

Type synonym using -XTypeInType can't be spliced with TH

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.0.2
Component: Template Haskell Version: 8.0.1-rc1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: th/T11484
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D2146
Wiki Page:

Description

The following code compiles:

{-# 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 the code that throws the error message to invoke 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.

Change History (10)

comment:1 Changed 16 months ago 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’

comment:2 Changed 16 months ago by RyanGlScott

I did some cursory debugging on this by pretty printing the TyCon and its TyVars when 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?

comment:3 Changed 16 months ago 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 TcTyCons 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.

comment:4 Changed 16 months ago 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.

comment:5 Changed 16 months ago 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.

comment:6 Changed 15 months ago by goldfire

I've done this change, pending validation, etc.

comment:7 Changed 15 months ago by goldfire

Differential Rev(s): Phab:D2146
Status: newpatch

comment:8 Changed 15 months ago by Richard Eisenberg <eir@…>

In 7242582/ghc:

Test #11484 in th/T11484

comment:9 Changed 15 months ago by goldfire

Milestone: 8.0.2
Status: patchmerge
Test Case: th/T11484

The actual fix is in c5919f75afab9dd6f0a4a2670402024cece5da57, mentioned as comment:8:ticket:11821. Worth merging the test if you merge that patch.

comment:10 Changed 11 months ago by bgamari

Resolution: fixed
Status: mergeclosed

Merged test to ghc-8.0 as 999428588c2eb20f66b7dc1a1021aeee759e1df2.

Note: See TracTickets for help on using tickets.